Theorems · Theorem · general topology
TopologicalSpace.Opens.isCoatom_iff
∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {s : TopologicalSpace.Opens α},
IsCoatom s ↔ ∃ x, s = {x}.complin a T1Space, coatoms of TopologicalSpace.Opens α are precisely complements of singletons:
({x} : Closeds α).compl.
- Defined in
- Mathlib.Topology.Sets.Closeds
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceT1Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- TopologicalSpace.Opensstatement and proof · cited by 2,040
- T1Spacestatement and proof · cited by 275
- TopologicalSpace.Closedsstatement and proof · cited by 168
- Function.Bijective.injectiveproof · cited by 115
- IsCoatomstatement and proof · cited by 114
- TopologicalSpace.Closeds.complstatement and proof · cited by 10
- TopologicalSpace.Opens.complproof · cited by 8
- OrderIso.isAtom_iffproof · cited by 5
- isAtom_dual_iff_isCoatomproof · cited by 3
- TopologicalSpace.Opens.compl_complproof · cited by 3
- TopologicalSpace.Closeds.complOrderIsoproof · cited by 3
Cited by2
Results whose statement or proof uses this declaration.
- ContinuousMap.idealOf_compl_singleton_isMaximalproof · cited by 1
- ContinuousMap.setOfIdeal_eq_compl_singletonproof · cited by 1