Theorems · Theorem · order theory

Set.exists_equiv_range_eq_graphOn_univ

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

Line test for equivalences. Let f : α → β × γ be a homomorphism to a product of monoids. Assume that f is surjective on both factors and that the image of f intersects every "vertical line" {(b, c) | c : γ} and every "horizontal line" {(b, c) | b : β} at most once. Then the image of f is the graph of some equivalence f' : β ≃ γ.

Defined in

Mathlib.Data.Set.Prod

Cited by

0 results in Mathlib

Foundations

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