Commit 2023-06-12 14:52 41b0484e

View on Github →

feat: port Topology.MetricSpace.HausdorffDimension (#4974)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/HausdorffDimension.lean

added theorem AntilipschitzWith.dimH_preimage_le

added theorem AntilipschitzWith.le_dimH_image

added theorem ContDiff.dense_compl_range_of_finrank_lt_finrank

added theorem ContDiff.dimH_range_le

added theorem ContDiffOn.dense_compl_image_of_dimH_lt_finrank

added theorem ContDiffOn.dimH_image_le

added theorem ContinuousLinearEquiv.dimH_image

added theorem ContinuousLinearEquiv.dimH_preimage

added theorem ContinuousLinearEquiv.dimH_univ

added theorem HolderOnWith.dimH_image_le

added theorem HolderWith.dimH_image_le

added theorem HolderWith.dimH_range_le

added theorem Isometry.dimH_image

added theorem IsometryEquiv.dimH_image

added theorem IsometryEquiv.dimH_preimage

added theorem IsometryEquiv.dimH_univ

added theorem LipschitzOnWith.dimH_image_le

added theorem LipschitzWith.dimH_image_le

added theorem LipschitzWith.dimH_range_le

added theorem Real.dimH_ball_pi

added theorem Real.dimH_ball_pi_fin

added theorem Real.dimH_of_mem_nhds

added theorem Real.dimH_of_nonempty_interior

added theorem Real.dimH_univ

added theorem Real.dimH_univ_eq_finrank

added theorem Real.dimH_univ_pi

added theorem Real.dimH_univ_pi_fin

added theorem bsupr_limsup_dimH

added theorem dense_compl_of_dimH_lt_finrank

added theorem dimH_bUnion

added theorem dimH_coe_finset

added theorem dimH_countable

added theorem dimH_def

added theorem dimH_empty

added theorem dimH_finite

added theorem dimH_iUnion

added theorem dimH_image_le_of_locally_holder_on

added theorem dimH_image_le_of_locally_lipschitz_on

added theorem dimH_le

added theorem dimH_le_of_hausdorffMeasure_ne_top

added theorem dimH_mono

added theorem dimH_of_hausdorffMeasure_ne_zero_ne_top

added theorem dimH_range_le_of_locally_holder_on

added theorem dimH_range_le_of_locally_lipschitz_on

added theorem dimH_sUnion

added theorem dimH_singleton

added theorem dimH_subsingleton

added theorem dimH_union

added theorem exists_mem_nhdsWithin_lt_dimH_of_lt_dimH

added theorem hausdorffMeasure_of_dimH_lt

added theorem hausdorffMeasure_of_lt_dimH

added theorem iSup_limsup_dimH

added theorem le_dimH_of_hausdorffMeasure_eq_top

added theorem le_dimH_of_hausdorffMeasure_ne_zero

added theorem measure_zero_of_dimH_lt