Theorems · Theorem · order theory
Set.sUnion_singleton
∀ {α : Type u_1} (s : Set α), ⋃₀ {s} = s- Defined in
- Mathlib.Data.Set.Lattice
- Cited by
- 17 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.
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.sUnionstatement · cited by 392
- sSup_singletonproof · cited by 14
Cited by17
Results whose statement or proof uses this declaration.
- IsLinearSet.isSemilinearSetproof · cited by 10
- MeasureTheory.IsSetRing.isSetSemiringproof · cited by 6
- sUnion_memPartitionproof · cited by 3
- UniformOnFun.edist_continuousRestrict_of_singletonproof · cited by 2
- lipschitzOnWith_cfc_fun_of_subsetproof · cited by 2
- lipschitzOnWith_cfcₙ_fun_of_subsetproof · cited by 2
- closure_sUnion_irreducibleComponents_sdiff_singletonproof · cited by 2
- MeasurableSpace.measurableSet_generateFrom_memPartition_iffproof · cited by 1
- Topology.IsLower.isTopologicalSpace_basisproof · cited by 1
- UniformOnFun.uniformContinuous_ofFun_toFun_of_subsetproof · cited by 1
- IsProperLinearSet.isProperSemilinearSetproof · cited by 1
- isStationary_union_iffproof · cited by 0