Theorems · Theorem · order theory
Set.sUnion_image
∀ {α : Type u_1} {β : Type u_2} (f : α → Set β) (s : Set α), ⋃₀ (f '' s) = ⋃ a ∈ s, f a- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 28 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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.imagestatement · cited by 5,609
- Set.iUnionstatement · cited by 2,483
- Set.sUnionstatement · cited by 392
- sSup_imageproof · cited by 36
Cited by28
Results whose statement or proof uses this declaration.
- Set.sUnion_eq_biUnionproof · cited by 51
- CategoryTheory.Subfunctor.iSup_objproof · cited by 23
- isClosed_sInterproof · cited by 10
- TopologicalSpace.isTopologicalBasis_of_subbasisproof · cited by 6
- Set.image_sUnionproof · cited by 5
- IsSemilinearSet.biUnionproof · cited by 5
- MeasureTheory.addContent_biUnionproof · cited by 2
- IsProperSemilinearSet.biUnionproof · cited by 2
- TopologicalSpace.vietoris.isTopologicalBasisproof · cited by 2
- isIrreducible_iff_sUnion_isClosedproof · cited by 2
- stableUnderSpecialization_iff_exists_sUnion_eqproof · cited by 1
- eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_openproof · cited by 1