Structures · Topology
SecondCountableTopology
A second-countable space is one with a countable basis.
- Defined in
- Mathlib.Topology.Bases
- Shape
- One type argument · adds is_open_generated_countable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances25
- Real
- TopCat.carrier
- NNReal
- ContinuousLinearMap
- ENNReal
- DomMulAct
- WithLp
- EReal
- DomAddAct
- TopologicalSpace.NonemptyCompacts
- TopologicalSpace.Compacts
- PiLp
- UpperHalfPlane
- Metric.Snowflaking
- GromovHausdorff.GHSpace
- TopologicalSpace.Opens.CompleteCopy
- Subtype
- Prod
- OrderDual
- Set.Elem
- HasQuotient.Quotient
- ContinuousMap
- WithTop
- Sum
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by699
- Measurable.aestronglyMeasurable
- AEMeasurable.aestronglyMeasurable
- StieltjesFunction.measure
- Measurable.stronglyMeasurable
- aestronglyMeasurable_id
- measurableSet_le
- measurableSet_lt
- LightProfinite.of
- TopologicalSpace.countableBasis
- SchwartzMap.toTemperedDistributionCLM
- Measurable.iSup
- ProbabilityTheory.HasGaussianLaw.memLp_two
- IsUnifLocDoublingMeasure.vitaliFamily
- VitaliFamily.limRatioMeas
- ProbabilityTheory.IsGaussian.integrable_id
- BoundedVariationOn.vectorMeasure
- SchwartzMap.integrable
- TopologicalSpace.isBasis_countableBasis
- ProbabilityTheory.IsGaussian.memLp_two_id
- TopologicalSpace.exists_countable_basis
- MeasureTheory.Measure.addHaarMeasure_unique
- TopologicalSpace.isOpen_iUnion_countable
- BoundedContinuousFunction.integrable
- MeasureTheory.LocallyIntegrable.aestronglyMeasurable
- StieltjesFunction.measure_Iic
- StieltjesFunction.measure_Ioc
- MeasureTheory.Measure.isAddLeftInvariant_eq_smul
- MeasureTheory.Measure.ext_of_charFunDual
- StieltjesFunction.measure_Icc
- Measurable.tsum
- TopologicalSpace.countable_countableBasis
- SchwartzMap.toTemperedDistributionCLM_apply_apply
- MeasureTheory.Measure.ext_of_charFun
- ProbabilityTheory.HasGaussianLaw.integrable
- MeasureTheory.AEEqFun.compMeasurable
- MeasureTheory.AEEqFun.comp₂Measurable
- Topology.IsEmbedding.secondCountableTopology
- BoundedVariationOn.vectorMeasure_Icc
- borel_eq_generateFrom_Iio
- MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
- Measurable.iInf
- StieltjesFunction.measure_singleton
- nullMeasurableSet_lt
- StieltjesFunction.measure_univ
- exists_partition_approximatesLinearOn_of_hasFDerivWithinAt
- MeasureTheory.StronglyAdapted.isStronglyProgressive_of_discrete
- MeasureTheory.measure_null_of_locally_null
- stronglyMeasurable_id
- VitaliFamily.measure_le_of_frequently_le
- Module.Basis.map_addHaar
Ancestors0
No ancestors.