Commit 2023-08-23 11:25 4c583ce7

View on Github →

feat: lemmas about indicator of the symmetric difference (#6738)

Estimated changes

Modified Mathlib/Algebra/IndicatorFunction.lean

added theorem Set.abs_indicator_symmDiff

added theorem Set.apply_mulIndicator_symmDiff

added theorem Set.mulIndicator_symmDiff

Modified Mathlib/Analysis/Normed/Group/Basic.lean

added theorem dist_mulIndicator

added theorem edist_mulIndicator

added theorem nndist_mulIndicator

Modified Mathlib/MeasureTheory/Function/LpSeminorm.lean

added theorem MeasureTheory.snorm_indicator_sub_indicator

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

added theorem MeasureTheory.Lp.coe_nnnorm_toLp

added theorem MeasureTheory.dist_indicatorConstLp_eq_norm

added theorem MeasureTheory.edist_indicatorConstLp_eq_nnnorm

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.measure_symmDiff_ne_top