Structures · Analysis
ESeminormedAddMonoid
An e-seminormed monoid is an additive monoid endowed with a continuous enorm. Note that we do not ask for the enorm to be positive definite: non-trivial elements may have enorm zero.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds enorm_zero, enorm_add_le
Extends2
Extended by2
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by128
- enorm_zero
- MeasureTheory.Integrable.add
- MeasureTheory.integrable_indicator_iff
- MeasureTheory.MemLp.add
- MeasureTheory.integrable_zero
- MeasureTheory.integrableOn_const
- MeasureTheory.Integrable.indicator
- MeasureTheory.eLpNorm_zero
- enorm_add_le
- MeasureTheory.eLpNorm_add_le
- MeasureTheory.Integrable.smul_measure_nnreal
- MeasureTheory.Integrable.fun_add
- enorm_indicator_eq_indicator_enorm
- MeasureTheory.eLpNorm_indicator_eq_eLpNorm_restrict
- MeasureTheory.Integrable.smul_measure
- MeasureTheory.IntegrableOn.integrable_indicator
- MeasureTheory.MemLp.zero
- MeasureTheory.IntegrableOn.add
- MeasureTheory.integrableOn_singleton
- integrableOn_Icc_iff_integrableOn_Ioc
- MeasureTheory.integrableOn_const_iff
- integrableOn_Ici_iff_integrableOn_Ioi
- MeasureTheory.eLpNorm'_zero
- MeasureTheory.integrable_smul_measure
- MeasureTheory.exists_Lp_half
- MeasureTheory.eLpNorm_indicator_le
- MeasureTheory.eLpNorm_indicator_const
- integrableOn_Icc_iff_integrableOn_Ioo
- MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top
- MeasureTheory.integrableOn_zero
- MeasureTheory.IntegrableOn.indicator
- MeasureTheory.MemLp.indicator
- MeasureTheory.eLpNorm_add_le'
- MeasureTheory.eLpNorm_zero'
- MeasureTheory.IntegrableAtFilter.add
- MeasureTheory.eLpNorm_indicator_const_le
- integrableOn_Ioc_iff_integrableOn_Ioo
- MeasureTheory.Integrable.of_measure_le_smul
- integrableOn_Icc_iff_integrableOn_Ioc'
- integrableOn_Ioc_iff_integrableOn_Ioo'
- MeasureTheory.eLpNormEssSup_indicator_const_le
- MeasureTheory.hasFiniteIntegral_zero
- MeasureTheory.eLpNorm_const_lt_top_iff_enorm
- MeasureTheory.eLpNorm_add_lt_top
- MeasureTheory.LocallyIntegrable.indicator
- MeasureTheory.locallyIntegrable_zero
- MeasureTheory.memLp_indicator_iff_restrict
- MeasureTheory.Integrable.add'
- MeasureTheory.eLpNorm'_add_le
- enorm_add_le_of_le