LevyProkhorovMetric

📁 Source: Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean

Statistics

Metric	Count
Definitions LevyProkhorov, delabOfMeasure, equiv, instPseudoEMetricSpaceMeasure, instPseudoMetricSpaceFiniteMeasure, instPseudoMetricSpaceProbabilityMeasure, levyProkhorovDist_metricSpace_probabilityMeasure, probabilityMeasureHomeomorph, toMeasure, toMeasureEquiv, homeomorph_probabilityMeasure_levyProkhorov, levyProkhorovDist, levyProkhorovEDist	13
Theorems integral_eq_integral_meas_le, integral_eq_integral_meas_le_of_hasFiniteIntegral, integral_le_of_levyProkhorovEDist_lt, continuous_equiv_probabilityMeasure, continuous_equiv_symm_probabilityMeasure, continuous_ofMeasure_probabilityMeasure, continuous_toMeasure_probabilityMeasure, dist_def, dist_finiteMeasure_def, dist_probabilityMeasure_def, edist_finiteMeasure_def, edist_measure_def, edist_probabilityMeasure_def, eq_convergenceInDistribution, le_convergenceInDistribution, toMeasureEquiv_apply, toMeasureEquiv_symm_apply_toMeasure, toMeasure_injective, toMeasure_add_pos_gt_mem_nhds, exists_measurable_partition_diam_le, instMetrizableSpaceProbabilityMeasure, instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace, left_measure_le_of_levyProkhorovEDist_lt, levyProkhorovDist_comm, levyProkhorovDist_le_of_forall_le, levyProkhorovDist_self, levyProkhorovDist_triangle, levyProkhorovEDist_comm, levyProkhorovEDist_le_max_measure_univ, levyProkhorovEDist_le_of_forall, levyProkhorovEDist_le_of_forall_add_pos_le, levyProkhorovEDist_le_of_forall_le, levyProkhorovEDist_lt_top, levyProkhorovEDist_ne_top, levyProkhorovEDist_self, levyProkhorovEDist_triangle, levyProkhorov_eq_convergenceInDistribution, levyProkhorov_le_convergenceInDistribution, meas_le_of_le_of_forall_le_meas_thickening_add, measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed, measure_le_measure_closure_of_levyProkhorovEDist_eq_zero, right_measure_le_of_levyProkhorovEDist_lt, tendsto_integral_meas_thickening_le	43
Total	56

MeasureTheory

Definitions

