Theorems · Theorem · order theory
Set.biUnion_of_singleton
∀ {α : Type u_1} (s : Set α), ⋃ x ∈ s, {x} = s- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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.iUnionstatement · cited by 2,483
- Set.extproof · cited by 2,266
Cited by43
Results whose statement or proof uses this declaration.
- Set.Countable.measurableSetproof · cited by 14
- Set.Finite.isCompactproof · cited by 10
- Set.biUnion_preimage_singletonproof · cited by 10
- Set.Countable.measure_zeroproof · cited by 9
- Set.Finite.isClosedproof · cited by 6
- ProbabilityTheory.indepSets_iff_singleton_indepSetsproof · cited by 5
- add_ball_zeroproof · cited by 4
- Filter.le_cofinite_iff_compl_singleton_memproof · cited by 4
- eq_bot_of_singletons_openproof · cited by 4
- Submodule.span_eq_iSup_of_singleton_spansproof · cited by 4
- IsCompact.finite_of_discreteproof · cited by 4
- IntermediateField.biSup_adjoin_simpleproof · cited by 4