Hausdorff

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

Statistics

Metric	Count
Definitions hausdorffMeasure, mkMetric, mkMetric', IsMetric, mkMetric, mkMetric', pre, «termμH[_]»	8
Theorems hausdorffMeasure_preimage_le, le_hausdorffMeasure_image, hausdorffMeasure_image_le, hausdorffMeasure_image, hausdorffMeasure_preimage, map_hausdorffMeasure, hausdorffMeasure_image, hausdorffMeasure_preimage, map_hausdorffMeasure, measurePreserving_hausdorffMeasure, hausdorffMeasure_image_le, hausdorffMeasure_image_le, hausdorffMeasure_apply, hausdorffMeasure_le_liminf_sum, hausdorffMeasure_le_liminf_tsum, hausdorffMeasure_le_one_of_subsingleton, hausdorffMeasure_mono, hausdorffMeasure_smul₀, hausdorffMeasure_zero_or_top, hausdorffMeasure_zero_singleton, le_hausdorffMeasure, le_mkMetric, mkMetric'_toOuterMeasure, mkMetric_apply, mkMetric_le_liminf_sum, mkMetric_le_liminf_tsum, mkMetric_mono, mkMetric_mono_smul, mkMetric_toOuterMeasure, mkMetric_top, noAtoms_hausdorff, one_le_hausdorffMeasure_zero_of_nonempty, borel_le_caratheodory, finset_iUnion_of_pairwise_separated, le_caratheodory, coe_mkMetric, isometryEquiv_comap_mkMetric, isometryEquiv_map_mkMetric, isometry_comap_mkMetric, isometry_map_mkMetric, le_mkMetric, eq_iSup_nat, le_pre, mono_pre, mono_pre_nat, pre_le, tendsto_pre, tendsto_pre_nat, trim_pre, mkMetric'_isMetric, mkMetric_mono, mkMetric_mono_smul, mkMetric_nnreal_smul, mkMetric_smul, mkMetric_top, trim_mkMetric, hausdorffMeasure_affineSegment, hausdorffMeasure_homothety_image, hausdorffMeasure_homothety_preimage, hausdorffMeasure_lineMap_image, hausdorffMeasure_measurePreserving_funUnique, hausdorffMeasure_measurePreserving_piFinTwo, hausdorffMeasure_orthogonalProjection_le, hausdorffMeasure_pi_real, hausdorffMeasure_prod_real, hausdorffMeasure_real, hausdorffMeasure_segment, hausdorffMeasure_smul, hausdorffMeasure_smul_right_image, hausdorffMeasure_vadd, instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd, instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite, instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul, instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite, isAddHaarMeasure_hausdorffMeasure	75
Total	83

AntilipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_preimage_le 📖	mathematical	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.preimage Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal ENNReal.ofNNReal	—	eq_or_ne Set.eq_empty_or_nonempty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.instCanonicallyOrderedAdd Set.Subsingleton.anti Set.subsingleton_univ subsingleton Set.subset_univ Set.subsingleton_iff_singleton eq_or_lt_of_le ENNReal.rpow_zero one_mul MeasureTheory.Measure.hausdorffMeasure_zero_singleton MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty MeasureTheory.NoAtoms.measure_singleton MeasureTheory.Measure.noAtoms_hausdorff MeasureTheory.Measure.hausdorffMeasure_apply ENNReal.mul_iSup iSup_congr_Prop ENNReal.mul_iInf_of_ne iInf_congr_Prop iSup₂_le le_iSup₂_of_le LT.lt.ne' le_iInf₂ le_iInf Set.preimage_mono iInf₂_le_of_le Set.preimage_iUnion iInf_le_of_le LE.le.trans ediam_preimage_le ENNReal.mul_le_of_le_div' ENNReal.tsum_le_tsum iSup_le_iff Set.nonempty_of_nonempty_preimage ciSup_pos ENNReal.mul_rpow_of_nonneg ENNReal.rpow_le_rpow
le_hausdorffMeasure_image 📖	mathematical	AntilipschitzWith EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal ENNReal.ofNNReal Set.image	—	MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.subset_preimage_image hausdorffMeasure_preimage_le

HolderOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_image_le 📖	mathematical	HolderOnWith EMetricSpace.toPseudoEMetricSpace NNReal Preorder.toLT PartialOrder.toPreorder instPartialOrderNNReal instZeroNNReal Real Real.instLE Real.instZero	ENNReal Preorder.toLE ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.image Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal ENNReal.ofNNReal Real.instMul NNReal.toReal	—	LE.le.eq_or_lt zero_le NNReal.instCanonicallyOrderedAdd Set.eq_empty_or_nonempty Set.image_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MulZeroClass.mul_zero ENNReal.instCanonicallyOrderedAdd MulZeroClass.zero_mul ediam_image_le Set.subsingleton_iff_singleton Set.mem_image_of_mem eq_or_lt_of_le ENNReal.rpow_zero MeasureTheory.Measure.hausdorffMeasure.congr_simp one_mul MeasureTheory.Measure.hausdorffMeasure_zero_singleton MeasureTheory.Measure.one_le_hausdorffMeasure_zero_of_nonempty MeasureTheory.NoAtoms.measure_singleton MeasureTheory.Measure.noAtoms_hausdorff LT.lt.ne' MeasureTheory.Measure.hausdorffMeasure_apply ENNReal.mul_iSup iSup_congr_Prop ENNReal.mul_iInf_of_ne iInf_congr_Prop iSup_le ENNReal.tendsto_const_mul_rpow_nhds_zero_of_pos ENNReal.coe_ne_top Filter.HasBasis.eventually_iff ENNReal.nhds_zero_basis_Iic Filter.Tendsto.eventually gt_mem_nhds ENNReal.instOrderTopology le_iSup₂_of_le iInf₂_mono' Set.image_iUnion Set.iUnion_inter Mathlib.Tactic.GCongr.rel_imp_rel Set.instIsTransSubset subset_refl Set.instReflSubset Set.image_mono Set.inter_subset_inter Set.inter_self iInf_mono' LE.le.trans ediam_image_inter_le LT.lt.le ENNReal.tsum_le_tsum Set.Nonempty.mono Set.inter_subset_left ciSup_pos ENNReal.rpow_mul ENNReal.mul_rpow_of_nonneg ENNReal.rpow_le_rpow

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_image 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.image	—	IsScalarTower.right MeasureTheory.OuterMeasure.isometry_comap_mkMetric ENNReal.monotone_rpow_of_nonneg
hausdorffMeasure_preimage 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.preimage Set.instInter Set.range	—	hausdorffMeasure_image Set.image_preimage_eq_inter_range
map_hausdorffMeasure 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	MeasureTheory.Measure.map MeasureTheory.Measure.hausdorffMeasure MeasureTheory.Measure.restrict Set.range	—	MeasureTheory.Measure.ext MeasureTheory.Measure.map_apply Continuous.measurable BorelSpace.opensMeasurable continuous MeasureTheory.Measure.restrict_apply hausdorffMeasure_preimage

IsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_image 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.image IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike instEquivLike	—	Isometry.hausdorffMeasure_image isometry surjective
hausdorffMeasure_preimage 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.preimage IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike instEquivLike	—	image_symm hausdorffMeasure_image
map_hausdorffMeasure 📖	mathematical	—	MeasureTheory.Measure.map DFunLike.coe IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike instEquivLike MeasureTheory.Measure.hausdorffMeasure	—	Isometry.map_hausdorffMeasure isometry surjective Function.Surjective.range_eq MeasureTheory.Measure.restrict_univ
measurePreserving_hausdorffMeasure 📖	mathematical	—	MeasureTheory.MeasurePreserving DFunLike.coe IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike instEquivLike MeasureTheory.Measure.hausdorffMeasure	—	Continuous.measurable BorelSpace.opensMeasurable continuous map_hausdorffMeasure

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_image_le 📖	mathematical	LipschitzOnWith EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.image Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal ENNReal.ofNNReal	—	MeasureTheory.Measure.hausdorffMeasure.congr_simp one_mul HolderOnWith.hausdorffMeasure_image_le holderOnWith zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_image_le 📖	mathematical	LipschitzWith EMetricSpace.toPseudoEMetricSpace Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike MeasureTheory.Measure.hausdorffMeasure Set.image Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instPowReal ENNReal.ofNNReal	—	LipschitzOnWith.hausdorffMeasure_image_le lipschitzOnWith

MeasureTheory

Definitions

