Mathlib v3 is deprecated. Go to Mathlib v4

Theorem measure_theory.norm_indicator_const_Lp_top

Modification history

2022-11-17 13:13

src/measure_theory/function/lp_space.lean

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …

Modified measure_theory.norm_indicator_const_Lp_top View on Github →

2021-07-05 17:24

src/measure_theory/lp_space.lean

feat(measure_theory/lp_space): define the Lp function corresponding to the indicator of a set (#8193) …

Added measure_theory.norm_indicator_const_Lp_top View on Github →