Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-27 13:50 f5d2cc8f

View on Github →

feat(measure_theory/function/l1_space): add some integrability lemmas (#14931)

Estimated changes

Modified src/analysis/normed_space/lattice_ordered_group.lean

added theorem norm_inf_le_add

added theorem norm_sup_le_add

Modified src/measure_theory/function/l1_space.lean

modified theorem measure_theory.integrable.abs

added theorem measure_theory.integrable.bdd_mul

added theorem measure_theory.integrable.inf

added theorem measure_theory.integrable.sup

Modified src/measure_theory/function/lp_order.lean

added theorem measure_theory.mem_ℒp.abs

added theorem measure_theory.mem_ℒp.inf

added theorem measure_theory.mem_ℒp.sup