Trim

📁 Source: Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean

Statistics

Metric	Count
Definitions	0
Theorems eLpNorm'_trim, eLpNormEssSup_trim, eLpNorm_trim, eLpNorm_trim_ae, essSup_trim, limsup_trim, memLp_of_memLp_trim	7
Total	7

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eLpNorm'_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE StronglyMeasurable	eLpNorm' ContinuousENorm.toENorm Measure.trim	—	lintegral_trim Measurable.pow_const ENNReal.hasMeasurablePow StronglyMeasurable.enorm
eLpNormEssSup_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE StronglyMeasurable	eLpNormEssSup ContinuousENorm.toENorm Measure.trim	—	essSup_trim StronglyMeasurable.enorm
eLpNorm_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE StronglyMeasurable	eLpNorm ContinuousENorm.toENorm Measure.trim	—	eLpNorm_exponent_zero eLpNorm_exponent_top eLpNormEssSup_trim eLpNorm_eq_eLpNorm' eLpNorm'_trim
eLpNorm_trim_ae 📖	mathematical	MeasurableSpace MeasurableSpace.instLE AEStronglyMeasurable Measure.trim	eLpNorm ContinuousENorm.toENorm	—	eLpNorm_congr_ae ae_eq_of_ae_eq_trim eLpNorm_trim
essSup_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Measure.trim	—	limsup_trim
limsup_trim 📖	mathematical	MeasurableSpace MeasurableSpace.instLE Measurable ENNReal ENNReal.measurableSpace	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.trim	—	Measure.instOuterMeasureClass Set.ext trim_measurableSet_eq MeasurableSet.compl measurableSet_le BorelSpace.opensMeasurable ENNReal.borelSpace OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.instSecondCountableTopology measurable_const
memLp_of_memLp_trim 📖	—	MeasurableSpace MeasurableSpace.instLE MemLp ContinuousENorm.toENorm Measure.trim	—	—	aestronglyMeasurable_of_aestronglyMeasurable_trim LE.le.trans_lt le_of_eq eLpNorm_trim_ae

---

← Back to Index