rel_eq — Mathlib

English

Let r be a biunique relation between α and β. Then for any a,b and a',b' with r a b and r a' b', we have (a = a') ↔ (b = b').

Русский

Пусть r — биуникальная связь между α и β. Тогда для любых a,b,a',b' с r a b и r a' b' имеем (a = a') ↔ (b = b').

LaTeX

$$$ \\forall a,b,a',b',\\ (r(a,b) \\land r(a',b')) \\rightarrow (a=a') \\leftrightarrow (b=b') $$$

Lean4

theorem rel_eq {r : α → β → Prop} (hr : BiUnique r) : (r ⇒ r ⇒ (· ↔ ·)) (· = ·) (· = ·) := fun _ _ h₁ _ _ h₂ =>
  ⟨fun h => hr.right h₁ <| h.symm ▸ h₂, fun h => hr.left h₁ <| h.symm ▸ h₂⟩

Похожие утверждения