Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.cthickening_subset_Union_closed_ball_of_lt

Modification history

2022-12-14 17:11
src/topology/metric_space/hausdorff_distance.lean
feat(measure_theory/covering/liminf_limsup): add lemma `blimsup_cthickening_mul_ae_eq` (#17803)
Added metric.cthickening_subset_Union_closed_ball_of_ltView on Github →