Theorems · Theorem · order theory
Set.sUnion_eq_iUnion
∀ {α : Type u_1} {s : Set (Set α)}, ⋃₀ s = ⋃ i, ↑i- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 26 results in Mathlib
- Foundations
- Depth 18 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.Elemstatement · cited by 7,166
- Set.iUnionstatement · cited by 2,483
- Set.sUnionstatement and proof · cited by 392
- Subtype.range_coeproof · cited by 98
Cited by26
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.setIntegral_densityProcessproof · cited by 4
- TopologicalSpace.IsTopologicalBasis.isOpenMap_iffproof · cited by 4
- iInf_sUnionproof · cited by 3
- Set.pairwise_sUnionproof · cited by 3
- TopologicalSpace.IsTopologicalBasis.open_eq_iUnionproof · cited by 3
- iSupIndep_sUnion_of_directedproof · cited by 1
- algebraicIndependent_sUnion_of_directedproof · cited by 1
- orthonormal_sUnion_of_directedproof · cited by 1
- IsSemilinearSet.exists_fg_eq_subtypeValproof · cited by 1
- iSup_sUnionproof · cited by 1
- isCompact_generateFrom'proof · cited by 1
- Set.directedOn_sUnionproof · cited by 1