DeZero.congr_fun

Énoncé

∀ {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : f = g) (a : α), f a = g a

De deux fonctions égales, tire l’égalité de leurs valeurs en un point.

Axiomes consommés

Aucun. Cet énoncé se démontre à partir des seules règles du noyau — il ne coûte rien à qui accepte Lean.

Code

/-- Congruence sur la fonction. -/
theorem congr_fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : f = g) (a : α) :
    f a = g a :=
  Eq.rec (motive := fun x _ => f a = x a) rfl h