Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-14 17:11 1897d7de

View on Github →

feat(measure_theory/covering/liminf_limsup): add lemma blimsup_cthickening_mul_ae_eq (#17803)

Estimated changes

Modified docs/references.bib

Created src/measure_theory/covering/liminf_limsup.lean

added theorem blimsup_cthickening_ae_le_of_eventually_mul_le

added theorem blimsup_cthickening_ae_le_of_eventually_mul_le_aux

added theorem blimsup_cthickening_mul_ae_eq

Modified src/measure_theory/measure/doubling.lean

added theorem is_doubling_measure.eventually_measure_le_scaling_constant_mul'

added theorem is_doubling_measure.eventually_measure_le_scaling_constant_mul

added theorem is_doubling_measure.one_le_scaling_constant_of

Modified src/measure_theory/measure/measure_space_def.lean

added theorem measure_theory.ae_eq_set_union

Modified src/order/filter/basic.lean

added theorem filter.tendsto.if'

Modified src/order/liminf_limsup.lean

added theorem filter.bliminf_congr

added theorem filter.bliminf_eq_supr_binfi_of_nat

added theorem filter.blimsup_congr

added theorem filter.blimsup_eq_infi_bsupr_of_nat

added theorem filter.exists_forall_mem_of_has_basis_mem_blimsup'

added theorem filter.exists_forall_mem_of_has_basis_mem_blimsup

Modified src/topology/metric_space/hausdorff_distance.lean

added theorem is_closed.cthickening_eq_bUnion_closed_ball

added theorem metric.cthickening_eq_bUnion_closed_ball

added theorem metric.cthickening_subset_Union_closed_ball_of_lt

Modified src/topology/order/basic.lean

added theorem filter.tendsto.max_left

added theorem filter.tendsto.max_right

added theorem filter.tendsto.min_left

added theorem filter.tendsto.min_right

added theorem filter.tendsto_nhds_max_left

added theorem filter.tendsto_nhds_max_right

added theorem filter.tendsto_nhds_min_left

added theorem filter.tendsto_nhds_min_right