Theorems · Theorem · general topology
subsingleton_of_disjoint_isClopen
∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α},
(∀ (i : ι), (s i).Nonempty) → Pairwise (Function.onFun Disjoint s) → (∀ (i : ι), IsClopen (s i)) → Subsingleton ιIn a preconnected space, any disjoint family of non-empty clopen subsets has at most one element.
- Defined in
- Mathlib.Topology.Connected.Clopen
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
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
- TopologicalSpacestatement and proof · cited by 24,529
- Set.univproof · cited by 3,945
- Set.Nonemptystatement and proof · cited by 2,627
- Nontrivialproof · cited by 2,416
- Disjointstatement and proof · cited by 2,201
- Function.onFunstatement and proof · cited by 570
- Pairwisestatement and proof · cited by 516
- Set.univ_interproof · cited by 258
- IsClopenstatement and proof · cited by 189
- Set.Nonempty.ne_emptyproof · cited by 65
- PreconnectedSpacestatement and proof · cited by 64
Cited by2
Results whose statement or proof uses this declaration.
- subsingleton_of_disjoint_isClosed_iUnion_eq_univproof · cited by 1
- subsingleton_of_disjoint_isOpen_iUnion_eq_univproof · cited by 0