Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-07 21:13 f3b0295a

View on Github →

chore(measure_theory): use ∞ notation for (⊤ : ℝ≥0∞) (#6080)

Estimated changes

Modified src/measure_theory/bochner_integration.lean

modified theorem measure_theory.integral_to_real

Modified src/measure_theory/borel_space.lean

modified def measurable_equiv.ennreal_equiv_nnreal

Modified src/measure_theory/content.lean

modified theorem measure_theory.outer_measure.of_content_exists_compact

modified theorem measure_theory.outer_measure.of_content_exists_open

Modified src/measure_theory/decomposition.lean

modified theorem measure_theory.hahn_decomposition

Modified src/measure_theory/haar_measure.lean

Modified src/measure_theory/integration.lean

modified theorem measure_theory.ae_lt_top

modified theorem measure_theory.exists_pos_set_lintegral_lt_of_measure_lt

modified theorem measure_theory.exists_simple_func_forall_lintegral_sub_lt_of_pos

modified theorem measure_theory.lintegral_const_mul'

modified theorem measure_theory.lintegral_mul_const'

modified theorem measure_theory.simple_func.fin_meas_supp.iff_lintegral_lt_top

modified theorem measure_theory.simple_func.fin_meas_supp.lintegral_lt_top

modified theorem measure_theory.simple_func.fin_meas_supp.of_lintegral_lt_top

modified theorem measure_theory.tendsto_set_lintegral_zero

Modified src/measure_theory/l1_space.lean

modified def measure_theory.ae_eq_fun.integrable

modified theorem measure_theory.integrable.smul_measure

modified theorem measure_theory.integrable_const_iff

modified theorem measure_theory.l1.lintegral_edist_to_fun_lt_top

Modified src/measure_theory/lp_space.lean

modified theorem measure_theory.Lp.coe_fn_mk

modified theorem measure_theory.Lp.mem_Lp_iff_snorm_lt_top

modified theorem measure_theory.Lp.snorm_lt_top

modified theorem measure_theory.Lp.snorm_ne_top

modified theorem measure_theory.mem_ℒp.snorm_lt_top

modified theorem measure_theory.mem_ℒp.snorm_ne_top

modified theorem measure_theory.snorm'_measure_zero_of_neg

modified theorem measure_theory.snorm_const'

modified theorem measure_theory.snorm_eq_snorm'

modified theorem measure_theory.snorm_exponent_top

Modified src/measure_theory/measure_space.lean

modified theorem is_compact.finite_measure

modified theorem measure_theory.measure.compl_mem_cofinite

modified theorem measure_theory.measure.count_apply_eq_top

modified theorem measure_theory.measure.count_apply_infinite

modified theorem measure_theory.measure.count_apply_lt_top

modified theorem measure_theory.measure.eventually_cofinite

modified def measure_theory.measure.finite_at_filter

modified theorem measure_theory.measure.finite_at_principal

modified theorem measure_theory.measure.mem_cofinite

modified theorem measure_theory.measure_compl

modified theorem measure_theory.measure_lt_top

modified theorem measure_theory.measure_mono_top

modified theorem measure_theory.measure_ne_top

Modified src/measure_theory/outer_measure.lean

modified theorem measure_theory.outer_measure.top_apply

Modified src/measure_theory/prod.lean

Modified src/measure_theory/prod_group.lean

Modified src/measure_theory/set_integral.lean

modified theorem measure_theory.integrable_on_const

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const'

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae''

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae'

modified theorem measure_theory.norm_set_integral_le_of_norm_le_const_ae

Modified src/measure_theory/simple_func_dense.lean