Name	Category	Theorems
«termμH[_]» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_affineSegment 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace Real Real.instOne affineSegment Real.instRing Real.partialOrder NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	affineSegment.eq_1 Real.borelSpace hausdorffMeasure_lineMap_image hausdorffMeasure_real Real.volume_Icc sub_zero ENNReal.ofReal_one Algebra.algebraMap_eq_smul_one edist_nndist
hausdorffMeasure_homothety_image 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace Set.image AffineMap CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNReal.instPowReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	IsometryEquiv.hausdorffMeasure_image Set.image_smul Measure.hausdorffMeasure_smul₀ NormedSpace.toNormSMulClass Set.image_image
hausdorffMeasure_homothety_preimage 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace Set.preimage AffineMap CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField NormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.homothety NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNReal.instPowReal NNReal.instInv NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing	—	AffineEquiv.image_symm AffineEquiv.coe_homothetyUnitsMulHom_apply_symm hausdorffMeasure_homothety_image IsUnit.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Units.isUnit Units.val_inv_eq_inv_val Units.val_mk0 nnnorm_inv
hausdorffMeasure_lineMap_image 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace Real Real.instOne Set.image AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace AffineMap.instFunLike AffineMap.lineMap NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNDist.nndist PseudoMetricSpace.toNNDist Real.measurableSpace Real.metricSpace Real.borelSpace	—	Real.borelSpace IsometryEquiv.hausdorffMeasure_image hausdorffMeasure_smul_right_image nndist_eq_nnnorm_vsub' Set.image_image
hausdorffMeasure_measurePreserving_funUnique 📖	mathematical	—	MeasurePreserving MeasurableSpace.pi DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.funUnique Measure.hausdorffMeasure emetricSpacePi Unique.fintype Pi.borelSpace_of_subsingleton Unique.instSubsingleton UniformSpace.toTopologicalSpace	—	IsometryEquiv.measurePreserving_hausdorffMeasure Pi.borelSpace_of_subsingleton Unique.instSubsingleton
hausdorffMeasure_measurePreserving_piFinTwo 📖	mathematical	BorelSpace UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace SecondCountableTopology	MeasurePreserving MeasurableSpace.pi Prod.instMeasurableSpace DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.piFinTwo Measure.hausdorffMeasure emetricSpacePi Fin.fintype Pi.borelSpace instCountableFin Prod.emetricSpaceMax Prod.borelSpace secondCountableTopologyEither_of_right	—	IsometryEquiv.measurePreserving_hausdorffMeasure Pi.borelSpace instCountableFin Prod.borelSpace secondCountableTopologyEither_of_right
hausdorffMeasure_orthogonalProjection_le 📖	mathematical	Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace SetLike.instMembership Submodule.setLike Subtype.instMeasurableSpace Set Measure.instFunLike Measure.hausdorffMeasure instEMetricSpaceSubtype MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Subtype.borelSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Set.image ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceSubtype Submodule.addCommMonoid Submodule.module ContinuousLinearMap.funLike Submodule.orthogonalProjection	—	Subtype.borelSpace ENNReal.one_rpow one_mul LipschitzWith.hausdorffMeasure_image_le Submodule.lipschitzWith_orthogonalProjection
hausdorffMeasure_pi_real 📖	mathematical	—	Measure.hausdorffMeasure emetricSpacePi Real MetricSpace.toEMetricSpace Real.metricSpace MeasurableSpace.pi Real.measurableSpace Pi.borelSpace Finite.to_countable Finite.of_fintype UniformSpace.toTopologicalSpace instSecondCountableTopologyReal Real.borelSpace Real.instNatCast Fintype.card MeasureSpace.volume MeasureSpace.pi Real.measureSpace	—	Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal Real.borelSpace Measure.pi_eq_generateFrom Real.borel_eq_generateFrom_Ioo_rat Real.isPiSystem_Ioo_rat Real.locallyFinite_volume Finset.prod_congr le_antisymm covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsStrictOrderedRing LT.lt.le one_div Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Metric.ediam_pi_le_of_le add_div Real.ediam_Icc add_sub_add_left_eq_sub add_sub_cancel_left ENNReal.ofReal_div_of_pos Nat.cast_pos Real.instIsOrderedRing Real.instNontrivial ENNReal.ofReal_one ENNReal.ofReal_natCast Nat.floor_lt_ceil_of_lt_of_pos mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono sub_lt_sub_right IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd Nat.cast_pos' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat mul_pos IsStrictOrderedRing.toPosMulStrictMono add_le_add_right div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE Nat.floor_le mul_nonneg IsOrderedRing.toPosMulMono sub_nonneg le_of_lt 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.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Nat.lt_floor_add_one Measure.hausdorffMeasure_le_liminf_sum Filter.liminf_le_liminf Filter.mp_mem Filter.univ_mem' Finset.sum_le_sum ENNReal.instIsOrderedAddMonoid ENNReal.rpow_natCast pow_le_pow_left' IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid covariant_swap_mul_of_covariant_mul Filter.isBounded_ge_of_bot Filter.isCobounded_ge_of_top Finset.sum_congr div_eq_mul_inv Finset.sum_const Fintype.card_pi Fintype.card_fin nsmul_eq_mul Nat.cast_prod Finset.prod_mul_distrib Finset.prod_const Real.volume_Ioo Filter.Tendsto.liminf_eq ENNReal.instOrderTopology Filter.atTop_neBot ENNReal.tendsto_finset_prod_of_ne_top Filter.Tendsto.congr' Filter.Tendsto.comp Continuous.tendsto ENNReal.continuous_ofReal tendsto_nat_ceil_mul_div_atTop instOrderTopologyReal tendsto_natCast_atTop_atTop Real.instArchimedean Measure.le_hausdorffMeasure ENNReal.coe_lt_top Real.volume_pi_le_diam_pow volume_pi_pi Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Measure.le_iff'
hausdorffMeasure_prod_real 📖	mathematical	—	Measure.hausdorffMeasure Real Prod.emetricSpaceMax MetricSpace.toEMetricSpace Real.metricSpace Prod.instMeasurableSpace Real.measurableSpace Prod.borelSpace UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat MeasureSpace.volume Measure.prod.measureSpace Real.measureSpace	—	Prod.borelSpace Real.borelSpace secondCountableTopologyEither_of_right instSecondCountableTopologyReal Nat.instAtLeastTwoHAddOfNat MeasurePreserving.map_eq volume_preserving_piFinTwo Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume FiniteDimensional.rclike_to_real SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace instIsTopologicalAddGroupReal TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Pi.borelSpace instCountableFin hausdorffMeasure_measurePreserving_piFinTwo Finite.to_countable Finite.of_fintype hausdorffMeasure_pi_real Fintype.card_fin Nat.cast_two
hausdorffMeasure_real 📖	mathematical	—	Measure.hausdorffMeasure Real MetricSpace.toEMetricSpace Real.metricSpace Real.measurableSpace Real.borelSpace Real.instOne MeasureSpace.volume Real.measureSpace	—	Real.borelSpace MeasurePreserving.map_eq volume_preserving_funUnique Pi.borelSpace_of_subsingleton Unique.instSubsingleton hausdorffMeasure_measurePreserving_funUnique Pi.borelSpace Finite.to_countable Finite.of_fintype instSecondCountableTopologyReal hausdorffMeasure_pi_real Fintype.card_unit Nat.cast_one
hausdorffMeasure_segment 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real Real.instOne segment Real.semiring Real.partialOrder ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction NormedSpace.toModule Real.normedField EDist.edist PseudoEMetricSpace.toEDist EMetricSpace.toPseudoEMetricSpace	—	affineSegment_eq_segment Real.instIsOrderedRing hausdorffMeasure_affineSegment
hausdorffMeasure_smul 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure Set.smulSet	—	Isometry.hausdorffMeasure_image IsIsometricSMul.isometry_smul
hausdorffMeasure_smul_right_image 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real Real.instOne Set.image SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Real.measurableSpace Real.metricSpace Real.borelSpace	—	Real.borelSpace eq_or_ne Set.eq_empty_or_nonempty Set.image_congr smul_zero Set.image_empty measure_empty Measure.instOuterMeasureClass nnnorm_zero hausdorffMeasure_real Set.Nonempty.image_const NoAtoms.measure_singleton Measure.noAtoms_hausdorff one_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike zero_smul norm_ne_zero_iff AddMonoidHomClass.isometry_of_norm DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass norm_smul NormedSpace.toNormSMulClass norm_inv norm_norm inv_mul_cancel₀ mul_one LinearMap.id_apply Set.image_smul Measure.hausdorffMeasure_smul₀ zero_le_one nnnorm_norm NNReal.rpow_one Isometry.hausdorffMeasure_image zero_le_one' Set.image_image SMulCommClass.smul_comm smulCommClass_self inv_smul_smul₀
hausdorffMeasure_vadd 📖	mathematical	Real Real.instLE Real.instZero HVAdd.hVAdd instHVAdd	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.hausdorffMeasure Set.vaddSet	—	Isometry.hausdorffMeasure_image IsIsometricVAdd.isometry_vadd
instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd 📖	mathematical	—	Measure.IsAddLeftInvariant AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.hausdorffMeasure	—	IsometryEquiv.map_hausdorffMeasure
instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite 📖	mathematical	—	Measure.IsAddRightInvariant AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.hausdorffMeasure	—	IsometryEquiv.map_hausdorffMeasure
instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul 📖	mathematical	—	Measure.IsMulLeftInvariant MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.hausdorffMeasure	—	IsometryEquiv.map_hausdorffMeasure
instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite 📖	mathematical	—	Measure.IsMulRightInvariant MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.hausdorffMeasure	—	IsometryEquiv.map_hausdorffMeasure
isAddHaarMeasure_hausdorffMeasure 📖	mathematical	—	Measure.IsAddHaarMeasure NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Measure.hausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Real Real.instNatCast Module.finrank Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField	—	RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.topologicalAddGroup instIsTopologicalAddGroupReal instContinuousSMulForall IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Real.instCompleteSpace TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace Pi.t2Space FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.rclike_to_real Module.finrank_fintype_fun_eq_card commRing_strongRankCondition Real.instNontrivial Fintype.card_fin Pi.borelSpace instCountableFin instSecondCountableTopologyReal Real.borelSpace Finite.to_countable hausdorffMeasure_pi_real IsCompact.measure_lt_top Measure.instIsFiniteMeasureOnCompactsForallVolumeOfSigmaFinite Measure.IsAddHaarMeasure.sigmaFinite instIsAddHaarMeasureVolume SeparableWeaklyLocallyCompactAddGroup.sigmaCompactSpace TopologicalSpace.SecondCountableTopology.to_separableSpace instWeaklyLocallyCompactSpaceOfLocallyCompactSpace locallyCompact_of_proper instProperSpaceReal Measure.IsAddHaarMeasure.toIsFiniteMeasureOnCompacts IsCompact.image ContinuousLinearEquiv.continuous ContinuousLinearEquiv.symm_image_image lt_of_le_of_lt RingHomIsometric.ids LipschitzWith.hausdorffMeasure_image_le ContinuousLinearEquiv.lipschitz Real.instIsOrderedRing ENNReal.rpow_natCast ENNReal.mul_lt_top ENNReal.pow_lt_top ENNReal.coe_lt_top instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd NormedAddGroup.to_isIsometricVAdd_left IsOpen.measure_pos Measure.instIsOpenPosMeasureForallVolumeOfSigmaFinite Measure.IsAddHaarMeasure.toIsOpenPosMeasure ContinuousLinearEquiv.isOpenMap LT.lt.ne' ENNReal.mul_pos_iff lt_of_lt_of_le

MeasureTheory.Measure

Definitions

Name	Category	Theorems
hausdorffMeasure 📖	CompOp	47 math math: MeasureTheory.hausdorffMeasure_segment, hausdorffMeasure_zero_singleton, AntilipschitzWith.hausdorffMeasure_preimage_le, MeasureTheory.isAddHaarMeasure_hausdorffMeasure, Isometry.hausdorffMeasure_image, MeasureTheory.instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul, hausdorffMeasure_le_liminf_sum, MeasureTheory.hausdorffMeasure_measurePreserving_piFinTwo, hausdorffMeasure_mono, noAtoms_hausdorff, IsometryEquiv.hausdorffMeasure_image, MeasureTheory.hausdorffMeasure_pi_real, hausdorffMeasure_smul₀, MeasureTheory.instIsAddRightInvariantHausdorffMeasureOfIsIsometricVAddAddOpposite, MeasureTheory.hausdorffMeasure_prod_real, MeasureTheory.hausdorffMeasure_lineMap_image, IsometryEquiv.map_hausdorffMeasure, dimH_eq_iInf, AntilipschitzWith.le_hausdorffMeasure_image, hausdorffMeasure_zero_or_top, IsometryEquiv.hausdorffMeasure_preimage, le_hausdorffMeasure, MeasureTheory.hausdorffMeasure_homothety_image, IsometryEquiv.measurePreserving_hausdorffMeasure, one_le_hausdorffMeasure_zero_of_nonempty, MeasureTheory.instIsMulRightInvariantHausdorffMeasureOfIsIsometricSMulMulOpposite, MeasureTheory.hausdorffMeasure_vadd, hausdorffMeasure_le_liminf_tsum, MeasureTheory.hausdorffMeasure_measurePreserving_funUnique, Isometry.hausdorffMeasure_preimage, MeasureTheory.hausdorffMeasure_smul_right_image, MeasureTheory.hausdorffMeasure_real, hausdorffMeasure_of_dimH_lt, Isometry.map_hausdorffMeasure, hausdorffMeasure_apply, MeasureTheory.hausdorffMeasure_orthogonalProjection_le, MeasureTheory.hausdorffMeasure_smul, hausdorffMeasure_le_one_of_subsingleton, LipschitzOnWith.hausdorffMeasure_image_le, MeasureTheory.hausdorffMeasure_affineSegment, LipschitzWith.hausdorffMeasure_image_le, Real.hausdorffMeasure_of_finrank_lt, MeasureTheory.instIsAddLeftInvariantHausdorffMeasureOfIsIsometricVAdd, MeasureTheory.hausdorffMeasure_homothety_preimage, HolderOnWith.hausdorffMeasure_image_le, dimH_def, hausdorffMeasure_of_lt_dimH
mkMetric 📖	CompOp	9 math math: mkMetric_apply, mkMetric_le_liminf_tsum, le_mkMetric, mkMetric_top, mkMetric_mono, mkMetric_le_liminf_sum, MeasureTheory.OuterMeasure.coe_mkMetric, mkMetric_toOuterMeasure, mkMetric_mono_smul
mkMetric' 📖	CompOp	1 math math: mkMetric'_toOuterMeasure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hausdorffMeasure_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike hausdorffMeasure iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.Nonempty Real ENNReal.instPowReal Metric.ediam EMetricSpace.toPseudoEMetricSpace SummationFilter.unconditional	—	mkMetric_apply
hausdorffMeasure_le_liminf_sum 📖	mathematical	Filter.Tendsto ENNReal nhds ENNReal.instTopologicalSpace instZeroENNReal Filter.Eventually Set Set.instHasSubset Set.iUnion	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike hausdorffMeasure Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Finset.sum ENNReal.instAddCommMonoid Finset.univ Real ENNReal.instPowReal Metric.ediam EMetricSpace.toPseudoEMetricSpace	—	mkMetric_le_liminf_sum
hausdorffMeasure_le_liminf_tsum 📖	mathematical	Countable Filter.Tendsto ENNReal nhds ENNReal.instTopologicalSpace instZeroENNReal Filter.Eventually Set Set.instHasSubset Set.iUnion	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike hausdorffMeasure Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder tsum ENNReal.instAddCommMonoid Real ENNReal.instPowReal Metric.ediam EMetricSpace.toPseudoEMetricSpace SummationFilter.unconditional	—	mkMetric_le_liminf_tsum
hausdorffMeasure_le_one_of_subsingleton 📖	mathematical	Set.Subsingleton Real Real.instLE Real.instZero	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike hausdorffMeasure AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass ENNReal.instCanonicallyOrderedAdd Set.subsingleton_iff_singleton eq_or_lt_of_le hausdorffMeasure_zero_singleton MeasureTheory.NoAtoms.measure_singleton noAtoms_hausdorff
hausdorffMeasure_mono 📖	mathematical	Real Real.instLE	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike hausdorffMeasure	—	LE.le.eq_or_lt le_rfl hausdorffMeasure_zero_or_top zero_le ENNReal.instCanonicallyOrderedAdd le_top
hausdorffMeasure_smul₀ 📖	mathematical	Real Real.instLE Real.instZero	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike hausdorffMeasure MetricSpace.toEMetricSpace NormedAddCommGroup.toMetricSpace Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring NormedDivisionRing.toDivisionRing Module.toDistribMulAction ESeminormedAddCommMonoid.toAddCommMonoid NNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id NNReal.instPowReal NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing NormedDivisionRing.toNormedRing	—	ENNReal.coe_rpow_of_nonneg LipschitzWith.hausdorffMeasure_image_le lipschitzWith_smul NormSMulClass.toIsBoundedSMul le_antisymm le_inv_smul_iff_of_pos PosSMulStrictMono.toPosSMulMono ENNReal.instPosSMulStrictMonoNNReal PosSMulMono.toPosSMulReflectLE NNReal.instIsStrictOrderedRing NNReal.instCanonicallyOrderedAdd NNReal.inv_rpow nnnorm_inv Eq.trans_le inv_smul_smul₀
hausdorffMeasure_zero_or_top 📖	mathematical	Real Real.instLT	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike hausdorffMeasure instZeroENNReal Top.top instTopENNReal	—	IsScalarTower.right le_iff' mkMetric_mono_smul ENNReal.coe_ne_top Nat.cast_zero ENNReal.coe_rpow_of_ne_zero pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd ENNReal.coe_eq_zero NNReal.rpow_eq_zero_iff Filter.mp_mem Ico_mem_nhdsGE instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.univ_mem' CanLift.prf ENNReal.canLift ne_top_of_lt Pi.smul_apply smul_eq_mul ENNReal.div_le_iff_le_mul eq_or_ne lt_or_ge ENNReal.zero_rpow_of_pos ENNReal.zero_div ENNReal.zero_rpow_of_neg LT.lt.trans_le ENNReal.div_top ENNReal.rpow_sub LE.le.trans LT.lt.le ENNReal.rpow_lt_rpow sub_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ENNReal.rpow_mul inv_mul_cancel₀ LT.lt.ne' ENNReal.rpow_one le_refl ENNReal.exists_nnreal_pos_mul_lt LT.lt.not_ge NNReal.instCanonicallyOrderedAdd
hausdorffMeasure_zero_singleton 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike hausdorffMeasure Real Real.instZero Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	le_antisymm Metric.ediam_singleton ENNReal.instCanonicallyOrderedAdd instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Set.iUnion_singleton_eq_range Set.range_const Set.instReflSubset Finset.sum_congr Finset.univ_unique ENNReal.rpow_zero Finset.sum_const Finset.card_singleton one_smul Filter.liminf_const Filter.atTop_neBot hausdorffMeasure_le_liminf_sum tendsto_const_nhds hausdorffMeasure_apply iInf_congr_Prop iSup_congr_Prop Set.mem_iUnion Set.mem_singleton ciSup_pos ENNReal.le_tsum le_trans le_iSup₂ zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero
le_hausdorffMeasure 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE DFunLike.coe MeasureTheory.Measure Set instFunLike Real ENNReal.instPowReal Metric.ediam EMetricSpace.toPseudoEMetricSpace	instPartialOrder hausdorffMeasure	—	le_mkMetric
le_mkMetric 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE DFunLike.coe MeasureTheory.Measure Set instFunLike Metric.ediam EMetricSpace.toPseudoEMetricSpace	instPartialOrder mkMetric	—	toOuterMeasure_le mkMetric_toOuterMeasure MeasureTheory.OuterMeasure.le_mkMetric
mkMetric'_toOuterMeasure 📖	mathematical	—	toOuterMeasure mkMetric' MeasureTheory.OuterMeasure.trim MeasureTheory.OuterMeasure.mkMetric'	—	—
mkMetric_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike mkMetric iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf Set.instHasSubset Set.iUnion tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.Nonempty Metric.ediam EMetricSpace.toPseudoEMetricSpace SummationFilter.unconditional	—	iSup_congr_Prop MeasureTheory.OuterMeasure.iSup_apply MeasureTheory.OuterMeasure.boundedBy_apply iInf_congr_Prop Function.Surjective.iSup_congr Function.Surjective.iInf_congr iInf_eq_if Mathlib.Tactic.Push.not_forall_eq ENNReal.tsum_eq_top_of_eq_top iSup_eq_if Metric.ediam_pos_iff LE.le.trans_lt zero_le ENNReal.instCanonicallyOrderedAdd LT.lt.not_ge
mkMetric_le_liminf_sum 📖	mathematical	Filter.Tendsto ENNReal nhds ENNReal.instTopologicalSpace instZeroENNReal Filter.Eventually Set Set.instHasSubset Set.iUnion	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike mkMetric Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Finset.sum ENNReal.instAddCommMonoid Finset.univ Metric.ediam EMetricSpace.toPseudoEMetricSpace	—	tsum_fintype SummationFilter.instLeAtTopUnconditional mkMetric_le_liminf_tsum Finite.to_countable Finite.of_fintype
mkMetric_le_liminf_tsum 📖	mathematical	Countable Filter.Tendsto ENNReal nhds ENNReal.instTopologicalSpace instZeroENNReal Filter.Eventually Set Set.instHasSubset Set.iUnion	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike mkMetric Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder tsum ENNReal.instAddCommMonoid Metric.ediam EMetricSpace.toPseudoEMetricSpace SummationFilter.unconditional	—	mkMetric_apply iSup₂_le le_of_forall_gt_imp_ge_of_dense ENNReal.instDenselyOrdered Filter.Frequently.exists Filter.Frequently.and_eventually Filter.frequently_lt_of_liminf_lt Filter.isCobounded_ge_of_top Filter.Eventually.and Filter.Tendsto.eventually gt_mem_nhds ENNReal.instOrderTopology iInf₂_le_of_le Encodable.iUnion_decode₂ iInf_le_of_le Metric.ediam_iUnion_mem_option LE.le.trans LT.lt.le tsum_iUnion_decode₂ iSup_congr_Prop Metric.ediam_empty iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd ENNReal.tsum_le_tsum iSup_le le_rfl
mkMetric_mono 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder nhdsWithin ENNReal.instTopologicalSpace instZeroENNReal Set.Ici	MeasureTheory.Measure instPartialOrder mkMetric	—	IsScalarTower.right one_smul mkMetric_mono_smul ENNReal.one_ne_top one_ne_zero NeZero.charZero_one ENNReal.instCharZero
mkMetric_mono_smul 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder nhdsWithin ENNReal.instTopologicalSpace instZeroENNReal Set.Ici Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id	MeasureTheory.Measure instPartialOrder mkMetric instSMul IsScalarTower.right	—	IsScalarTower.right MeasureTheory.OuterMeasure.coe_mkMetric coe_smul MeasureTheory.OuterMeasure.mkMetric_mono_smul
mkMetric_toOuterMeasure 📖	mathematical	—	toOuterMeasure mkMetric MeasureTheory.OuterMeasure.mkMetric	—	MeasureTheory.OuterMeasure.trim_mkMetric
mkMetric_top 📖	mathematical	—	mkMetric Top.top ENNReal instTopENNReal MeasureTheory.Measure OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	toOuterMeasure_injective mkMetric_toOuterMeasure MeasureTheory.OuterMeasure.mkMetric_top toOuterMeasure_top
noAtoms_hausdorff 📖	mathematical	Real Real.instLT Real.instZero	MeasureTheory.NoAtoms hausdorffMeasure	—	nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd hausdorffMeasure_apply iSup₂_le iInf₂_le_of_le Set.subset_iUnion iInf_le_of_le Metric.ediam_singleton iSup_congr_Prop ENNReal.zero_rpow_of_pos iSup_pos tsum_zero
one_le_hausdorffMeasure_zero_of_nonempty 📖	mathematical	Set.Nonempty	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike hausdorffMeasure Real Real.instZero	—	hausdorffMeasure_zero_singleton MeasureTheory.measure_mono instOuterMeasureClass Set.singleton_subset_iff

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
IsMetric 📖	MathDef	1 math math: mkMetric'_isMetric
mkMetric 📖	CompOp	13 math math: mkMetric_top, le_mkMetric, isometry_comap_mkMetric, isometryEquiv_map_mkMetric, isometry_map_mkMetric, coe_mkMetric, mkMetric_mono, mkMetric_smul, trim_mkMetric, mkMetric_nnreal_smul, mkMetric_mono_smul, MeasureTheory.Measure.mkMetric_toOuterMeasure, isometryEquiv_comap_mkMetric
mkMetric' 📖	CompOp	5 math math: mkMetric'.tendsto_pre, mkMetric'.tendsto_pre_nat, mkMetric'_isMetric, MeasureTheory.Measure.mkMetric'_toOuterMeasure, mkMetric'.eq_iSup_nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mkMetric 📖	mathematical	—	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal instFunLikeSetENNReal mkMetric MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.mkMetric	—	MeasureTheory.Measure.mkMetric_toOuterMeasure MeasureTheory.Measure.coe_toOuterMeasure
isometryEquiv_comap_mkMetric 📖	mathematical	—	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comap IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike mkMetric	—	isometry_comap_mkMetric IsometryEquiv.isometry IsometryEquiv.surjective
isometryEquiv_map_mkMetric 📖	mathematical	—	DFunLike.coe LinearMap ENNReal CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike map IsometryEquiv EMetricSpace.toPseudoEMetricSpace EquivLike.toFunLike IsometryEquiv.instEquivLike mkMetric	—	IsScalarTower.right isometryEquiv_comap_mkMetric map_comap_of_surjective IsometryEquiv.surjective
isometry_comap_mkMetric 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace Monotone ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike comap mkMetric	—	IsScalarTower.right iSup_congr_Prop comap_iSup Function.Surjective.iSup_congr comap_boundedBy iInf_congr_Prop le_trans LE.le.trans Metric.ediam_mono ciInf_pos MeasureTheory.extend_congr Isometry.ediam_image
isometry_map_mkMetric 📖	mathematical	Isometry EMetricSpace.toPseudoEMetricSpace Monotone ENNReal PartialOrder.toPreorder ENNReal.instPartialOrder	DFunLike.coe LinearMap CommSemiring.toSemiring ENNReal.instCommSemiring RingHom.id Semiring.toNonAssocSemiring MeasureTheory.OuterMeasure addCommMonoid instModule Semiring.toModule IsScalarTower.right Algebra.id LinearMap.instFunLike map mkMetric restrict Set.range	—	IsScalarTower.right isometry_comap_mkMetric map_comap
le_mkMetric 📖	mathematical	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Preorder.toLE DFunLike.coe MeasureTheory.OuterMeasure Set instFunLikeSetENNReal Metric.ediam EMetricSpace.toPseudoEMetricSpace	instPartialOrder mkMetric	—	le_iSup₂_of_le mkMetric'.le_pre
mkMetric'_isMetric 📖	mathematical	—	IsMetric mkMetric'	—	tendsto_nhds_unique_of_eventuallyEq ENNReal.instT2Space ENNReal.nhdsGT_zero_neBot mkMetric'.tendsto_pre Filter.Tendsto.add ENNReal.instContinuousAdd Filter.mp_mem Ioo_mem_nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd Filter.univ_mem' boundedBy_union_of_top_of_nonempty_inter LT.lt.trans_le LE.le.trans Metric.edist_le_ediam_of_mem iInf_eq_top LT.lt.not_ge
mkMetric_mono 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder nhdsWithin ENNReal.instTopologicalSpace instZeroENNReal Set.Ici	MeasureTheory.OuterMeasure instPartialOrder mkMetric	—	IsScalarTower.right one_smul mkMetric_mono_smul ENNReal.one_ne_top one_ne_zero NeZero.charZero_one ENNReal.instCharZero
mkMetric_mono_smul 📖	mathematical	Filter.EventuallyLE ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder nhdsWithin ENNReal.instTopologicalSpace instZeroENNReal Set.Ici Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id	MeasureTheory.OuterMeasure instPartialOrder mkMetric instSMul IsScalarTower.right	—	IsScalarTower.right mem_nhdsGE_iff_exists_Ico_subset' ENNReal.instOrderTopology zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero le_of_tendsto_of_tendsto OrderTopology.to_orderClosedTopology ENNReal.nhdsGT_zero_neBot mkMetric'.tendsto_pre ENNReal.Tendsto.const_mul Filter.mem_of_superset Ioo_mem_nhdsGT instClosedIciTopology smul_eq_mul smul_apply smul_boundedBy le_boundedBy LE.le.trans boundedBy_le iInf_congr_Prop iInf_eq_if zero_le ENNReal.instCanonicallyOrderedAdd LE.le.trans_lt ENNReal.mul_top
mkMetric_nnreal_smul 📖	mathematical	—	mkMetric NNReal Function.hasSMul ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id MeasureTheory.OuterMeasure instSMul IsScalarTower.right	—	IsScalarTower.right ENNReal.smul_def mkMetric_smul ENNReal.coe_ne_top ENNReal.coe_ne_zero
mkMetric_smul 📖	mathematical	—	mkMetric ENNReal Function.hasSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id MeasureTheory.OuterMeasure instSMul IsScalarTower.right	—	IsScalarTower.right iSup_congr_Prop smul_iSup smul_boundedBy MeasureTheory.ennreal_smul_extend
mkMetric_top 📖	mathematical	—	mkMetric Top.top ENNReal instTopENNReal MeasureTheory.OuterMeasure OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	iSup_congr_Prop MeasureTheory.extend_top boundedBy_top le_iSup_iff iSup_pos
trim_mkMetric 📖	mathematical	—	trim mkMetric	—	mkMetric'.eq_iSup_nat trim_iSup instCountableNat mkMetric'.trim_pre BorelSpace.opensMeasurable Metric.ediam_closure

