HausdorffDimension

📁 Source: Mathlib/Topology/MetricSpace/HausdorffDimension.lean

Statistics

Metric	Count
Definitions `dimH`	1
Theorems `dimH_preimage_le`, `le_dimH_image`, `dense_compl_range_of_finrank_lt_finrank`, `dimH_range_le`, `dense_compl_image_of_dimH_lt_finrank`, `dimH_image_le`, `dimH_image`, `dimH_preimage`, `dimH_univ`, `dimH_zero`, `dimH_image_le`, `dimH_image_le`, `dimH_range_le`, `dimH_image`, `dimH_image`, `dimH_preimage`, `dimH_univ`, `dimH_image_le`, `dimH_image_le`, `dimH_range_le`, `dimH_eq_finrank_vectorSpan`, `dimH_ball_pi`, `dimH_ball_pi_fin`, `dimH_lt_top`, `dimH_ne_top`, `dimH_of_mem_nhds`, `dimH_of_nonempty_interior`, `dimH_segment`, `dimH_univ`, `dimH_univ_eq_finrank`, `dimH_univ_pi`, `dimH_univ_pi_fin`, `hausdorffMeasure_of_finrank_lt`, `dimH_zero`, `dimH_zero`, `dimH_zero`, `bsupr_limsup_dimH`, `dense_compl_of_dimH_lt_finrank`, `dimH_bUnion`, `dimH_coe_finset`, `dimH_countable`, `dimH_def`, `dimH_empty`, `dimH_eq_iInf`, `dimH_finite`, `dimH_iUnion`, `dimH_image_le_of_locally_holder_on`, `dimH_image_le_of_locally_lipschitzOn`, `dimH_le`, `dimH_le_of_hausdorffMeasure_ne_top`, `dimH_mono`, `dimH_of_hausdorffMeasure_ne_zero_ne_top`, `dimH_orthogonalProjection_le`, `dimH_range_le_of_locally_holder_on`, `dimH_range_le_of_locally_lipschitzOn`, `dimH_sUnion`, `dimH_singleton`, `dimH_subsingleton`, `dimH_union`, `exists_mem_nhdsWithin_lt_dimH_of_lt_dimH`, `hausdorffMeasure_of_dimH_lt`, `hausdorffMeasure_of_lt_dimH`, `iSup_limsup_dimH`, `le_dimH_of_hausdorffMeasure_eq_top`, `le_dimH_of_hausdorffMeasure_ne_zero`, `measure_zero_of_dimH_lt`	66
Total	67

AntilipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_preimage_le` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.preimage`	—	`dimH_le` `le_dimH_of_hausdorffMeasure_eq_top` `hausdorffMeasure_preimage_le` `NNReal.coe_nonneg` `Mathlib.Tactic.Contrapose.contrapose₁` `ENNReal.mul_ne_top` `top_le_iff`
`le_dimH_image` 📖	mathematical	`AntilipschitzWith` `EMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.image`	—	`dimH_mono` `Set.subset_preimage_image` `dimH_preimage_le`

ContDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_compl_range_of_finrank_lt_finrank` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Dense` `Compl.compl` `Set` `Set.instCompl` `Set.range`	—	`dense_compl_of_dimH_lt_finrank` `LE.le.trans_lt` `dimH_range_le` `Nat.cast_lt` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `ENNReal.instIsOrderedRing` `ENNReal.instCharZero`
`dimH_range_le` 📖	mathematical	`ContDiff` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.range` `AddMonoidWithOne.toNatCast` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	—	`Set.image_univ` `ContDiffOn.dimH_image_le` `contDiffOn` `convex_univ` `Set.Subset.rfl` `Real.dimH_univ_eq_finrank`

ContDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dense_compl_image_of_dimH_lt_finrank` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Convex` `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` `Set` `Set.instHasSubset` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `AddMonoidWithOne.toNatCast` `instAddCommMonoidWithOneENNReal` `Module.finrank`	`Dense` `Compl.compl` `Set.instCompl` `Set.image`	—	`dense_compl_of_dimH_lt_finrank` `LE.le.trans_lt` `dimH_image_le`
`dimH_image_le` 📖	mathematical	`ContDiffOn` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `WithTop` `ENat` `WithTop.one` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instCommSemiringENat` `Convex` `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` `Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.image`	—	`dimH_image_le_of_locally_lipschitzOn` `UniformSpace.secondCountable_of_separable` `EMetric.instIsCountablyGeneratedUniformity` `TopologicalSpace.SecondCountableTopology.to_separableSpace` `secondCountable_of_proper` `FiniteDimensional.proper_real` `ContDiffWithinAt.exists_lipschitzOnWith` `nhdsWithin_mono`

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image` 📖	mathematical	—	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.image` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `le_antisymm` `LipschitzWith.dimH_image_le` `RingHomIsometric.ids` `lipschitz` `symm_image_image`
`dimH_preimage` 📖	mathematical	—	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.preimage` `DFunLike.coe` `ContinuousLinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `EquivLike.toFunLike` `equivLike`	—	`RingHomInvPair.ids` `image_symm_eq_preimage` `dimH_image`
`dimH_univ` 📖	mathematical	—	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.univ`	—	`RingHomInvPair.ids` `dimH_preimage` `Set.preimage_univ`

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_zero` 📖	mathematical	—	`dimH` `SetLike.coe` `Finset` `instSetLike` `ENNReal` `instZeroENNReal`	—	`dimH_coe_finset`

HolderOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image_le` 📖	mathematical	`HolderOnWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `dimH` `Set.image` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal`	—	`dimH_le` `hausdorffMeasure_image_le` `NNReal.coe_nonneg` `Mathlib.Tactic.Contrapose.contrapose₁` `ENNReal.mul_ne_top` `ENNReal.coe_ne_top` `top_le_iff` `ENNReal.coe_rpow_of_nonneg` `ENNReal.le_div_iff_mul_le` `ENNReal.coe_eq_zero` `LT.lt.ne'` `mul_comm` `ENNReal.coe_mul` `le_dimH_of_hausdorffMeasure_eq_top`

HolderWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image_le` 📖	mathematical	`HolderWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `dimH` `Set.image` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal`	—	`HolderOnWith.dimH_image_le` `holderOnWith`
`dimH_range_le` 📖	mathematical	`HolderWith` `EMetricSpace.toPseudoEMetricSpace` `NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `dimH` `Set.range` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Set.univ` `ENNReal.ofNNReal`	—	`dimH_image_le` `Set.image_univ`

Isometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image` 📖	mathematical	`Isometry` `EMetricSpace.toPseudoEMetricSpace`	`dimH` `Set.image`	—	`le_antisymm` `LipschitzWith.dimH_image_le` `lipschitz` `AntilipschitzWith.le_dimH_image` `antilipschitz`

IsometryEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image` 📖	mathematical	—	`dimH` `Set.image` `DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`Isometry.dimH_image` `isometry`
`dimH_preimage` 📖	mathematical	—	`dimH` `Set.preimage` `DFunLike.coe` `IsometryEquiv` `EMetricSpace.toPseudoEMetricSpace` `EquivLike.toFunLike` `instEquivLike`	—	`image_symm` `dimH_image`
`dimH_univ` 📖	mathematical	—	`dimH` `Set.univ`	—	`dimH_preimage` `Set.preimage_univ`

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image_le` 📖	mathematical	`LipschitzOnWith` `EMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.image`	—	`div_one` `HolderOnWith.dimH_image_le` `holderOnWith` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`

LipschitzWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_image_le` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.image`	—	`LipschitzOnWith.dimH_image_le` `lipschitzOnWith`
`dimH_range_le` 📖	mathematical	`LipschitzWith` `EMetricSpace.toPseudoEMetricSpace`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.range` `Set.univ`	—	`dimH_image_le` `Set.image_univ`

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_ball_pi` 📖	mathematical	`Real` `instLT` `instZero`	`dimH` `emetricSpacePi` `MetricSpace.toEMetricSpace` `metricSpace` `Metric.ball` `pseudoMetricSpacePi` `pseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Fintype.card`	—	`isEmpty_or_nonempty` `dimH_subsingleton` `Unique.instSubsingleton` `Nat.cast_eq_zero` `ENNReal.instCharZero` `Fintype.card_eq_zero_iff` `ENNReal.coe_natCast` `Pi.borelSpace` `Finite.to_countable` `Finite.of_fintype` `instSecondCountableTopologyReal` `borelSpace` `Nat.instAtLeastTwoHAddOfNat` `MeasureTheory.hausdorffMeasure_pi_real` `volume_pi_ball` `dimH_of_hausdorffMeasure_ne_zero_ne_top` `NNReal.coe_natCast` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `instIsStrictOrderedRing` `instZeroLEOneClass` `mul_pos` `zero_lt_two'` `NeZero.charZero_one` `RCLike.charZero_rclike` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `ENNReal.ofReal_ne_top`
`dimH_ball_pi_fin` 📖	mathematical	`Real` `instLT` `instZero`	`dimH` `emetricSpacePi` `Fin.fintype` `MetricSpace.toEMetricSpace` `metricSpace` `Metric.ball` `pseudoMetricSpacePi` `pseudoMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`dimH_ball_pi` `Fintype.card_fin`
`dimH_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Top.top` `instTopENNReal`	—	`dimH_mono` `Set.subset_univ` `dimH_univ_eq_finrank`
`dimH_ne_top` 📖	—	—	—	—	`LT.lt.ne` `dimH_lt_top`
`dimH_of_mem_nhds` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `Pi.topologicalAddGroup` `instIsTopologicalAddGroupReal` `instContinuousSMulForall` `IsModuleTopology.toContinuousSMul` `IsTopologicalSemiring.toIsModuleTopology` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `instCompleteSpace` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Pi.t2Space` `FiniteDimensional.finiteDimensional_pi'` `Finite.of_fintype` `FiniteDimensional.rclike_to_real` `Module.finrank_fin_fun` `commRing_strongRankCondition` `instNontrivial` `ContinuousLinearEquiv.dimH_image` `le_antisymm` `LE.le.trans_eq` `dimH_mono` `Set.subset_univ` `dimH_univ_pi_fin` `ContinuousLinearEquiv.map_nhds_eq` `Filter.image_mem_map` `Filter.HasBasis.mem_iff` `Metric.nhds_basis_ball` `dimH_ball_pi_fin`
`dimH_of_nonempty_interior` 📖	mathematical	`Set.Nonempty` `interior` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField`	—	`dimH_of_mem_nhds` `mem_interior_iff_mem_nhds`
`dimH_segment` 📖	mathematical	—	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `segment` `Real` `semiring` `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` `instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `normedField` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`Convex.dimH_eq_finrank_vectorSpan` `convex_segment` `instIsOrderedRing` `left_mem_segment` `instZeroLEOneClass` `vectorSpan_segment` `instIsStrictOrderedRing` `finrank_span_singleton` `sub_ne_zero` `Nat.cast_one`
`dimH_univ` 📖	mathematical	—	`dimH` `Real` `MetricSpace.toEMetricSpace` `metricSpace` `Set.univ` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`dimH_univ_eq_finrank` `FiniteDimensional.rclike_to_real` `Module.finrank_self` `commRing_strongRankCondition` `instNontrivial` `Nat.cast_one`
`dimH_univ_eq_finrank` 📖	mathematical	—	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.univ` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField`	—	`dimH_of_mem_nhds` `Filter.univ_mem`
`dimH_univ_pi` 📖	mathematical	—	`dimH` `emetricSpacePi` `Real` `MetricSpace.toEMetricSpace` `metricSpace` `Set.univ` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Fintype.card`	—	`Metric.iUnion_ball_nat_succ` `dimH_iUnion` `instCountableNat` `dimH_ball_pi` `Nat.cast_add_one_pos` `IsOrderedAddMonoid.toAddLeftMono` `instIsOrderedAddMonoid` `instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `iSup_const`
`dimH_univ_pi_fin` 📖	mathematical	—	`dimH` `emetricSpacePi` `Real` `Fin.fintype` `MetricSpace.toEMetricSpace` `metricSpace` `Set.univ` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`dimH_univ_pi` `Fintype.card_fin`
`hausdorffMeasure_of_finrank_lt` 📖	mathematical	`Real` `instLT` `instNatCast` `Module.finrank` `semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `normedField`	`MeasureTheory.Measure.hausdorffMeasure` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero`	—	`CanLift.prf` `NNReal.canLift` `LE.le.trans` `Nat.cast_nonneg` `instIsOrderedRing` `LT.lt.le` `MeasureTheory.Measure.measure_univ_eq_zero` `hausdorffMeasure_of_dimH_lt` `dimH_univ_eq_finrank` `NNReal.coe_natCast`

