Theorem dimH_iUnion

Modification history

2024-02-04 23:05

Mathlib/Topology/MetricSpace/HausdorffDimension.lean

chore(HausdorffDimension): fix `Encodable`/`Countable` (#10250)

Modified dimH_iUnion View on Github →

2023-06-12 14:52

Mathlib/Topology/MetricSpace/HausdorffDimension.lean

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

Added dimH_iUnion View on Github →