Structures · Topology
PolishSpace
A Polish space is a topological space with second countable topology, that can be endowed
with a metric for which it is complete.
To endow a Polish space with a complete metric space structure, do
letI := upgradeIsCompletelyMetrizable α.
- Defined in
- Mathlib.Topology.MetricSpace.Polish
- Shape
- One type argument
Extends2
Extended by1
Concrete types that are instances2
- ENNReal
- EReal
How is a type an instance?
Loading the hierarchy index…
Assumed by52
- MeasureTheory.analyticSet_range_of_polishSpace
- IsClosed.polishSpace
- MeasurableSet.image_of_continuousOn_injOn
- MeasurableSet.isClopenable
- MeasurableSet.image_of_monotoneOn
- MeasureTheory.Measure.IsAddLeftInvariant.addQuotientMeasureEqMeasurePreimage_of_set
- IsOpen.isClopenable
- IsClosed.analyticSet
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addInvariantMeasure_quotient
- MeasureTheory.Measure.IsMulLeftInvariant.quotientMeasureEqMeasurePreimage_of_set
- Measurable.exists_continuous
- Topology.IsClosedEmbedding.polishSpace
- PolishSpace.exists_polishSpace_forall_le
- MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient
- IsOpen.polishSpace
- IsOpen.analyticSet_image
- ContinuousOn.measurableEmbedding
- IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_AddHaarMeasure
- MeasurableSet.image_of_monotoneOn_of_continuousOn
- Continuous.map_eq_borel
- PolishSpace.exists_nat_nat_continuous_surjective
- IsClosed.measurableSet_image_of_continuousOn_injOn
- MeasureTheory.measurableSet_range_of_continuous_injective
- IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure
- PolishSpace.IsClopenable.iUnion
- Equiv.polishSpace_induced
- IsClosed.isClopenable
- MeasurableSet.analyticSet
- Continuous.measurableEmbedding
- MeasureTheory.ProbabilityMeasure.tendsto_of_tight_of_separatesPoints
- CosetSpace.borelSpace
- QuotientGroup.borelSpace
- QuotientAddGroup.borelSpace
- MeasureTheory.leftInvariantIsQuotientMeasureEqMeasurePreimage
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.vaddInvariantMeasure_quotient
- MeasureTheory.AddQuotientMeasureEqMeasurePreimage.addHaarMeasure_quotient
- standardBorel_of_polish
- IsClosed.exists_nat_bool_injection_of_not_countable
- MeasurableSet.image_of_antitoneOn
- MeasureTheory.isClopenable_iff_measurableSet
- PolishSpace.toIsCompletelyMetrizableSpace
- Quotient.borelSpace
- MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish
- MeasureTheory.AnalyticSet.preimage
- PolishSpace.toSecondCountableTopology
- MeasureTheory.QuotientMeasureEqMeasurePreimage.haarMeasure_quotient
- Continuous.map_borel_eq
- AddCosetSpace.borelSpace
- MeasureTheory.leftInvariantIsAddQuotientMeasureEqMeasurePreimage
- IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure