congr

Énoncé

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

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

Cette déclaration vient du cœur de Lean 4 (Init.Prelude) et non de ce dépôt. Elle figure dans la bibliothèque parce que la liste blanche du projet l’autorise.