forall_existsUnique_iff' — Mathlib

English

A relation r is function-like iff there exists f with r = (f · = ·).

Русский

Отношение r функционально тогда и только тогда, когда существует функция f такая, что r = (f · = ·).

LaTeX

$$$ \forall {\alpha} {\beta} {r : {\alpha} → {\beta} → Prop}, (\forall a, \exists! b, r a b) \leftrightarrow \exists f : {\alpha} → {\beta}, r = (f \cdot = \cdot)$$$

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 : α → β, r = (f · = ·) := by
  simp [forall_existsUnique_iff, funext_iff]

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