Theorems · Theorem · general topology
SeparatedNhds.of_finset_finset
∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (s t : Finset X), Disjoint s t → SeparatedNhds ↑s ↑t- Defined in
- Mathlib.Topology.Separation.Hausdorff
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceT2Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Finsetstatement and proof · cited by 13,712
- SetLike.coestatement · cited by 8,199
- Disjointstatement and proof · cited by 2,201
- T2Spacestatement and proof · cited by 1,351
- Finset.finite_toSetproof · cited by 210
- SeparatedNhdsstatement · cited by 33
- Set.Finite.isCompactproof · cited by 10
- SeparatedNhds.of_isCompact_isCompactproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- SeparatedNhds.of_singleton_finsetproof · cited by 0
- SeparatedNhds.of_finiteproof · cited by 0