Name	Category	Theorems
LevyProkhorov 📖	CompData	17 math math: LevyProkhorov.dist_probabilityMeasure_def, LevyProkhorov.eq_convergenceInDistribution, LevyProkhorov.edist_measure_def, LevyProkhorov.continuous_equiv_symm_probabilityMeasure, LevyProkhorov.toMeasureEquiv_symm_apply_toMeasure, LevyProkhorov.continuous_equiv_probabilityMeasure, LevyProkhorov.edist_finiteMeasure_def, LevyProkhorov.dist_def, LevyProkhorov.edist_probabilityMeasure_def, LevyProkhorov.toMeasureEquiv_apply, LevyProkhorov.continuous_ofMeasure_probabilityMeasure, LevyProkhorov.le_convergenceInDistribution, levyProkhorov_le_convergenceInDistribution, LevyProkhorov.continuous_toMeasure_probabilityMeasure, LevyProkhorov.toMeasure_injective, LevyProkhorov.dist_finiteMeasure_def, levyProkhorov_eq_convergenceInDistribution
homeomorph_probabilityMeasure_levyProkhorov 📖	CompOp	—
levyProkhorovDist 📖	CompOp	7 math math: levyProkhorovDist_triangle, LevyProkhorov.dist_probabilityMeasure_def, levyProkhorovDist_comm, LevyProkhorov.dist_def, levyProkhorovDist_le_of_forall_le, levyProkhorovDist_self, LevyProkhorov.dist_finiteMeasure_def
levyProkhorovEDist 📖	CompOp	11 math math: levyProkhorovEDist_le_of_forall, levyProkhorovEDist_le_of_forall_add_pos_le, levyProkhorovEDist_comm, LevyProkhorov.edist_measure_def, LevyProkhorov.edist_finiteMeasure_def, levyProkhorovEDist_lt_top, levyProkhorovEDist_triangle, levyProkhorovEDist_le_max_measure_univ, LevyProkhorov.edist_probabilityMeasure_def, levyProkhorovEDist_self, levyProkhorovEDist_le_of_forall_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMetrizableSpaceProbabilityMeasure 📖	mathematical	—	TopologicalSpace.MetrizableSpace ProbabilityMeasure ProbabilityMeasure.instTopologicalSpace BorelSpace.opensMeasurable	—	Topology.IsEmbedding.metrizableSpace BorelSpace.opensMeasurable EMetricSpace.metrizableSpace Homeomorph.isEmbedding
instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace 📖	mathematical	—	TopologicalSpace.PseudoMetrizableSpace ProbabilityMeasure ProbabilityMeasure.instTopologicalSpace	—	Topology.IsInducing.pseudoMetrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace Homeomorph.isInducing
left_measure_le_of_levyProkhorovEDist_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder levyProkhorovEDist MeasurableSet	Preorder.toLE DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	—	sInf_lt_iff meas_le_of_le_of_forall_le_meas_thickening_add LT.lt.le
levyProkhorovDist_comm 📖	mathematical	—	levyProkhorovDist	—	levyProkhorovEDist_comm
levyProkhorovDist_le_of_forall_le 📖	mathematical	Real Real.instLE Real.instZero ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.ofReal	levyProkhorovDist	—	ENNReal.toReal_le_of_le_ofReal levyProkhorovEDist_le_of_forall_le ENNReal.ofReal_lt_ofReal_iff ENNReal.toReal_pos LT.lt.ne' LT.lt.bot_lt LT.lt.ne ENNReal.ofReal_toReal_eq_iff ENNReal.ofReal_toReal
levyProkhorovDist_self 📖	mathematical	—	levyProkhorovDist Real Real.instZero	—	levyProkhorovEDist_self
levyProkhorovDist_triangle 📖	mathematical	—	Real Real.instLE levyProkhorovDist Real.instAdd	—	LT.lt.ne levyProkhorovEDist_lt_top ENNReal.toReal_add ENNReal.toReal_mono ENNReal.add_ne_top levyProkhorovEDist_triangle
levyProkhorovEDist_comm 📖	mathematical	—	levyProkhorovEDist	—	—
levyProkhorovEDist_le_max_measure_univ 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder levyProkhorovEDist ENNReal.instMax DFunLike.coe Measure Set Measure.instFunLike Set.univ	—	sInf_le le_add_left ENNReal.instCanonicallyOrderedAdd Measure.instOuterMeasureClass
levyProkhorovEDist_le_of_forall 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	levyProkhorovEDist	—	levyProkhorovEDist_le_of_forall_add_pos_le ENNReal.lt_add_right LT.lt.ne Ne.lt_top
levyProkhorovEDist_le_of_forall_add_pos_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	levyProkhorovEDist	—	ENNReal.le_of_forall_pos_le_add add_top sInf_le add_assoc ENNReal.coe_pos ENNReal.coe_lt_top
levyProkhorovEDist_le_of_forall_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	levyProkhorovEDist	—	levyProkhorovEDist_le_of_forall Metric.subset_compl_thickening_compl_thickening_self LE.le.trans measure_mono Measure.instOuterMeasureClass prob_compl_eq_one_sub IsOpen.measurableSet Metric.isOpen_thickening IsClosed.measurableSet IsOpen.isClosed_compl add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Eq.le tsub_le_tsub_right ENNReal.instOrderedSub add_assoc tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE ENNReal.instCanonicallyOrderedAdd prob_le_one instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ENNReal.add_sub_cancel_left measure_ne_top IsZeroOrProbabilityMeasure.toIsFiniteMeasure add_comm le_refl
levyProkhorovEDist_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder levyProkhorovEDist Top.top instTopENNReal	—	LE.le.trans_lt levyProkhorovEDist_le_max_measure_univ
levyProkhorovEDist_ne_top 📖	—	—	—	—	LT.lt.ne levyProkhorovEDist_lt_top
levyProkhorovEDist_self 📖	mathematical	—	levyProkhorovEDist ENNReal instZeroENNReal	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd csInf_Ioo ENNReal.instDenselyOrdered ENNReal.zero_lt_top sInf_le_sInf le_add_right measure_mono Measure.instOuterMeasureClass Metric.self_subset_thickening ENNReal.toReal_pos LT.lt.ne' LT.lt.ne
levyProkhorovEDist_triangle 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder levyProkhorovEDist Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	top_add add_top levyProkhorovEDist_le_of_forall_add_pos_le Nat.instAtLeastTwoHAddOfNat ENNReal.div_pos LT.lt.ne' ENNReal.ofNat_ne_top ENNReal.lt_add_right add_assoc add_comm ENNReal.add_halves ENNReal.toReal_add ENNReal.Finiteness.add_ne_top ENNReal.div_ne_top ne_top_of_lt ne_of_gt Mathlib.Meta.Positivity.pos_of_isNat ENNReal.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo left_measure_le_of_levyProkhorovEDist_lt le_imp_le_of_le_of_le add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOpen.measurableSet Metric.isOpen_thickening le_refl measure_mono Measure.instOuterMeasureClass Metric.thickening_thickening_subset right_measure_le_of_levyProkhorovEDist_lt
levyProkhorov_eq_convergenceInDistribution 📖	mathematical	—	TopologicalSpace ProbabilityMeasure ProbabilityMeasure.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace TopologicalSpace.coinduced LevyProkhorov LevyProkhorov.toMeasure LevyProkhorov.instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace	—	LevyProkhorov.eq_convergenceInDistribution
levyProkhorov_le_convergenceInDistribution 📖	mathematical	—	TopologicalSpace ProbabilityMeasure Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced LevyProkhorov LevyProkhorov.toMeasure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace LevyProkhorov.instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace ProbabilityMeasure.instTopologicalSpace	—	LevyProkhorov.le_convergenceInDistribution
meas_le_of_le_of_forall_le_meas_thickening_add 📖	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	—	—	add_top LE.le.trans add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add measure_mono Measure.instOuterMeasureClass Metric.thickening_mono ENNReal.toReal_mono
measure_eq_measure_of_levyProkhorovEDist_eq_zero_of_isClosed 📖	mathematical	levyProkhorovEDist ENNReal instZeroENNReal Real Real.instLT Real.instZero	DFunLike.coe Measure Set Measure.instFunLike	—	le_antisymm LE.le.trans measure_le_measure_closure_of_levyProkhorovEDist_eq_zero IsClosed.measurableSet le_of_eq IsClosed.closure_eq levyProkhorovEDist_comm
measure_le_measure_closure_of_levyProkhorovEDist_eq_zero 📖	mathematical	levyProkhorovEDist ENNReal instZeroENNReal MeasurableSet Real Real.instLT Real.instZero	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace	—	tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within tendsto_nhdsWithin_of_tendsto_nhds ContinuousAt.tendsto ENNReal.continuousAt_toReal ENNReal.zero_ne_top Filter.mp_mem Ioo_mem_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero Filter.univ_mem' ENNReal.toReal_pos LT.lt.ne' ne_top_of_lt Filter.Tendsto.comp tendsto_measure_thickening Filter.Tendsto.add ENNReal.instContinuousAdd Filter.tendsto_id ge_of_tendsto ENNReal.nhdsGT_zero_neBot add_zero self_mem_nhdsWithin left_measure_le_of_levyProkhorovEDist_lt
right_measure_le_of_levyProkhorovEDist_lt 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder levyProkhorovEDist MeasurableSet	Preorder.toLE DFunLike.coe Measure Set Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Metric.thickening ENNReal.toReal	—	sInf_lt_iff meas_le_of_le_of_forall_le_meas_thickening_add LT.lt.le
tendsto_integral_meas_thickening_le 📖	mathematical	—	Filter.Tendsto Real integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureSpace.toMeasurableSpace Real.measureSpace Measure.restrict MeasureSpace.volume Measure.real ProbabilityMeasure.toMeasure Metric.thickening PseudoMetricSpace.toPseudoEMetricSpace setOf Real.instLE DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike nhdsWithin Real.instZero Set.Ioi Real.instPreorder nhds	—	tendsto_integral_filter_of_dominated_convergence TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Filter.Eventually.of_forall Measurable.aestronglyMeasurable instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Measurable.comp ENNReal.measurable_toNNReal Antitone.measurable ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid measure_mono Measure.instOuterMeasureClass Metric.thickening_subset_of_subset LE.le.trans NNReal.abs_eq ENNReal.toReal_mono ENNReal.one_ne_top prob_le_one instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityMeasure.instIsProbabilityMeasureToMeasure Measure.restrict_apply Set.univ_inter integrable_const Filter.Tendsto.comp ENNReal.tendsto_toNNReal measure_ne_top IsZeroOrProbabilityMeasure.toIsFiniteMeasure tendsto_measure_thickening_of_isClosed Real.zero_lt_one isClosed_le continuous_const BoundedContinuousFunction.continuous