MeasureTheory.OuterMeasure.IsMetric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
borel_le_caratheodory 📖	mathematical	MeasureTheory.OuterMeasure.IsMetric	MeasurableSpace MeasurableSpace.instLE borel UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace MeasureTheory.OuterMeasure.caratheodory	—	borel_eq_generateFrom_isClosed MeasurableSpace.generateFrom_le MeasureTheory.OuterMeasure.isCaratheodory_iff_le ENNReal.inv_ne_zero ENNReal.natCast_ne_top LE.le.trans Metric.infEDist_le_edist_of_mem Metric.AreSeparated.mono Set.Subset.rfl Set.inter_subset_right Set.subset_inter Set.inter_subset_left Metric.AreSeparated.subset_compl_right Metric.AreSeparated.symm MeasureTheory.OuterMeasure.mono Set.union_subset_union_right Set.inter_union_diff Set.Subset.antisymm Set.iUnion_subset ENNReal.exists_inv_nat_lt Metric.mem_iff_infEDist_zero_of_closed Set.mem_iUnion LT.lt.le add_top Set.diff_subset le_trans ENNReal.inv_le_inv Nat.cast_le IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero Eq.le MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top tsum_even_add_odd ENNReal.instT2Space ENNReal.instContinuousAdd ENNReal.summable ENNReal.add_ne_top ne_top_of_le_ne_top ENNReal.tsum_eq_iSup_nat iSup_le_iff finset_iUnion_of_pairwise_separated ENNReal.inv_lt_inv Nat.cast_lt Nat.instAtLeastTwoHAddOfNat Nat.cast_add Nat.cast_mul Nat.cast_one ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub not_le Metric.infEDist_lt_iff Metric.le_infEDist ENNReal.le_of_add_le_add_right LT.lt.ne_top add_le_add covariant_swap_add_of_covariant_add le_rfl Eq.trans_le tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE PseudoEMetricSpace.edist_triangle Ne.lt_or_gt add_zero add_le_add_right ENNReal.add_iSup iSup_le
finset_iUnion_of_pairwise_separated 📖	mathematical	MeasureTheory.OuterMeasure.IsMetric Metric.AreSeparated EMetricSpace.toPseudoEMetricSpace	DFunLike.coe MeasureTheory.OuterMeasure Set ENNReal MeasureTheory.OuterMeasure.instFunLikeSetENNReal Set.iUnion Finset Finset.instMembership Finset.sum ENNReal.instAddCommMonoid	—	Finset.induction_on Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty MeasureTheory.measure_empty MeasureTheory.OuterMeasure.instOuterMeasureClass Finset.set_biUnion_insert Metric.AreSeparated.finset_iUnion_right Finset.sum_insert
le_caratheodory 📖	mathematical	MeasureTheory.OuterMeasure.IsMetric	MeasurableSpace MeasurableSpace.instLE MeasureTheory.OuterMeasure.caratheodory	—	BorelSpace.measurable_eq borel_le_caratheodory

