Structures · Topology
T1Space
A T₁ space, also known as a Fréchet space, is a topological space
where every singleton set is closed. Equivalently, for every pair
x ≠ y, there is an open set containing x and not y.
- Defined in
- Mathlib.Topology.Separation.Basic
- Shape
- One type argument · adds t1
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Concrete types that are instances13
- DomMulAct
- RestrictedProduct
- DomAddAct
- ContinuousMapZero
- Matrix.SpecialLinearGroup
- OnePoint
- MaximalSpectrum
- CofiniteTopology
- Subtype
- Prod
- ULift
- HasQuotient.Quotient
- ContinuousMap
How is a type an instance?
Loading the hierarchy index…
Assumed by279
- isClosed_singleton
- isOpen_compl_singleton
- isOpen_ne
- T1Space.t1
- Filter.Tendsto.eventually_ne
- compl_singleton_mem_nhds
- nhdsWithin_insert_of_ne
- closure_singleton
- Continuous.isOpen_support
- eventually_ne_nhds
- ContinuousLinearMap.isClosed_ker
- Set.Finite.isDiscrete
- Set.Finite.isClosed
- ContinuousAt.eventually_ne
- fderivWithin_congr_set'
- hasFDerivWithinAt_congr_set'
- Ne.nhdsWithin_compl_singleton
- Submodule.IsTopCompl.isClosed'
- Specializes.eq
- ker_nhds
- HasCompactSupport.eq_zero_or_locallyCompactSpace_of_addGroup
- compl_singleton_mem_nhds_iff
- isClosedMap_const
- specializes_iff_eq
- gauge_pos
- Filter.tendsto_mul_iff_of_ne_zero
- eventually_ne_nhdsWithin
- HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group
- continuousWithinAt_update_of_ne
- gaugeRescaleHomeomorph
- Topology.IsEmbedding.t1Space
- Submodule.IsTopCompl.isClosed
- nhdsNE_of_nhdsNE_sdiff_finite
- continuousWithinAt_insert
- pure_le_nhds_iff
- Set.Subsingleton.isClosed
- HasFDerivWithinAt.of_finite
- codiscreteWithin_iff_locallyFiniteComplementWithin
- isOpen_singleton_of_finite_mem_nhds
- Homeomorph.t1Space
- biInter_basis_nhds
- eventuallyEq_insert
- supportDiscreteWithin_iff_locallyFiniteWithin
- tendsto_indicator_const_iff_forall_eventually
- Set.Infinite.of_accPt
- differentiableWithinAt_congr_set'
- HasFDerivWithinAt.singleton
- Units.isClosedEmbedding_embedProduct
- TopologicalSpace.IsTopologicalBasis.exists_mem_of_ne
- nhdsSet_le_iff
Ancestors0
No ancestors.