Theorems · Theorem · order theory
Set.biUnion_univ
∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ Set.univ, s x = ⋃ x, s x- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 11 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.
Cites4
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.univstatement · cited by 3,945
- Set.iUnionstatement · cited by 2,483
- iSup_univproof · cited by 8
Cited by11
Results whose statement or proof uses this declaration.
- IsPreconnected.iUnion_of_reflTransGenproof · cited by 2
- finprod_mem_iUnionproof · cited by 1
- finsum_mem_iUnionproof · cited by 1
- Set.accumulate_subset_iUnionproof · cited by 1
- AddSubmonoid.FG.piproof · cited by 1
- Submonoid.FG.piproof · cited by 1
- TopologicalSpace.Compacts.compactSpace_iffproof · cited by 0
- TopologicalSpace.NonemptyCompacts.compactSpace_iffproof · cited by 0
- MulAction.isClosedMap_quotientproof · cited by 0
- AddAction.isClosedMap_quotientproof · cited by 0
- ENNReal.tsum_biUnionproof · cited by 0