English
A symmetric relation r : α → α → Prop is function-like iff there exists an involutive function f with r a b ↔ f a = b.
Русский
Симметричное отношение r : α → α → Prop функционально тогда и только тогда, когда существует инволютивная функция f с r a b ↔ f a = b.
LaTeX
$$$ \\forall {\\alpha} {r : {\\alpha} → {\\alpha} → Prop}, \\operatorname{Symmetric} r \\Rightarrow (\\forall a, \\exists! b, r a b) \\leftrightarrow \\exists f : {\\alpha} → {\\alpha}, \\operatorname{Involutive} f ∧ \\forall {a b}, r a b \\leftrightarrow f a = b$$$
Lean4
/-- A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`. -/
protected theorem forall_existsUnique_iff' {r : α → α → Prop} (hr : Symmetric r) :
(∀ a, ∃! b, r a b) ↔ ∃ f : α → α, Involutive f ∧ r = (f · = ·) :=
by
refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩
rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩
exact ⟨f, symmetric_apply_eq_iff.1 hr, rfl⟩