MeasureTheory.BoundedContinuousFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral_eq_integral_meas_le 📖	mathematical	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero Real.instZero DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Norm.norm BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.Measure.real setOf	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq_integral_meas_le_of_hasFiniteIntegral BoundedContinuousFunction.integrable instSecondCountableTopologyReal Real.borelSpace
integral_eq_integral_meas_le_of_hasFiniteIntegral 📖	mathematical	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero Real.instZero DFunLike.coe BoundedContinuousFunction Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike MeasureTheory.HasFiniteIntegral ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Norm.norm BoundedContinuousFunction.instNorm MeasureTheory.Measure.real setOf	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Integrable.integral_eq_integral_Ioc_meas_le Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace Continuous.measurable BoundedContinuousFunction.continuous Filter.Eventually.of_forall BoundedContinuousFunction.apply_le_norm
integral_le_of_levyProkhorovEDist_lt 📖	mathematical	Real Real.instLT Real.instZero ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.levyProkhorovEDist PseudoMetricSpace.toPseudoEMetricSpace ENNReal.ofReal Filter.EventuallyLE Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero DFunLike.coe BoundedContinuousFunction UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace BoundedContinuousFunction.instFunLike	MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instAdd MeasureTheory.MeasureSpace.toMeasurableSpace Real.measureSpace MeasureTheory.Measure.restrict MeasureTheory.MeasureSpace.volume Set.Ioc Real.instPreorder Norm.norm BoundedContinuousFunction.instNorm NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing MeasureTheory.Measure.real Metric.thickening setOf Real.instMul	—	MeasureTheory.Measure.instOuterMeasureClass integral_eq_integral_meas_le ENNReal.toReal_add MeasureTheory.measure_ne_top ENNReal.ofReal_ne_top ENNReal.toReal_ofReal LT.lt.le ENNReal.toReal_mono ENNReal.add_ne_top MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt Continuous.measurable Real.borelSpace BoundedContinuousFunction.continuous measurableSet_Ici BorelSpace.opensMeasurable instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid MeasureTheory.Measure.integrableOn_of_bounded LT.lt.ne measure_Ioc_lt_top ConditionallyCompleteLinearOrder.toCompactIccSpace instOrderTopologyReal Real.locallyFinite_volume Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal Measurable.ennreal_toReal Antitone.measurable ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology MeasureTheory.measure_mono LE.le.trans Filter.Eventually.of_forall abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono MeasureTheory.measureReal_nonneg MeasureTheory.measureReal_mono Set.subset_univ Metric.thickening_subset_of_subset le_trans MeasureTheory.setIntegral_mono IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule Real.instIsStrictOrderedRing MeasureTheory.Integrable.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal MeasureTheory.integrable_const Real.isFiniteMeasure_restrict_Ioc MeasureTheory.integral_add MeasureTheory.integral_const Real.instCompleteSpace MeasureTheory.measureReal_restrict_apply Set.univ_inter Real.volume_real_Ioc sub_zero sup_of_le_left IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Eq.le mul_comm

