DeZero.congr_both

Énoncé

∀ {α : Sort u} {β : Sort v} {f : α → β} {g : α → β} {a : α} {b : α} (hf : f = g) (ha : a = b), f a = g b

Si deux fonctions sont égales et leurs arguments aussi, les résultats le sont.

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 simultanée sur la fonction et sur l'argument. -/
theorem congr_both {α : Sort u} {β : Sort v} {f g : α → β} {a b : α} (hf : f = g) (ha : a = b) :
    f a = g b :=
  eq_trans (congr_fun hf a) (congr_arg g ha)