Finite Field
30-sec diagnosis
Back to NPA

Declaration

local_eq_refl

Mathlib.Topology.Metric.Basic

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

forall (X : Sort u), forall (Y : Sort v), forall (domain : forall (x : X), Prop), forall (f : forall (x : X), Y), @LocalEq.{u,v} X Y domain f f

Proof term

fun X => fun Y => fun domain => fun f => fun (x : X) => fun (hx : domain x) => @Eq.refl.{v} Y (f x)

Constants

Mathlib.Topology.Metric.Basic.LocalEq

Interface hash: sha256:1aeefaf1faffec3f4b418f515c6834bb3430074860ff7c26124f8535f0e4f4f4