Theorems · Theorem · order theory

Set.exists_range_eq_graphOn_univ

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β × γ},
  Function.Surjective (Prod.fst ∘ f) →
    (∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', Set.range f = Set.graphOn f' Set.univ

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' : β → γ.

Defined in

Mathlib.Data.Set.Prod

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Classical.choice, Quot.sound