MeasureTheory.LevyProkhorov

Definitions

Name	Category	Theorems
delabOfMeasure 📖	CompOp	—
equiv 📖	CompOp	—
instPseudoEMetricSpaceMeasure 📖	CompOp	1 math math: edist_measure_def
instPseudoMetricSpaceFiniteMeasure 📖	CompOp	2 math math: edist_finiteMeasure_def, dist_finiteMeasure_def
instPseudoMetricSpaceProbabilityMeasure 📖	CompOp	11 math math: dist_probabilityMeasure_def, eq_convergenceInDistribution, continuous_equiv_symm_probabilityMeasure, continuous_equiv_probabilityMeasure, dist_def, edist_probabilityMeasure_def, continuous_ofMeasure_probabilityMeasure, le_convergenceInDistribution, MeasureTheory.levyProkhorov_le_convergenceInDistribution, continuous_toMeasure_probabilityMeasure, MeasureTheory.levyProkhorov_eq_convergenceInDistribution
levyProkhorovDist_metricSpace_probabilityMeasure 📖	CompOp	—
probabilityMeasureHomeomorph 📖	CompOp	—
toMeasure 📖	CompOp	15 math math: dist_probabilityMeasure_def, eq_convergenceInDistribution, edist_measure_def, toMeasureEquiv_symm_apply_toMeasure, continuous_equiv_probabilityMeasure, edist_finiteMeasure_def, dist_def, edist_probabilityMeasure_def, toMeasureEquiv_apply, le_convergenceInDistribution, MeasureTheory.levyProkhorov_le_convergenceInDistribution, continuous_toMeasure_probabilityMeasure, toMeasure_injective, dist_finiteMeasure_def, MeasureTheory.levyProkhorov_eq_convergenceInDistribution
toMeasureEquiv 📖	CompOp	2 math math: toMeasureEquiv_symm_apply_toMeasure, toMeasureEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_equiv_probabilityMeasure 📖	mathematical	—	Continuous MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace MeasureTheory.ProbabilityMeasure.instTopologicalSpace toMeasure	—	continuous_toMeasure_probabilityMeasure
continuous_equiv_symm_probabilityMeasure 📖	mathematical	—	Continuous MeasureTheory.ProbabilityMeasure MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace ofMeasure	—	continuous_ofMeasure_probabilityMeasure
continuous_ofMeasure_probabilityMeasure 📖	mathematical	—	Continuous MeasureTheory.ProbabilityMeasure MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace ofMeasure	—	continuous_iff_continuousAt Metric.continuousAt_iff' Nat.instAtLeastTwoHAddOfNat lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true ENNReal.ofReal_pos MeasureTheory.SeparableSpace.exists_measurable_partition_diam_le MeasureTheory.tendsto_measure_biUnion_Ici_zero_of_pairwise_disjoint MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure MeasureTheory.ProbabilityMeasure.instIsProbabilityMeasureToMeasure MeasurableSet.nullMeasurableSet isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Set.iUnion_congr_Prop Set.compl_Iio Set.biUnion_compl_eq_of_pairwise_disjoint_of_iUnion_eq_univ le_rfl Set.Finite.finite_subsets Set.finite_Iio Metric.isOpen_thickening MeasureTheory.ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds Filter.mp_mem Finset.iInter_mem_sets Filter.univ_mem' lt_of_le_of_lt dist_comm dist_probabilityMeasure_def MeasureTheory.levyProkhorovDist_le_of_forall_le le_of_not_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg CancelDenoms.mul_subst Set.nonempty_of_mem Set.mem_inter Metric.self_subset_thickening HasSubset.Subset.trans Set.instIsTransSubset Set.union_subset_union Set.compl_iUnion Set.disjoint_left Metric.mem_thickening_iff dist_triangle add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add LT.lt.le LE.le.trans Metric.dist_le_diam_of_mem Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt CancelDenoms.add_subst MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measure_union_le ENNReal.instIsOrderedAddMonoid Set.iInter_congr_Prop Metric.thickening_iUnion add_assoc ENNReal.ofReal_add two_mul ENNReal.ofReal_le_ofReal
continuous_toMeasure_probabilityMeasure 📖	mathematical	—	Continuous MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace MeasureTheory.ProbabilityMeasure.instTopologicalSpace toMeasure	—	SeqContinuous.continuous FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral MeasureTheory.ProbabilityMeasure.instIsProbabilityMeasureToMeasure MeasureTheory.integral_zero Filter.limsup_const Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat lt_of_le_of_ne norm_nonneg le_of_forall_pos_le_add LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing AddGroup.existsAddOfLE contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Filter.limsup_le_of_le le_trans MeasureTheory.integral_nonneg IsStrictOrderedModule.toIsOrderedModule IsStrictOrderedRing.toIsStrictOrderedModule instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal le_rfl exists_seq_strictAnti_tendsto instOrderTopologyReal instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_iff_dist_tendsto_zero tendsto_nhdsWithin_iff add_zero Filter.Eventually.of_forall Set.mem_Ioi lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.sub_neg_of_lt dist_nonneg Filter.Tendsto.comp MeasureTheory.tendsto_integral_meas_thickening_le Real.volume_Ioc sub_zero ofReal_norm Nat.instAtLeastTwoHAddOfNat Iio_mem_nhds Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt CancelDenoms.sub_subst CancelDenoms.add_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Meta.NormNum.isNat_lt_true Filter.mp_mem half_pos mul_pos inv_pos Filter.univ_mem' MeasureTheory.BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure Right.add_pos_of_nonneg_of_pos covariant_swap_add_of_covariant_add ENNReal.ofReal_add le_of_lt ENNReal.add_lt_add_of_le_of_lt MeasureTheory.levyProkhorovEDist_ne_top le_of_eq dist_probabilityMeasure_def MeasureTheory.levyProkhorovDist.eq_1 ENNReal.ofReal_toReal ENNReal.ofReal_pos MeasureTheory.Measure.instOuterMeasureClass le_imp_le_of_le_of_le le_refl add_le_add_left MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le add_assoc mul_comm add_le_add_right mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono lt_of_le_of_ne' Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isNat_eq_false Mathlib.Tactic.FieldSimp.NF.cons_ne_zero ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add
dist_def 📖	mathematical	—	Dist.dist MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure PseudoMetricSpace.toDist instPseudoMetricSpaceProbabilityMeasure MeasureTheory.levyProkhorovDist MeasureTheory.ProbabilityMeasure.toMeasure toMeasure	—	dist_probabilityMeasure_def
dist_finiteMeasure_def 📖	mathematical	—	Dist.dist MeasureTheory.LevyProkhorov MeasureTheory.FiniteMeasure PseudoMetricSpace.toDist instPseudoMetricSpaceFiniteMeasure MeasureTheory.levyProkhorovDist MeasureTheory.FiniteMeasure.toMeasure toMeasure	—	—
dist_probabilityMeasure_def 📖	mathematical	—	Dist.dist MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure PseudoMetricSpace.toDist instPseudoMetricSpaceProbabilityMeasure MeasureTheory.levyProkhorovDist MeasureTheory.ProbabilityMeasure.toMeasure toMeasure	—	—
edist_finiteMeasure_def 📖	mathematical	—	EDist.edist MeasureTheory.LevyProkhorov MeasureTheory.FiniteMeasure PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace instPseudoMetricSpaceFiniteMeasure MeasureTheory.levyProkhorovEDist MeasureTheory.FiniteMeasure.toMeasure toMeasure	—	—
edist_measure_def 📖	mathematical	—	EDist.edist MeasureTheory.LevyProkhorov MeasureTheory.Measure PseudoEMetricSpace.toEDist instPseudoEMetricSpaceMeasure MeasureTheory.levyProkhorovEDist toMeasure	—	—
edist_probabilityMeasure_def 📖	mathematical	—	EDist.edist MeasureTheory.LevyProkhorov MeasureTheory.ProbabilityMeasure PseudoEMetricSpace.toEDist PseudoMetricSpace.toPseudoEMetricSpace instPseudoMetricSpaceProbabilityMeasure MeasureTheory.levyProkhorovEDist MeasureTheory.ProbabilityMeasure.toMeasure toMeasure	—	—
eq_convergenceInDistribution 📖	mathematical	—	TopologicalSpace MeasureTheory.ProbabilityMeasure MeasureTheory.ProbabilityMeasure.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace TopologicalSpace.coinduced MeasureTheory.LevyProkhorov toMeasure instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace	—	LE.le.antisymm' le_convergenceInDistribution IsOpen.preimage continuous_ofMeasure_probabilityMeasure
le_convergenceInDistribution 📖	mathematical	—	TopologicalSpace MeasureTheory.ProbabilityMeasure Preorder.toLE PartialOrder.toPreorder TopologicalSpace.instPartialOrder TopologicalSpace.coinduced MeasureTheory.LevyProkhorov toMeasure UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace instPseudoMetricSpaceProbabilityMeasure PseudoMetricSpace.toPseudoEMetricSpace MeasureTheory.ProbabilityMeasure.instTopologicalSpace	—	Continuous.coinduced_le continuous_toMeasure_probabilityMeasure
toMeasureEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv MeasureTheory.LevyProkhorov EquivLike.toFunLike Equiv.instEquivLike toMeasureEquiv toMeasure	—	—
toMeasureEquiv_symm_apply_toMeasure 📖	mathematical	—	toMeasure DFunLike.coe Equiv MeasureTheory.LevyProkhorov EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toMeasureEquiv	—	—
toMeasure_injective 📖	mathematical	—	MeasureTheory.LevyProkhorov toMeasure	—	—

