Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-18 12:53 a7ac6996

View on Github →

feat(topology/metric_space): dimH is the supr of local dimH (#9741)

Estimated changes

Modified src/topology/metric_space/hausdorff_dimension.lean

added theorem bsupr_limsup_dimH

added theorem exists_mem_nhds_within_lt_dimH_of_lt_dimH

added theorem supr_limsup_dimH