Real.Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_eq_finrank_vectorSpan` 📖	mathematical	`Convex` `Real` `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` `Set.Nonempty`	`dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `ENNReal` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Submodule` `Ring.toSemiring` `Real.instRing` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `vectorSpan` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `Submodule.addCommMonoid` `Submodule.module`	—	`Set.Nonempty.to_subtype` `IsScalarTower.left` `instNonemptySubtypeMemAffineSubspaceAffineSpanOfElem` `subset_affineSpan` `Set.Nonempty.some_mem` `Set.image_preimage_eq_of_subset` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Eq.superset` `Set.instReflSubset` `Subtype.range_coe` `Isometry.dimH_image` `isometry_subtype_coe` `AffineIsometryEquiv.isometry` `Real.dimH_of_nonempty_interior` `FiniteDimensional.finiteDimensional_submodule` `Set.image_congr` `Homeomorph.image_interior` `intrinsicInterior_nonempty` `direction_affineSpan`

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_zero` 📖	mathematical	—	`dimH` `ENNReal` `instZeroENNReal`	—	`dimH_countable`

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_zero` 📖	mathematical	—	`dimH` `ENNReal` `instZeroENNReal`	—	`dimH_finite`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dimH_zero` 📖	mathematical	`Set.Subsingleton`	`dimH` `ENNReal` `instZeroENNReal`	—	`dimH_subsingleton`

(root)

Definitions

Name	Category	Theorems
`dimH` 📖	CompOp	57 math math: `LipschitzWith.dimH_image_le`, `IsometryEquiv.dimH_preimage`, `Real.dimH_of_mem_nhds`, `dimH_sUnion`, `le_dimH_of_hausdorffMeasure_ne_zero`, `Real.dimH_lt_top`, `dimH_coe_finset`, `HolderOnWith.dimH_image_le`, `ContDiffOn.dimH_image_le`, `Finset.dimH_zero`, `le_dimH_of_hausdorffMeasure_eq_top`, `dimH_range_le_of_locally_holder_on`, `Real.dimH_univ_eq_finrank`, `Real.dimH_univ`, `dimH_of_hausdorffMeasure_ne_zero_ne_top`, `dimH_countable`, `dimH_empty`, `dimH_union`, `Real.dimH_univ_pi_fin`, `Real.dimH_ball_pi`, `dimH_le`, `LipschitzOnWith.dimH_image_le`, `HolderWith.dimH_range_le`, `ContinuousLinearEquiv.dimH_image`, `Set.Countable.dimH_zero`, `dimH_eq_iInf`, `IsometryEquiv.dimH_univ`, `dimH_image_le_of_locally_lipschitzOn`, `Real.dimH_of_nonempty_interior`, `dimH_bUnion`, `dimH_le_of_hausdorffMeasure_ne_top`, `dimH_mono`, `Real.Convex.dimH_eq_finrank_vectorSpan`, `IsometryEquiv.dimH_image`, `AntilipschitzWith.dimH_preimage_le`, `Real.dimH_univ_pi`, `LipschitzWith.dimH_range_le`, `dimH_finite`, `AntilipschitzWith.le_dimH_image`, `dimH_singleton`, `Real.dimH_ball_pi_fin`, `Set.Subsingleton.dimH_zero`, `dimH_orthogonalProjection_le`, `ContinuousLinearEquiv.dimH_univ`, `Real.dimH_segment`, `ContDiff.dimH_range_le`, `dimH_iUnion`, `ContinuousLinearEquiv.dimH_preimage`, `dimH_range_le_of_locally_lipschitzOn`, `dimH_image_le_of_locally_holder_on`, `bsupr_limsup_dimH`, `dimH_def`, `dimH_subsingleton`, `iSup_limsup_dimH`, `Isometry.dimH_image`, `Set.Finite.dimH_zero`, `HolderWith.dimH_image_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bsupr_limsup_dimH` 📖	mathematical	—	`iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set` `Set.instMembership` `Filter.limsup` `dimH` `Filter.smallSets` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace`	—	`le_antisymm` `iSup₂_le` `Filter.limsup_le_of_le` `Filter.isCobounded_le_of_bot` `Filter.eventually_smallSets` `self_mem_nhdsWithin` `dimH_mono` `le_of_forall_lt_imp_le_of_dense` `ENNReal.instDenselyOrdered` `exists_mem_nhdsWithin_lt_dimH_of_lt_dimH` `le_iSup₂_of_le` `Filter.limsup_eq` `le_sInf` `LE.le.trans` `LT.lt.le` `Set.Subset.rfl`
`dense_compl_of_dimH_lt_finrank` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Module.finrank` `Real` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField`	`Dense` `Compl.compl` `Set` `Set.instCompl`	—	`mem_closure_iff_nhds` `Set.nonempty_iff_ne_empty` `LT.lt.not_ge` `Real.dimH_of_mem_nhds` `dimH_mono` `Set.diff_eq_empty` `Set.diff_eq`
`dimH_bUnion` 📖	mathematical	—	`dimH` `Set.iUnion` `Set` `Set.instMembership` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Set.biUnion_eq_iUnion` `dimH_iUnion` `Encodable.countable` `iSup_subtype''`
`dimH_coe_finset` 📖	mathematical	—	`dimH` `SetLike.coe` `Finset` `Finset.instSetLike` `ENNReal` `instZeroENNReal`	—	`Set.Finite.dimH_zero` `Finset.finite_toSet`
`dimH_countable` 📖	mathematical	—	`dimH` `ENNReal` `instZeroENNReal`	—	`dimH_bUnion` `iSup_congr_Prop` `dimH_singleton` `ENNReal.iSup_zero` `Set.biUnion_of_singleton`
`dimH_def` 📖	mathematical	—	`dimH` `iSup` `ENNReal` `NNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `Top.top` `instTopENNReal` `ENNReal.ofNNReal`	—	`BorelSpace.measurable_eq` `dimH.eq_1`
`dimH_empty` 📖	mathematical	—	`dimH` `Set` `Set.instEmptyCollection` `ENNReal` `instZeroENNReal`	—	`Set.Subsingleton.dimH_zero` `Set.subsingleton_empty`
`dimH_eq_iInf` 📖	mathematical	—	`dimH` `iInf` `ENNReal` `NNReal` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `instZeroENNReal` `ENNReal.ofNNReal`	—	`le_antisymm` `dimH_def` `ENNReal.instCanonicallyOrderedAdd` `MeasureTheory.Measure.hausdorffMeasure_mono` `LT.lt.le` `ENNReal.lt_iff_exists_nnreal_btwn` `hausdorffMeasure_of_dimH_lt` `LT.lt.not_ge` `iInf₂_le`
`dimH_finite` 📖	mathematical	—	`dimH` `ENNReal` `instZeroENNReal`	—	`Set.Countable.dimH_zero` `Set.Finite.countable`
`dimH_iUnion` 📖	mathematical	—	`dimH` `Set.iUnion` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`le_antisymm` `dimH_le` `Mathlib.Tactic.Contrapose.contrapose₁` `hausdorffMeasure_of_dimH_lt` `LE.le.trans_lt` `le_iSup` `MeasureTheory.measure_iUnion_null` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.zero_ne_top` `iSup_le` `dimH_mono` `Set.subset_iUnion`
`dimH_image_le_of_locally_holder_on` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `HolderOnWith`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `dimH` `Set.image` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `ENNReal.ofNNReal`	—	`TopologicalSpace.countable_cover_nhdsWithin` `Set.inter_eq_self_of_subset_left` `Set.inter_iUnion₂` `Set.image_iUnion₂` `dimH_bUnion` `ENNReal.iSup_div` `iSup₂_mono` `HolderOnWith.dimH_image_le` `HolderOnWith.mono` `Set.inter_subset_right` `Function.sometimes_spec`
`dimH_image_le_of_locally_lipschitzOn` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `LipschitzOnWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.image`	—	`div_one` `dimH_image_le_of_locally_holder_on` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `NNReal.instIsStrictOrderedRing`
`dimH_le` 📖	mathematical	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal`	`dimH`	—	`Eq.trans_le` `dimH_def` `iSup₂_le`
`dimH_le_of_hausdorffMeasure_ne_top` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `ENNReal.ofNNReal`	—	`le_of_not_gt` `hausdorffMeasure_of_lt_dimH`
`dimH_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH`	—	`dimH_le` `le_dimH_of_hausdorffMeasure_eq_top` `top_unique` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass`
`dimH_of_hausdorffMeasure_ne_zero_ne_top` 📖	mathematical	—	`dimH` `ENNReal.ofNNReal`	—	`le_antisymm` `dimH_le_of_hausdorffMeasure_ne_top` `le_dimH_of_hausdorffMeasure_ne_zero`
`dimH_orthogonalProjection_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `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` `instEMetricSpaceSubtype` `MetricSpace.toEMetricSpace` `NormedAddCommGroup.toMetricSpace` `Set.image` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceSubtype` `Submodule.addCommMonoid` `Submodule.module` `ContinuousLinearMap.funLike` `Submodule.orthogonalProjection`	—	`LipschitzWith.dimH_image_le` `Submodule.lipschitzWith_orthogonalProjection`
`dimH_range_le_of_locally_holder_on` 📖	mathematical	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instZeroNNReal` `Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `HolderOnWith`	`ENNReal` `Preorder.toLE` `ENNReal.instPartialOrder` `dimH` `Set.range` `DivInvMonoid.toDiv` `ENNReal.instDivInvMonoid` `Set.univ` `ENNReal.ofNNReal`	—	`Set.image_univ` `dimH_image_le_of_locally_holder_on` `nhdsWithin_univ`
`dimH_range_le_of_locally_lipschitzOn` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace` `LipschitzOnWith`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `Set.range` `Set.univ`	—	`Set.image_univ` `dimH_image_le_of_locally_lipschitzOn` `nhdsWithin_univ`
`dimH_sUnion` 📖	mathematical	—	`dimH` `Set.sUnion` `iSup` `ENNReal` `Set` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Set.instMembership`	—	`Set.sUnion_eq_biUnion` `dimH_bUnion`
`dimH_singleton` 📖	mathematical	—	`dimH` `Set` `Set.instSingletonSet` `ENNReal` `instZeroENNReal`	—	`Set.Subsingleton.dimH_zero` `Set.subsingleton_singleton`
`dimH_subsingleton` 📖	mathematical	`Set.Subsingleton`	`dimH` `ENNReal` `instZeroENNReal`	—	`le_antisymm` `dimH_le_of_hausdorffMeasure_ne_top` `LT.lt.ne` `LE.le.trans_lt` `MeasureTheory.Measure.hausdorffMeasure_le_one_of_subsingleton` `le_rfl` `ENNReal.one_lt_top` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`dimH_union` 📖	mathematical	—	`dimH` `Set` `Set.instUnion` `ENNReal` `ENNReal.instMax`	—	`Set.union_eq_iUnion` `dimH_iUnion` `Bool.countable` `iSup_bool_eq`
`exists_mem_nhdsWithin_lt_dimH_of_lt_dimH` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH`	`Set` `Set.instMembership`	—	`Mathlib.Tactic.Contrapose.contrapose₁` `Mathlib.Tactic.Push.not_and_eq` `Mathlib.Tactic.Push.not_forall_eq` `TopologicalSpace.countable_cover_nhdsWithin` `dimH_mono` `dimH_bUnion` `iSup₂_le` `Function.sometimes_spec`
`hausdorffMeasure_of_dimH_lt` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `ENNReal.ofNNReal`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `instZeroENNReal`	—	`ENNReal.lt_iff_exists_nnreal_btwn` `dimH_def` `MeasureTheory.Measure.hausdorffMeasure_zero_or_top` `NNReal.coe_lt_coe` `ENNReal.coe_lt_coe` `LT.lt.not_ge` `le_iSup₂`
`hausdorffMeasure_of_lt_dimH` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `dimH`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `Top.top` `instTopENNReal`	—	`dimH_def` `top_unique` `MeasureTheory.Measure.hausdorffMeasure_mono` `LT.lt.le` `NNReal.coe_lt_coe` `ENNReal.coe_lt_coe`
`iSup_limsup_dimH` 📖	mathematical	—	`iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Filter.limsup` `Set` `dimH` `Filter.smallSets` `nhdsWithin` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `EMetricSpace.toPseudoEMetricSpace`	—	`le_antisymm` `iSup_le` `Filter.limsup_le_of_le` `Filter.isCobounded_le_of_bot` `Filter.eventually_smallSets` `self_mem_nhdsWithin` `dimH_mono` `bsupr_limsup_dimH` `iSup₂_le_iSup`
`le_dimH_of_hausdorffMeasure_eq_top` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `Top.top` `instTopENNReal`	`Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `dimH`	—	`dimH_def` `le_iSup₂`
`le_dimH_of_hausdorffMeasure_ne_zero` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofNNReal` `dimH`	—	`le_of_not_gt` `hausdorffMeasure_of_dimH_lt`
`measure_zero_of_dimH_lt` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `MeasureTheory.Measure.hausdorffMeasure` `NNReal.toReal` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `dimH` `ENNReal.ofNNReal`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `instZeroENNReal`	—	`hausdorffMeasure_of_dimH_lt`

---

← Back to Index