English
For f : G →* H and x ∈ G × H, x ∈ f.graph if and only if f(x_1) = x_2.
Русский
Для f : G →* H и x ∈ G × H верно: x ∈ граф f тогда, когда f(x_1) = x_2.
LaTeX
$$$x \\in f.graph \\iff f(x_1) = x_2$, where $x = (x_1, x_2) \\in G \\times H$.$$
Lean4
/-- **Vertical line test** for group homomorphisms.
Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`. -/
@[to_additive /-- **Vertical line test** for group homomorphisms.
Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`. -/
]
theorem exists_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
(hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) : ∃ f' : H →* I, range f = f'.graph := by
simpa [SetLike.ext_iff] using exists_mrange_eq_mgraph hf₁ hf
