Theorems · Theorem · order theory

Set.surjective_iff_surjective_of_iUnion_eq_univ

∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_5} {f : α → β} {U : ι → Set β},
  Set.iUnion U = Set.univ → (Function.Surjective f ↔ ∀ (i : ι), Function.Surjective ((U i).restrictPreimage f))

Defined in: Mathlib.Data.Set.Lattice.Image
Cited by: 2 results in Mathlib
Foundations: Depth 11 from the axioms · uses Classical.choice

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.Elemstatement · cited by 7,166
Set.preimagestatement · cited by 4,946
Set.univstatement and proof · cited by 3,945
Set.iUnionstatement and proof · cited by 2,483
Set.mem_iUnionproof · cited by 212
Set.restrictPreimagestatement and proof · cited by 84
Set.restrictPreimage_surjectiveproof · cited by 4

Cited by2

Results whose statement or proof uses this declaration.

Set.bijective_iff_bijective_of_iUnion_eq_univproof · cited by 0
TopologicalSpace.IsOpenCover.isHomeomorph_iff_restrictPreimageproof · cited by 0