Theorems · Theorem · general topology
SeparatedNhds.disjoint_closure_left
∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint (closure s) t- Cited by
- 4 results in Mathlib
- Foundations
- Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
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.
- Setstatement and proof · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- IsOpenproof · cited by 2,400
- Disjointstatement and proof · cited by 2,201
- closurestatement and proof · cited by 1,254
- closure_monoproof · cited by 133
- Disjoint.monoproof · cited by 69
- SeparatedNhdsstatement and proof · cited by 33
- Disjoint.closure_leftproof · cited by 6
Cited by4
Results whose statement or proof uses this declaration.
- SeparatedNhds.disjoint_closure_rightproof · cited by 2
- IsClosed.HasSeparatingCoverproof · cited by 0
- Topology.IsInducing.sumElim_of_separatedNhdsproof · cited by 0
- Topology.IsEmbedding.sumElim_of_separatedNhdsproof · cited by 0