Theorem enorm_indicator_le_of_subset

Modification history

2025-03-07 15:46
Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
chore(Analysis/Normed/Group/IndicatorFunction): generalise to enorm (#22690) …
Modified enorm_indicator_le_of_subsetView on Github →
2025-02-04 15:53
Mathlib/Analysis/NormedSpace/IndicatorFunction.lean
chore: generalise lemmas to `ENorm` spaces, part 1 (#21380) …
Added enorm_indicator_le_of_subsetView on Github →