English
A relation r : α → β → Prop is function-like (each a has a unique b with r a b) if and only if there exists a function f : α → β such that r a b ↔ f a = b.
Русский
Отношение r : α → β → Prop является «функциональным» (у каждого a существует единственный b, такой что r a b), тогда и только тогда существует функция f : α → β с r a b ↔ f a = b.
LaTeX
$$$ \forall {\alpha} {\beta} {r : {\alpha} → {\beta} → Prop},\; (\forall a, \exists! b, r a b) \leftrightarrow \exists f : {\alpha} → {\beta}, \forall {a b}, r a b \leftrightarrow f a = b$$$
Lean4
/-- A 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 function `f`. -/
theorem forall_existsUnique_iff {r : α → β → Prop} : (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, ∀ {a b}, r a b ↔ f a = b :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· refine ⟨fun a ↦ (h a).choose, fun hr ↦ ?_, fun h' ↦ h' ▸ ?_⟩
exacts [((h _).choose_spec.2 _ hr).symm, (h _).choose_spec.1]
· rintro ⟨f, hf⟩
simp [hf]
