Structures · Analysis
ContinuousENorm
A type E equipped with a continuous map ‖·‖ₑ : E → ℝ≥0∞
NB. We do not demand that the topology is somehow defined by the enorm:
for ℝ≥0∞ (the motivating example behind this definition), this is not true.
- Defined in
- Mathlib.Analysis.Normed.Group.Defs
- Shape
- One type argument · adds continuous_enorm
Extends1
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 by240
- MeasureTheory.Integrable
- MeasureTheory.IntegrableOn
- MeasureTheory.LocallyIntegrable
- MeasureTheory.Integrable.aestronglyMeasurable
- MeasureTheory.LocallyIntegrableOn
- MeasureTheory.Integrable.integrableOn
- MeasureTheory.memLp_one_iff_integrable
- MeasureTheory.IntegrableAtFilter
- MeasureTheory.IntegrableOn.mono_set
- MeasureTheory.integrable_congr
- MeasureTheory.Integrable.hasFiniteIntegral
- MeasureTheory.AEStronglyMeasurable.enorm
- MeasureTheory.Integrable.congr
- MeasureTheory.Integrable.mono_measure
- MeasureTheory.integrable_map_measure
- MeasureTheory.IntegrableOn.mono
- MeasureTheory.StronglyMeasurable.enorm
- MeasureTheory.integrableOn_union
- MeasureTheory.Integrable.restrict
- MeasureTheory.Integrable.comp_measurable
- MeasureTheory.MemLp.integrable
- MeasureTheory.LocallyIntegrableOn.integrableOn_compact_subset
- MeasureTheory.eLpNorm_mono_measure
- MeasureTheory.IntegrableOn.congr_fun
- continuous_enorm
- MeasureTheory.LocallyIntegrable.integrableOn_isCompact
- MeasureTheory.integrableOn_congr_fun
- MeasureTheory.MemLp.mono_exponent
- MeasureTheory.Integrable.aemeasurable
- MeasureTheory.memLp_map_measure_iff
- MeasureTheory.integrableOn_univ
- MeasureTheory.LocallyIntegrable.locallyIntegrableOn
- MeasureTheory.MeasurePreserving.integrable_comp_emb
- MeasureTheory.LocallyIntegrable.aestronglyMeasurable
- measurable_enorm
- MeasureTheory.IntegrableAtFilter.filter_mono
- MeasureTheory.IntegrableOn.union
- MeasureTheory.AEEqFun.Integrable
- MeasureTheory.IntegrableOn.integrable
- MeasureTheory.locallyIntegrableOn_univ
- MeasurableEmbedding.integrable_map_iff
- MeasureTheory.Integrable.comp_aemeasurable
- MeasureTheory.LocallyIntegrableOn.aestronglyMeasurable
- MeasureTheory.Integrable.add_measure
- MeasureTheory.integrableOn_empty
- MeasurableEmbedding.memLp_map_measure_iff
- MeasureTheory.MemLp.restrict
- MeasurableEmbedding.integrableOn_map_iff
- MeasureTheory.IntegrableOn.congr_fun_ae
- MeasureTheory.memLp_of_memLp_trim