Metric

📁 Source: Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean

Statistics

Metric	Count
Definitions	0
Theorems `dist`, `edist`, `enorm`, `nnnorm`, `norm`, `dist`, `edist`, `enorm`, `infDist`, `infEDist`, `infEdist`, `infNndist`, `nndist`, `nnnorm`, `norm`, `exists_borelSpace_of_countablyGenerated_of_separatesPoints`, `exists_opensMeasurableSpace_of_countablySeparated`, `measurableSet_ball`, `measurableSet_closedBall`, `measurableSet_eball`, `measurable_dist`, `measurable_edist`, `measurable_edist_left`, `measurable_edist_right`, `measurable_enorm`, `measurable_infDist`, `measurable_infEDist`, `measurable_infEdist`, `measurable_infNndist`, `measurable_nndist`, `measurable_nnnorm`, `measurable_norm`, `tendsto_measure_cthickening`, `tendsto_measure_cthickening_of_isClosed`, `tendsto_measure_cthickening_of_isCompact`, `tendsto_measure_thickening`, `tendsto_measure_thickening_of_isClosed`	37
Total	37

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist` 📖	mathematical	`AEMeasurable`	`Real` `Real.measurableSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Continuous.aemeasurable2` `Real.borelSpace` `secondCountableTopologyEither_of_right` `continuous_dist`
`edist` 📖	mathematical	`AEMeasurable`	`ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.aemeasurable2` `ENNReal.borelSpace` `secondCountableTopologyEither_of_right` `continuous_edist`
`enorm` 📖	mathematical	`AEMeasurable`	`ENNReal` `ENNReal.measurableSpace` `ENorm.enorm` `ContinuousENorm.toENorm`	—	`Measurable.comp_aemeasurable` `measurable_enorm`
`nnnorm` 📖	mathematical	`AEMeasurable`	`NNReal` `NNReal.measurableSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Measurable.comp_aemeasurable` `measurable_nnnorm`
`norm` 📖	mathematical	`AEMeasurable`	`Real` `Real.measurableSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Measurable.comp_aemeasurable` `measurable_norm`

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist` 📖	mathematical	`Measurable`	`Real` `Real.measurableSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Continuous.measurable2` `Real.borelSpace` `secondCountableTopologyEither_of_right` `continuous_dist`
`edist` 📖	mathematical	`Measurable`	`ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.measurable2` `ENNReal.borelSpace` `secondCountableTopologyEither_of_right` `continuous_edist`
`enorm` 📖	mathematical	`Measurable`	`ENNReal` `ENNReal.measurableSpace` `ENorm.enorm` `ContinuousENorm.toENorm`	—	`comp` `measurable_enorm`
`infDist` 📖	mathematical	`Measurable`	`Real` `Real.measurableSpace` `Metric.infDist`	—	`comp` `measurable_infDist`
`infEDist` 📖	mathematical	`Measurable`	`ENNReal` `ENNReal.measurableSpace` `Metric.infEDist`	—	`comp` `measurable_infEDist`
`infEdist` 📖	mathematical	`Measurable`	`ENNReal` `ENNReal.measurableSpace` `Metric.infEDist`	—	`infEDist`
`infNndist` 📖	mathematical	`Measurable`	`NNReal` `NNReal.measurableSpace` `Metric.infNndist`	—	`comp` `measurable_infNndist`
`nndist` 📖	mathematical	`Measurable`	`NNReal` `NNReal.measurableSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`Continuous.measurable2` `NNReal.borelSpace` `secondCountableTopologyEither_of_right` `continuous_nndist`
`nnnorm` 📖	mathematical	`Measurable`	`NNReal` `NNReal.measurableSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`comp` `measurable_nnnorm`
`norm` 📖	mathematical	`Measurable`	`Real` `Real.measurableSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`comp` `measurable_norm`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_borelSpace_of_countablyGenerated_of_separatesPoints` 📖	mathematical	—	`SecondCountableTopology` `T4Space` `BorelSpace`	—	`MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated` `Topology.IsInducing.induced` `Homeomorph.secondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology` `TopologicalSpace.instSecondCountableTopologyForallOfCountable` `instCountableNat` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `Countable.LindelofSpace` `Bool.countable` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `TopologicalSpace.DiscreteTopology.metrizableSpace` `instDiscreteTopologyBool` `Homeomorph.t4Space` `instT4SpaceOfT1SpaceOfNormalSpace` `Subtype.t1Space` `instT1SpaceForall` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `CompletelyNormalSpace.toNormalSpace` `instCompletelyNormalSpaceSubtype` `CompletelyNormalSpace.of_regularSpace_secondCountableTopology` `instRegularSpaceForall` `TopologicalSpace.PseudoMetrizableSpace.regularSpace` `MeasurableEmbedding.borelSpace` `Subtype.borelSpace` `Pi.borelSpace` `Bool.borelSpace` `MeasurableEquiv.measurableEmbedding` `Homeomorph.isInducing`
`exists_opensMeasurableSpace_of_countablySeparated` 📖	mathematical	—	`SecondCountableTopology` `T4Space` `OpensMeasurableSpace`	—	`MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated` `exists_borelSpace_of_countablyGenerated_of_separatesPoints` `LE.le.trans` `Eq.le` `BorelSpace.measurable_eq`
`measurableSet_ball` 📖	mathematical	—	`MeasurableSet` `Metric.ball`	—	`IsOpen.measurableSet` `Metric.isOpen_ball`
`measurableSet_closedBall` 📖	mathematical	—	`MeasurableSet` `Metric.closedBall`	—	`IsClosed.measurableSet` `Metric.isClosed_closedBall`
`measurableSet_eball` 📖	mathematical	—	`MeasurableSet` `Metric.eball`	—	`IsOpen.measurableSet` `Metric.isOpen_eball`
`measurable_dist` 📖	mathematical	—	`Measurable` `Real` `Prod.instMeasurableSpace` `Real.measurableSpace` `Dist.dist` `PseudoMetricSpace.toDist`	—	`Continuous.measurable` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `Real.borelSpace` `continuous_dist`
`measurable_edist` 📖	mathematical	—	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.measurable` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `ENNReal.borelSpace` `continuous_edist`
`measurable_edist_left` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.measurable` `ENNReal.borelSpace` `Continuous.edist` `continuous_id'` `continuous_const`
`measurable_edist_right` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `EDist.edist` `PseudoEMetricSpace.toEDist`	—	`Continuous.measurable` `ENNReal.borelSpace` `Continuous.edist` `continuous_const` `continuous_id'`
`measurable_enorm` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `ENorm.enorm` `ContinuousENorm.toENorm`	—	`Continuous.measurable` `ENNReal.borelSpace` `continuous_enorm`
`measurable_infDist` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `Metric.infDist`	—	`Continuous.measurable` `Real.borelSpace` `Metric.continuous_infDist_pt`
`measurable_infEDist` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `Metric.infEDist`	—	`Continuous.measurable` `ENNReal.borelSpace` `Metric.continuous_infEDist`
`measurable_infEdist` 📖	mathematical	—	`Measurable` `ENNReal` `ENNReal.measurableSpace` `Metric.infEDist`	—	`measurable_infEDist`
`measurable_infNndist` 📖	mathematical	—	`Measurable` `NNReal` `NNReal.measurableSpace` `Metric.infNndist`	—	`Continuous.measurable` `NNReal.borelSpace` `Metric.continuous_infNndist_pt`
`measurable_nndist` 📖	mathematical	—	`Measurable` `NNReal` `Prod.instMeasurableSpace` `NNReal.measurableSpace` `NNDist.nndist` `PseudoMetricSpace.toNNDist`	—	`Continuous.measurable` `Prod.opensMeasurableSpace` `secondCountableTopologyEither_of_right` `NNReal.borelSpace` `continuous_nndist`
`measurable_nnnorm` 📖	mathematical	—	`Measurable` `NNReal` `NNReal.measurableSpace` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Continuous.measurable` `NNReal.borelSpace` `continuous_nnnorm`
`measurable_norm` 📖	mathematical	—	`Measurable` `Real` `Real.measurableSpace` `Norm.norm` `NormedAddCommGroup.toNorm`	—	`Continuous.measurable` `Real.borelSpace` `continuous_norm`
`tendsto_measure_cthickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.cthickening` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ENNReal.instTopologicalSpace` `closure` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.closure_eq_iInter_cthickening` `MeasureTheory.tendsto_measure_biInter_gt` `instOrderTopologyReal` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `IsClosed.nullMeasurableSet` `Metric.isClosed_cthickening` `Metric.cthickening_mono` `Filter.Tendsto.congr'` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `Metric.cthickening_of_nonpos` `tendsto_const_nhds` `nhdsLE_sup_nhdsGT` `Filter.Tendsto.sup`
`tendsto_measure_cthickening_of_isClosed` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.cthickening` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `ENNReal.instTopologicalSpace`	—	`IsClosed.closure_eq` `tendsto_measure_cthickening`
`tendsto_measure_cthickening_of_isCompact` 📖	mathematical	`IsCompact` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	`Filter.Tendsto` `Real` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.cthickening` `EMetricSpace.toPseudoEMetricSpace` `MetricSpace.toEMetricSpace` `nhds` `Real.pseudoMetricSpace` `Real.instZero` `ENNReal.instTopologicalSpace`	—	`tendsto_measure_cthickening_of_isClosed` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LT.lt.ne` `Bornology.IsBounded.measure_lt_top` `Bornology.IsBounded.cthickening` `IsCompact.isBounded` `IsCompact.isClosed` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`tendsto_measure_thickening` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.thickening` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.Ioi` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace` `closure` `PseudoEMetricSpace.toUniformSpace`	—	`Metric.closure_eq_iInter_thickening` `MeasureTheory.tendsto_measure_biInter_gt` `instOrderTopologyReal` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `IsOpen.nullMeasurableSet` `Metric.isOpen_thickening` `Metric.thickening_mono`
`tendsto_measure_thickening_of_isClosed` 📖	mathematical	`Real` `Real.instLT` `Real.instZero`	`Filter.Tendsto` `ENNReal` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Metric.thickening` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Set.Ioi` `Real.instPreorder` `nhds` `ENNReal.instTopologicalSpace`	—	`IsClosed.closure_eq` `tendsto_measure_thickening`

---

← Back to Index