Theorems · Theorem · general topology
isOpen_compl_singleton
∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X}, IsOpen {x}ᶜ- Defined in
- Mathlib.Topology.Separation.Basic
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- TopologicalSpaceT1Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- TopologicalSpacestatement and proof · cited by 24,529
- Compl.complstatement · cited by 2,925
- IsOpenstatement · cited by 2,400
- T1Spacestatement and proof · cited by 275
- IsClosed.isOpen_complproof · cited by 126
Cited by27
Results whose statement or proof uses this declaration.
- isOpen_neproof · cited by 22
- Filter.Tendsto.eventually_neproof · cited by 11
- Real.continuousAt_logproof · cited by 7
- compl_singleton_mem_nhds_iffproof · cited by 4
- isInducing_stoneCechUnitproof · cited by 4
- Dense.sdiff_singletonproof · cited by 2
- Metric.PiNatEmbed.injective_distDenseSeqproof · cited by 2
- UpperHalfPlane.contMDiff_denom_zpowproof · cited by 2
- HurwitzZeta.differentiableAt_cosZetaproof · cited by 2
- HurwitzZeta.differentiableAt_update_of_residueproof · cited by 2
- derivedSet_closureproof · cited by 1
- ChartedSpace.t1Spaceproof · cited by 1