Structures · Topology
T2Space
A T₂ space, also known as a Hausdorff space, is one in which for every
x ≠ y there exists disjoint open sets around x and y. This is
the most widely used of the separation axioms.
- Defined in
- Mathlib.Topology.Separation.Hausdorff
- Shape
- One type argument · adds t2
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances49
- Quiver.Hom
- Complex
- TopCat.carrier
- SeparationQuotient
- ContinuousLinearMap
- ENNReal
- CStarMatrix
- Unitization
- Matrix
- DomMulAct
- Units
- EReal
- RestrictedProduct
- TrivSqZeroExt
- UniformFun
- DomAddAct
- AddUnits
- ContinuousMapZero
- ContinuousAlternatingMap
- TopologicalSpace.NonemptyCompacts
- ContinuousMultilinearMap
- TopologicalSpace.Compacts
- PontryaginDual
- ContinuousAddMonoidHom
- ContinuousMonoidHom
- CategoryTheory.Aut
- WeakDual
- WeakSpace
- MeasureTheory.FiniteMeasure
- ConnectedComponents
- Ultrafilter
- MeasureTheory.ProbabilityMeasure
- Metric.Snowflaking
- StoneCech
- CategoryTheory.Monad.Algebra.A
- CompactCoherentification
- T2Quotient
- CompactConvergenceCLM
- PointwiseConvergenceCLM
- Subtype
- Prod
- ULift
- MulOpposite
- AddOpposite
- HasQuotient.Quotient
- ContinuousMap
- Sum
- Sigma
- Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by1,502
- HasSum.tsum_eq
- MeasureTheory.VectorMeasure.variation
- tendsto_nhds_unique
- HasFDerivAt.fderiv
- IsCompact.isClosed
- isClosed_eq
- HasFDerivWithinAt.fderivWithin
- HasProd.tprod_eq
- LinearMap.toContinuousLinearMap
- Topology.RelCWComplex.skeletonLT
- FiniteDimensional.complete
- Topology.RelCWComplex.skeleton
- IsCompact.measurableSet
- LinearEquiv.toContinuousLinearEquiv
- CompHausLike.of
- HasSum.unique
- tsum_mul_left
- MeasureTheory.VectorMeasure.of_union
- Filter.Tendsto.limUnder_eq
- LightProfinite.of
- MvPowerSeries.aeval
- Module.Basis.equivFunL
- LinearMap.continuous_of_finiteDimensional
- toEuclidean
- TopologicalSpace.NonemptyCompacts.toCloseds
- Summable.tsum_add
- MeasureTheory.VectorMeasure.enorm_measure_le_variation
- MeasureTheory.VectorMeasure.variation_restrict
- tendsto_nhds_unique_of_eventuallyEq
- MeasureTheory.VectorMeasure.variation_le_of_forall_enorm_le
- TopologicalSpace.Compacts.toCloseds
- CompHaus.of
- Profinite.of
- t2_separation
- PowerSeries.aeval
- Summable.hasSum_iff
- CompHausLike.ofHom
- CFC.sqrt_mul_sqrt_self
- ContinuousLinearMap.fderiv
- ContinuousLinearEquiv.ofFinrankEq
- MeasureTheory.VectorMeasure.of_disjoint_iUnion
- SmoothBumpCovering.toSmoothPartitionOfUnity
- Euclidean.ball
- MeasureTheory.VectorMeasure.variation.congr_simp
- Function.locallyFinsuppWithin.finiteSupport
- MeasureTheory.VectorMeasure.isSigmaSubadditiveSetFun_enorm
- DifferentiableAt.fderivWithin
- Function.LeftInverse.map_tsum
- cfcₙ_nnreal_eq_real
- Continuous.isClosedMap
Ancestors0
No ancestors.