English
Vertical line test for sets of pairs: if the projection to the first factor is bijective, then the set is the graph of a function.
Русский
Вертикальная линейная проверка для множеств пар: если проекция на первую координату биективна, множество является графиком функции.
LaTeX
$$$\exists f : β \to γ, s = \operatorname{graphOn}(f, \mathsf{univ})$$$
Lean4
/-- **Vertical line test** for functions.
Let `s : Set (β × γ)` be a set in a product. Assume that `s` maps bijectively to the first factor.
Then `s` is the graph of some function `f : β → γ`. -/
theorem exists_eq_mgraphOn_univ {s : Set (β × γ)} (hs₁ : Bijective (Prod.fst ∘ (Subtype.val : s → β × γ))) :
∃ f : β → γ, s = univ.graphOn f := by
simpa using
exists_range_eq_graphOn_univ hs₁.surjective fun a b h ↦
congr_arg (Prod.snd ∘ (Subtype.val : s → β × γ)) (hs₁.injective h)
