English
A symmetric relation r : α → α → Prop is function-like iff there exists an involutive function f such that ∀ {a b}, r a b ↔ f a = b.
Русский
Симметричное отношение r функционально тогда и только тогда, когда существует инволютивная функция f такая, что ∀ {a b}, 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 ∧ ∀ {a b}, r a b ↔ f a = b := by
simp [hr.forall_existsUnique_iff', funext_iff]
