Structures · Topology
TopologicalSpace
A topology on X.
- Defined in
- Mathlib.Topology.Defs.Basic
- Shape
- One type argument · adds IsOpen, isOpen_univ, isOpen_inter, isOpen_sUnion
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by2
Forgetful instances
Concrete types that are instances100
- Int
- Nat
- Bool
- TopCat.carrier
- SeparationQuotient
- NNReal
- ContinuousLinearMap
- ZMod
- ENNReal
- CStarMatrix
- CommRingCat.carrier
- Matrix
- ENat
- DomMulAct
- Units
- WithLp
- EReal
- RestrictedProduct
- TrivSqZeroExt
- ModuleCat.carrier
- UniformFun
- AbstractCompletion.space
- UniformOnFun
- Localization
- DomAddAct
- AddUnits
- ContinuousMapZero
- ContinuousAlternatingMap
- NumberField.InfiniteAdeleRing
- TopologicalSpace.NonemptyCompacts
- IsDedekindDomain.FiniteAdeleRing
- ContinuousLinearMapWOT
- NumberField.AdeleRing
- TopCommRingCat.α
- Ordinal
- Empty
- Matrix.SpecialLinearGroup
- PEmpty
- AlgEquiv
- PrimeSpectrum
- WithIdealFilter
- SignType
- ContinuousMultilinearMap
- SchwartzMap
- TopologicalSpace.Compacts
- PiLp
- PontryaginDual
- Circle
- TestFunction
- ContDiffMapSupportedIn
- UniformConvergenceCLM
- SingularManifold.M
- ContinuousAddMonoidHom
- ContinuousMonoidHom
- WithTopology
- CategoryTheory.Aut
- WeakDual
- OnePoint
- TangentSpace
- WeakSpace
- WeakBilin
- TopRep.V
- Complex.UnitClosedDisc
- VectorBundleCore.Fiber
- Path
- List.Vector
- MaximalSpectrum
- Field.absoluteGaloisGroup
- Complex.UnitDisc
- UpperHalfPlane
- MeasureTheory.FiniteMeasure
- ConnectedComponents
- ZerothHomotopy
- Ultrafilter
- Bundle.Pullback
- Topology.WithUpper
- Topology.WithLower
- CategoryTheory.ObjectProperty.FullSubcategory.obj
- FirstOrder.Language.Theory.CompleteType
- MeasureTheory.ProbabilityMeasure
- Metric.Snowflaking
- TopologicalSpace.Opens.CompleteCopy
- ProjectiveSpectrum
- Topology.WithScott
- Topology.WithUpperSet
- Topology.WithLawson
- Topology.WithLowerSet
- EuclideanHalfSpace
- EuclideanQuadrant
- Bundle.TotalSpace
- StoneCech
- ModelPi
- Order.Fill
- TopCat.Presheaf.EtaleSpace
- ModelProd
- PreStoneCech
- Topology.ContinuousMapGeneratedBy
- CategoryTheory.Monad.Algebra.A
- CompactCoherentification
- T2Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by28,282
- nhds
- IsOpen
- nhdsWithin
- ContinuousOn
- MeasureTheory.Integrable
- IsCompact
- closure
- tsum
- PartialHomeomorph.toPartialEquiv
- MeasureTheory.AEEqFun
- OpenPartialHomeomorph.toPartialHomeomorph
- Summable
- MeasureTheory.AEStronglyMeasurable
- OpenPartialHomeomorph.toFun'
- interior
- ContinuousLinearMap.comp
- ContinuousAt
- deriv
- DifferentiableAt
- FormalMultilinearSeries
- TangentSpace
- MeasureTheory.IntegrableOn
- ContinuousLinearMap.toLinearMap
- HasSum
- ContinuousWithinAt
- HasDerivAt
- IsOpen.mem_nhds
- OpenPartialHomeomorph.symm
- StrongDual
- MeasureTheory.MemLp
- DifferentiableWithinAt
- ContinuousLinearEquiv.toContinuousLinearMap
- DifferentiableOn
- ModelWithCorners.prod
- fderiv
- MeasureTheory.AEEqFun.cast
- ModelWithCorners.toFun'
- Continuous.comp
- ContinuousLinearEquiv.symm
- Homeomorph.symm
- MeasureTheory.StronglyMeasurable
- Dense
- fderivWithin
- HasFDerivWithinAt
- HasFDerivAt
- HasDerivWithinAt
- tendsto_const_nhds
- IntervalIntegrable
- Continuous.continuousOn
- subset_closure