Structures · Topology
T0Space
A T₀ space, also known as a Kolmogorov space, is a topological space such that for every pair
x ≠ y, there is an open set containing one but not the other. We formulate the definition in terms
of the Inseparable relation.
- Defined in
- Mathlib.Topology.Separation.Basic
- Shape
- One type argument · adds t0
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by6
Concrete types that are instances25
- TopCat.carrier
- SeparationQuotient
- UniformSpace.Completion
- IsDedekindDomain.HeightOneSpectrum.adicCompletion
- DomMulAct
- WithLp
- RestrictedProduct
- DomAddAct
- ContinuousMapZero
- TopologicalSpace.NonemptyCompacts
- PrimeSpectrum
- TopologicalSpace.Compacts
- PiLp
- TopologicalSpace.Closeds
- OnePoint
- Metric.Snowflaking
- TopologicalSpace.Opens.CompleteCopy
- UniformSpaceCat.carrier
- CpltSepUniformSpace.α
- Subtype
- Prod
- ULift
- ContinuousMap
- Set
- Filter
How is a type an instance?
Loading the hierarchy index…
Assumed by194
- Inseparable.eq
- UniformSpace.Completion.extension_coe
- IsUniformEmbedding.isClosedEmbedding
- IsComplete.isClosed
- Topology.IsInducing.isEmbedding
- ContinuousLinearMap.extend_eq
- ContinuousLinearMap.fromCompletion
- Topology.IsEmbedding.t0Space
- MeasureTheory.diracProbaEquiv
- ContinuousLinearMap.extend
- NormedAddGroupHom.extension
- TopologicalSpace.Closeds.isUniformEmbedding_singleton
- AddMonoidHom.extension
- IsGenericPoint.eq
- Summable.tsum_prod
- Isometry.completion_extension
- exists_isOpen_xor_mem
- irreducibleSetEquivPoints
- inseparable_iff_eq
- CpltSepUniformSpace.of
- UniformSpace.Completion.extension_unique
- ContinuousLinearMap.extend_unique
- specializationOrder
- Topology.IsInducing.injective
- UniformSpace.Completion.isUniformEmbedding_coe
- IsUniformInducing.isUniformEmbedding
- isClosed_of_spaced_out
- AddCircle.isAddQuotientCoveringMap_zsmul
- CauchyFilter.separated_pureCauchy_injective
- IsCompactOperator.restrict'
- isUniformEmbedding_iff_isUniformInducing
- SeparationQuotient.lift'
- genericPoints.equiv
- tsum_primes_pow_eq
- AbstractCompletion.extension₂_coe_coe
- UniformSpace.Completion.coe_injective
- minimal_nonempty_closed_eq_singleton
- UniformSpace.Completion.coe_inj
- Summable.tsum_sigma
- genericPoints.component_injective
- Isometry.extensionHom_coe
- Summable.tsum_comm
- SemiNormedGrp.completion.lift
- nhds_injective
- totallySeparatedSpace_of_t0_of_basis_clopen
- minimal_nonempty_closed_subsingleton
- AddMonoidHom.extension_coe
- isClosed_range_of_spaced_out
- AddCircle.isAddQuotientCoveringMap_nsmul
- UniformSpace.Completion.extensionHom
Ancestors0
No ancestors.