Theorems · Theorem · general topology
compl_singleton_mem_nhds
∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, y ≠ x → {x}ᶜ ∈ nhds y- Defined in
- Mathlib.Topology.Separation.Basic
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 62 from the axioms · uses propext, Quot.sound
- Assumes
- TopologicalSpaceT1Space
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- Filterstatement · cited by 8,121
- nhdsstatement · cited by 5,554
- Compl.complstatement · cited by 2,925
- T1Spacestatement and proof · cited by 275
- compl_singleton_mem_nhds_iffproof · cited by 4
Cited by10
Results whose statement or proof uses this declaration.
- Valued.continuous_extensionproof · cited by 2
- eq_of_tendsto_nhdsproof · cited by 2
- summable_const_iffproof · cited by 1
- Complex.not_continuousAt_Gamma_neg_natproof · cited by 1
- deriv_riemannZeta_eq_neg_inv_sub_sq_addproof · cited by 1
- Complex.deriv_Gamma_add_oneproof · cited by 1
- UniformSpace.Completion.continuous_hatInvproof · cited by 1
- multipliable_const_iffproof · cited by 0
- deriv_riemannZeta_eq_neg_inv_sub_sq_mul_addproof · cited by 0
- UniformSpace.Completion.mul_hatInv_cancelproof · cited by 0