MeasureTheory.OuterMeasure.mkMetric'

Definitions

Name	Category	Theorems
pre 📖	CompOp	8 math math: tendsto_pre, tendsto_pre_nat, pre_le, mono_pre_nat, trim_pre, mono_pre, eq_iSup_nat, le_pre

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_iSup_nat 📖	mathematical	—	MeasureTheory.OuterMeasure.mkMetric' iSup MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instSupSet pre ENNReal ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.OuterMeasure.ext MeasureTheory.OuterMeasure.iSup_apply tendsto_nhds_unique ENNReal.instT2Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_pre_nat tendsto_atTop_iSup LinearOrder.supConvergenceClass ENNReal.instOrderTopology mono_pre_nat
le_pre 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.OuterMeasure.instPartialOrder pre ENNReal ENNReal.instPartialOrder DFunLike.coe Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal	—	iInf_congr_Prop
mono_pre 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instPartialOrder pre	—	le_pre pre_le LE.le.trans
mono_pre_nat 📖	mathematical	—	Monotone MeasureTheory.OuterMeasure Nat.instPreorder PartialOrder.toPreorder MeasureTheory.OuterMeasure.instPartialOrder pre ENNReal ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	le_pre pre_le LE.le.trans IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing ENNReal.instCharZero
pre_le 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Metric.ediam EMetricSpace.toPseudoEMetricSpace	DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal pre	—	LE.le.trans MeasureTheory.OuterMeasure.boundedBy_le iInf_le
tendsto_pre 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal pre nhdsWithin ENNReal.instTopologicalSpace instZeroENNReal Set.Ioi PartialOrder.toPreorder ENNReal.instPartialOrder nhds MeasureTheory.OuterMeasure.mkMetric'	—	tendsto_comp_coe_Ioi_atBot ENNReal.instOrderTopology Order.IsPredPrelimit.of_dense ENNReal.instDenselyOrdered iSup_subtype' MeasureTheory.OuterMeasure.iSup_apply tendsto_atBot_iSup LinearOrder.supConvergenceClass mono_pre
tendsto_pre_nat 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe MeasureTheory.OuterMeasure Set MeasureTheory.OuterMeasure.instFunLikeSetENNReal pre ENNReal.instInv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace MeasureTheory.OuterMeasure.mkMetric'	—	Filter.Tendsto.comp tendsto_pre Filter.tendsto_inf ENNReal.tendsto_inv_nat_nhds_zero Filter.tendsto_principal Filter.Eventually.of_forall
trim_pre 📖	mathematical	closure UniformSpace.toTopologicalSpace PseudoEMetricSpace.toUniformSpace EMetricSpace.toPseudoEMetricSpace	MeasureTheory.OuterMeasure.trim pre	—	le_antisymm le_pre MeasureTheory.OuterMeasure.trim_eq_iInf iInf_le_of_le subset_closure measurableSet_closure LE.le.trans_eq pre_le Metric.ediam_closure MeasureTheory.OuterMeasure.le_trim

---

← Back to Index