Mathlib v3 is deprecated. Go to Mathlib v4

Theorem exists_mem_nhds_within_lt_dimH_of_lt_dimH

Modification history

2021-10-18 12:53
src/topology/metric_space/hausdorff_dimension.lean
feat(topology/metric_space): dimH is the supr of local dimH (#9741)
Added exists_mem_nhds_within_lt_dimH_of_lt_dimHView on Github →