Mathlib Map

Theorems · Theorem · functional analysis

MeasureTheory.enorm_le_eLpNorm_count

∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {p : ENNReal} (f : α → ε) (i : α),
  p ≠ 0 → ‖f i‖ₑ ≤ MeasureTheory.eLpNorm f p MeasureTheory.Measure.count
Defined in
Mathlib.MeasureTheory.Function.LpSeminorm.Count
Cited by
1 results in Mathlib
Foundations
Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
MeasurableSpaceMeasurableSingletonClassTopologicalSpaceContinuousENorm
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.eLpNorm_count_lt_top · cited by 0MeasureTheory.eLpNorm_cou…TopologicalSpace · cited by 24529TopologicalSpaceMeasurableSpace · cited by 13106MeasurableSpaceENNReal · cited by 9879ENNRealone_smul · cited by 1374one_smulENorm.enorm · cited by 715ENorm.enormMeasureTheory.eLpNorm · cited by 329MeasureTheory.eLpNormContinuousENorm · cited by 290ContinuousENormMeasurableSingletonClass · cited by 230MeasurableSingletonClassMeasureTheory.Measure.dirac · cited by 210Measure.diracMeasureTheory.Measure.count · cited by 60Measure.countMeasureTheory.Measure.restrict_singleton · cited by 12Measure.restrict_singletonMeasureTheory.Measure.count_singleton' · cited by 10Measure.count_singleton'MeasureTheory.eLpNorm_restrict_le · cited by 2MeasureTheory.eLpNorm_res…MeasureTheory.eLpNorm_dirac · cited by 1MeasureTheory.eLpNorm_dir…MeasureTheory.enorm_le_eLpNor…CITED BYCITES

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by1

Results whose statement or proof uses this declaration.