English
If a function f: α → β × γ is surjective on the first factor and satisfies a vertical-line condition, then there exists f' : β → γ with range f = graphOn f' over the universal set.
Русский
Если f: α → β × γ суръективна по первой координате и удовлетворяет условию вертикальной прямой, существует f' : β → γ такой, что range f = graphOn f' над единичной областью.
LaTeX
$$$\exists f' : β \to γ, \ operatorname{range}(f) = \operatorname{graphOn}(f', \mathsf{univ})$$$
Lean4
/-- **Vertical line test** for functions.
Let `f : α → β × γ` be a function to a product. Assume that `f` is surjective on the first factor
and that the image of `f` intersects every "vertical line" `{(b, c) | c : γ}` at most once.
Then the image of `f` is the graph of some monoid homomorphism `f' : β → γ`. -/
theorem exists_range_eq_graphOn_univ {f : α → β × γ} (hf₁ : Surjective (Prod.fst ∘ f))
(hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ f' : β → γ, range f = univ.graphOn f' :=
by
refine ⟨fun h ↦ (f (hf₁ h).choose).snd, ?_⟩
ext x
simp only [mem_range, comp_apply, mem_graphOn, mem_univ, true_and]
refine ⟨?_, fun hi ↦ ⟨(hf₁ x.1).choose, Prod.ext (hf₁ x.1).choose_spec hi⟩⟩
rintro ⟨g, rfl⟩
exact hf _ _ (hf₁ (f g).1).choose_spec
