Mathlib v3 is deprecated. Go to Mathlib v4

Theorem bsupr_limsup_dimH

Modification history

2022-10-13 11:47
src/topology/metric_space/hausdorff_dimension.lean
feat(order/liminf_limsup): define `filter.blimsup`, `filter.bliminf` (#16819) …
Modified bsupr_limsup_dimHView on Github →
2022-04-24 20:37
src/topology/metric_space/hausdorff_dimension.lean
refactor(*): migrate from `filter.lift' _ powerset` to `filter.small_sets` (#13673)
Modified bsupr_limsup_dimHView on Github →
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 bsupr_limsup_dimHView on Github →