Theorems · Theorem
Set.mem_sUnion
∀ {α : Type u} {x : α} {S : Set (Set α)}, x ∈ ⋃₀ S ↔ ∃ t ∈ S, x ∈ t- Defined in
- Mathlib.Order.SetNotation
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
Cited by11
Results whose statement or proof uses this declaration.
- Bornology.sUnion_isVonNBounded_eq_univproof · cited by 3
- TopologicalSpace.IsTopologicalBasis.compactsproof · cited by 2
- exists_preirreducibleproof · cited by 2
- UniformOnFun.uniformContinuous_ofFun_toFunproof · cited by 1
- Partition.mem_iff_existsproof · cited by 1
- UniformOnFun.t2Space_of_coveringproof · cited by 1
- Partition.mem_iff_uniqueproof · cited by 1
- Setoid.eqv_classes_of_disjoint_unionproof · cited by 1
- UniformOnFun.uniformContinuous_restrict_toFunproof · cited by 0
- Setoid.sUnion_classesproof · cited by 0
- Setoid.IsPartition.sUnion_eq_univproof · cited by 0