English
There exists a unique function whose graph is a given relation R if and only if for every a there exists a unique b with aRb.
Русский
Существует единственная функция, граф которой равен данной relation R, тогда и только тогда, когда для каждого a существует единственный b с aRb.
LaTeX
$$$(\exists! f, \text{graph } f = R) \iff \forall a, \exists! b, a \sim_R b$$$
Lean4
theorem exists_graph_eq_iff (R : SetRel α β) : (∃! f, Function.graph f = R) ↔ ∀ a, ∃! b, a ~[R] b :=
by
constructor
· rintro ⟨f, rfl, _⟩ x
simp
intro h
choose f hf using fun x ↦ (h x).exists
refine ⟨f, ?_, by aesop⟩
ext ⟨a, b⟩
constructor
· aesop
· exact (h _).unique (hf _)