MeasureTheory.ProbabilityMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasure_add_pos_gt_mem_nhds 📖	mathematical	IsOpen UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set MeasureTheory.ProbabilityMeasure Filter Filter.instMembership nhds instTopologicalSpace setOf DFunLike.coe MeasureTheory.Measure MeasureTheory.Measure.instFunLike toMeasure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Filter.Eventually.of_forall lt_of_lt_of_le le_add_self ENNReal.instCanonicallyOrderedAdd add_top MeasureTheory.IsZeroOrProbabilityMeasure.toIsFiniteMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure instIsProbabilityMeasureToMeasure ENNReal.sub_lt_self MeasureTheory.measure_ne_top LT.lt.ne le_liminf_measure_open_of_tendsto instHasOuterApproxClosedOfPseudoMetrizableSpace PseudoEMetricSpace.pseudoMetrizableSpace Filter.tendsto_id Filter.mp_mem Filter.gt_mem_sets_of_limsInf_gt Filter.isBounded_ge_of_bot Filter.univ_mem' tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid ENNReal.instOrderedSub ENNReal.add_lt_add_right

MeasureTheory.SeparableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_measurable_partition_diam_le 📖	mathematical	Real Real.instLT Real.instZero	MeasurableSet Bornology.IsBounded PseudoMetricSpace.toBornology Real.instLE Metric.diam Set.iUnion Set.univ Pairwise Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	isEmpty_or_nonempty MeasurableSet.empty Bornology.isBounded_empty Metric.diam_empty LT.lt.le Unique.instSubsingleton disjoint_of_subsingleton TopologicalSpace.exists_dense_seq Nat.instAtLeastTwoHAddOfNat half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing MeasurableSet.disjointed measurableSet_ball Bornology.IsBounded.subset Metric.isBounded_ball disjointed_subset LE.le.trans Metric.diam_mono Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Metric.diam_ball Metric.ball_eq_ball' DenseRange.iUnion_uniformity_ball Metric.dist_mem_uniformity iUnion_disjointed disjoint_disjointed

---

← Back to Index