EssSup

📁 Source: Mathlib/MeasureTheory/Function/EssSup.lean

Statistics

Metric	Count
Definitions essInf, essSup	2
Theorems ae_le_essSup, coe_essSup, essSup_add_le, essSup_const_mul, essSup_eq_zero_iff, essSup_indicator_eq_essSup_restrict, essSup_liminf_le, essSup_mul_le, essSup_piecewise, essSup_restrict_eq_of_support_subset, ofReal_essSup, toReal_essSup, essSup_map_measure, essInf_apply, essSup_apply, ae_essInf_le, ae_le_essSup, ae_lt_of_essSup_lt, ae_lt_of_lt_essInf, essInf_antitone_measure, essInf_cond_count_eq_ciInf, essInf_congr_ae, essInf_const, essInf_const', essInf_const_top, essInf_count, essInf_count_eq_ciInf, essInf_eq_ciInf, essInf_eq_iInf, essInf_eq_sSup, essInf_measure_zero, essInf_mono_ae, essSup_comp_le_essSup_map_measure, essSup_congr_ae, essSup_const, essSup_const', essSup_const_bot, essSup_count, essSup_count_eq_ciSup, essSup_ennreal_smul_measure, essSup_eq_ciSup, essSup_eq_iSup, essSup_eq_sInf, essSup_le_of_ae_le, essSup_map_measure, essSup_map_measure_of_measurable, essSup_measure_zero, essSup_mono_ae, essSup_mono_measure, essSup_mono_measure', essSup_smul_measure, essSup_uniformOn_eq_ciSup, le_essInf_of_ae_le, meas_essSup_lt, meas_lt_essInf	55
Total	57

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_le_essSup 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	eventually_le_limsup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
coe_essSup 📖	mathematical	Filter.IsBoundedUnder NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	ofNNReal essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder NNReal.instConditionallyCompleteLinearOrderBot ENNReal CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	MeasureTheory.Measure.instOuterMeasureClass coe_sInf eq_of_forall_le_iff
essSup_add_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	limsup_add_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
essSup_const_mul 📖	mathematical	—	essSup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	limsup_const_mul MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
essSup_eq_zero_iff 📖	mathematical	—	essSup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder instZeroENNReal Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Pi.instZero	—	limsup_eq_zero_iff MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
essSup_indicator_eq_essSup_restrict 📖	mathematical	MeasurableSet	essSup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Set.indicator instZeroENNReal MeasureTheory.Measure.restrict	—	essSup_piecewise Eq.trans_le MeasureTheory.Measure.instOuterMeasureClass Filter.limsup_const_bot zero_le instCanonicallyOrderedAdd
essSup_liminf_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Filter.liminf Filter.atTop	—	limsup_liminf_le_liminf_limsup MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
essSup_mul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	limsup_mul_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.instCountableInterFilter
essSup_piecewise 📖	mathematical	MeasurableSet	essSup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Set.piecewise instMax MeasureTheory.Measure.restrict Compl.compl Set Set.instCompl	—	MeasureTheory.Measure.instOuterMeasureClass Filter.limsup_piecewise Filter.blimsup_eq_limsup MeasureTheory.ae_restrict_eq MeasurableSet.compl
essSup_restrict_eq_of_support_subset 📖	mathematical	Set Set.instHasSubset Function.support ENNReal instZeroENNReal	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder MeasureTheory.Measure.restrict	—	le_antisymm essSup_mono_measure' MeasureTheory.Measure.restrict_le_self le_of_forall_lt exists_between instDenselyOrdered MeasureTheory.Measure.restrict_apply_self notMem_of_lt_csInf essSup_eq_sInf OrderBot.bddBelow bot_lt_iff_ne_bot MeasureTheory.Measure.restrict_mono subset_trans Set.instIsTransSubset LT.lt.ne' lt_of_le_of_lt bot_le le_rfl lt_of_lt_of_le LT.lt.trans_le le_sInf Mathlib.Tactic.Contrapose.contrapose₁ ne_of_gt MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass LT.lt.trans
ofReal_essSup 📖	mathematical	Filter.IsCoboundedUnder Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.IsBoundedUnder	ofReal essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder ENNReal ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	MeasureTheory.Measure.instOuterMeasureClass ofReal_limsup
toReal_essSup 📖	mathematical	Filter.Eventually ENNReal Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass Filter.IsBoundedUnder Real Real.instLE toReal	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Real.instConditionallyCompleteLinearOrder	—	MeasureTheory.Measure.instOuterMeasureClass eq_zero_or_neZero MeasureTheory.ae_zero Filter.map_bot sInf_univ bot_eq_zero' instCanonicallyOrderedAdd csInf_of_not_bddBelow instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.sInf_empty toReal_limsup

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essSup_map_measure 📖	mathematical	MeasurableEmbedding	essSup CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure.map	—	le_antisymm Filter.limsSup_le_limsSup MeasureTheory.Measure.instOuterMeasureClass Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.eventually_map ae_map_iff essSup_comp_le_essSup_map_measure Measurable.aemeasurable measurable

OrderIso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essInf_apply 📖	mathematical	—	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLikeOrderIso essInf CompleteLattice.toConditionallyCompleteLattice	—	essSup_apply
essSup_apply 📖	mathematical	—	DFunLike.coe OrderIso Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder instFunLikeOrderIso essSup CompleteLattice.toConditionallyCompleteLattice	—	limsup_apply MeasureTheory.Measure.instOuterMeasureClass Filter.isBounded_le_of_top Filter.isCobounded_le_of_bot

(root)

Definitions

Name	Category	Theorems
essInf 📖	CompOp	17 math math: essInf_const', essInf_eq_ciInf, essInf_measure_zero, essInf_count, essInf_antitone_measure, essInf_const_top, essInf_eq_sSup, OrderIso.essInf_apply, essInf_mono_ae, essInf_congr_ae, essInf_count_eq_ciInf, essInf_eq_iInf, essInf_cond_count_eq_ciInf, ae_essInf_le, meas_lt_essInf, essInf_const, le_essInf_of_ae_le
essSup 📖	CompOp	45 math math: essSup_le_of_ae_le, essSup_const', meas_essSup_lt, essSup_const, OrderIso.essSup_apply, essSup_ennreal_smul_measure, essSup_map_measure, MeasurableEmbedding.essSup_map_measure, ENNReal.essSup_add_le, ENNReal.essSup_const_mul, MeasureTheory.essSup_trim, essSup_map_measure_of_measurable, essSup_const_bot, essSup_eq_sInf, essSup_comp_quotientAddGroup_mk, ae_le_essSup, ENNReal.essSup_piecewise, MeasureTheory.IsAddFundamentalDomain.essSup_measure_restrict, ENNReal.coe_essSup, ENNReal.essSup_liminf_le, essSup_mono_measure, essSup_eq_iSup, MeasureTheory.eLpNormEssSup_eq_essSup_enorm, essSup_measure_zero, essSup_uniformOn_eq_ciSup, ENNReal.ofReal_essSup, essSup_comp_quotientGroup_mk, MeasureTheory.IsFundamentalDomain.essSup_measure_restrict, essSup_count_eq_ciSup, ENNReal.toReal_essSup, ENNReal.essSup_mul_le, essSup_count, ENNReal.essSup_indicator_eq_essSup_restrict, essSup_comp_le_essSup_map_measure, ENNReal.essSup_restrict_eq_of_support_subset, MeasureTheory.Lp.eLpNorm_exponent_top_lim_eq_essSup_liminf, essSup_smul_measure, essSup_mono_ae, essSup_congr_ae, essSup_mono_measure', MeasureTheory.lpNorm_exponent_top_eq_essSup, essSup_eq_ciSup, ProbabilityTheory.IdentDistrib.essSup_eq, ENNReal.essSup_eq_zero_iff, ENNReal.ae_le_essSup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_essInf_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually essInf	—	MeasureTheory.Measure.instOuterMeasureClass eventually_liminf_le MeasureTheory.instCountableInterFilter
ae_le_essSup 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually essSup	—	MeasureTheory.Measure.instOuterMeasureClass eventually_le_limsup MeasureTheory.instCountableInterFilter
ae_lt_of_essSup_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice essSup Filter.IsBoundedUnder Preorder.toLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventually_lt_of_limsup_lt
ae_lt_of_lt_essInf 📖	mathematical	Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice essInf Filter.IsBoundedUnder Preorder.toLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.Eventually	—	MeasureTheory.Measure.instOuterMeasureClass Filter.eventually_lt_of_lt_liminf
essInf_antitone_measure 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder essInf CompleteLattice.toConditionallyCompleteLattice	—	Filter.liminf_le_liminf_of_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_le_iff_absolutelyContinuous Filter.isBounded_ge_of_bot Filter.isCobounded_ge_of_top
essInf_cond_count_eq_ciInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essInf ProbabilityTheory.uniformOn Set.univ iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	essInf_eq_ciInf ProbabilityTheory.cond_apply MeasureTheory.Measure.count_univ Set.inter_singleton_of_mem MeasureTheory.Measure.count_singleton' mul_one
essInf_congr_ae 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essInf	—	MeasureTheory.Measure.instOuterMeasureClass essSup_congr_ae
essInf_const 📖	mathematical	—	essInf	—	essInf_const'
essInf_const' 📖	mathematical	—	essInf	—	Filter.liminf_const MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae.neBot
essInf_const_top 📖	mathematical	—	essInf CompleteLattice.toConditionallyCompleteLattice Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Filter.liminf_const_top MeasureTheory.Measure.instOuterMeasureClass
essInf_count 📖	mathematical	—	essInf CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure.count iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	—	essInf_eq_iInf MeasureTheory.Measure.count_singleton' NeZero.charZero_one ENNReal.instCharZero
essInf_count_eq_ciInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essInf MeasureTheory.Measure.count iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	essInf_eq_ciInf MeasureTheory.Measure.count_singleton' NeZero.charZero_one ENNReal.instCharZero
essInf_eq_ciInf 📖	mathematical	BddBelow Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essInf iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf	—	MeasureTheory.Measure.instOuterMeasureClass essInf.eq_1 MeasureTheory.ae_eq_top Filter.liminf_top_eq_ciInf
essInf_eq_iInf 📖	mathematical	—	essInf CompleteLattice.toConditionallyCompleteLattice iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	—	MeasureTheory.Measure.instOuterMeasureClass essInf.eq_1 MeasureTheory.ae_eq_top Filter.liminf_top_eq_iInf
essInf_eq_sSup 📖	mathematical	—	essInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice SupSet.sSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder setOf ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass
essInf_measure_zero 📖	mathematical	—	essInf CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure MeasureTheory.Measure.instZero Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	essSup_measure_zero
essInf_mono_ae 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essInf CompleteLattice.toConditionallyCompleteLattice	—	MeasureTheory.Measure.instOuterMeasureClass Filter.liminf_le_liminf Filter.isBounded_ge_of_bot Filter.isCobounded_ge_of_top
essSup_comp_le_essSup_map_measure 📖	mathematical	AEMeasurable	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder essSup CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure.map	—	Filter.limsSup_le_limsSup_of_le MeasureTheory.Measure.instOuterMeasureClass Filter.map_map Filter.map_mono MeasureTheory.Measure.tendsto_ae_map Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top
essSup_congr_ae 📖	mathematical	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essSup	—	MeasureTheory.Measure.instOuterMeasureClass Filter.limsup_congr
essSup_const 📖	mathematical	—	essSup	—	essSup_const'
essSup_const' 📖	mathematical	—	essSup	—	Filter.limsup_const MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae.neBot
essSup_const_bot 📖	mathematical	—	essSup CompleteLattice.toConditionallyCompleteLattice Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Filter.limsup_const_bot MeasureTheory.Measure.instOuterMeasureClass
essSup_count 📖	mathematical	—	essSup CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure.count iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	—	essSup_eq_iSup MeasureTheory.Measure.count_singleton' NeZero.charZero_one ENNReal.instCharZero
essSup_count_eq_ciSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essSup MeasureTheory.Measure.count iSup ConditionallyCompletePartialOrderSup.toSupSet	—	essSup_eq_ciSup MeasureTheory.Measure.count_singleton' NeZero.charZero_one ENNReal.instCharZero
essSup_ennreal_smul_measure 📖	mathematical	—	essSup ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_ennreal_smul_measure_eq
essSup_eq_ciSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essSup iSup ConditionallyCompletePartialOrderSup.toSupSet	—	MeasureTheory.Measure.instOuterMeasureClass essSup.eq_1 MeasureTheory.ae_eq_top Filter.limsup_top_eq_ciSup
essSup_eq_iSup 📖	mathematical	—	essSup CompleteLattice.toConditionallyCompleteLattice iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	—	MeasureTheory.Measure.instOuterMeasureClass essSup.eq_1 MeasureTheory.ae_eq_top Filter.limsup_top_eq_iSup
essSup_eq_sInf 📖	mathematical	—	essSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder setOf ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass
essSup_le_of_ae_le 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essSup CompleteLattice.toConditionallyCompleteLattice	—	MeasureTheory.Measure.instOuterMeasureClass Filter.limsup_le_of_le Filter.isCobounded_le_of_bot
essSup_map_measure 📖	mathematical	AEMeasurable MeasureTheory.Measure.map	essSup CompleteLattice.toConditionallyCompleteLattice	—	essSup_congr_ae essSup_map_measure_of_measurable MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_of_ae_map Filter.EventuallyEq.symm Filter.EventuallyEq.eq_1
essSup_map_measure_of_measurable 📖	mathematical	Measurable AEMeasurable	essSup CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure.map	—	le_antisymm Filter.limsSup_le_limsSup MeasureTheory.Measure.instOuterMeasureClass Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.eventually_map MeasureTheory.ae_map_iff measurableSet_le measurable_const essSup_comp_le_essSup_map_measure
essSup_measure_zero 📖	mathematical	—	essSup CompleteLattice.toConditionallyCompleteLattice MeasureTheory.Measure MeasureTheory.Measure.instZero Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	le_bot_iff sInf_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_zero Filter.map_bot
essSup_mono_ae 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essSup CompleteLattice.toConditionallyCompleteLattice	—	MeasureTheory.Measure.instOuterMeasureClass Filter.limsup_le_limsup Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top
essSup_mono_measure 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous	Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder essSup CompleteLattice.toConditionallyCompleteLattice	—	Filter.limsup_le_limsup_of_le MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_le_iff_absolutelyContinuous Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top
essSup_mono_measure' 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder	OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder essSup CompleteLattice.toConditionallyCompleteLattice	—	essSup_mono_measure MeasureTheory.Measure.absolutelyContinuous_of_le
essSup_smul_measure 📖	mathematical	—	essSup MeasureTheory.Measure MeasureTheory.Measure.instSMul SMulZeroClass.toSMul ENNReal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ENNReal.instAddCommMonoid	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.ae_smul_measure_eq
essSup_uniformOn_eq_ciSup 📖	mathematical	BddAbove Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder Set.range	essSup ProbabilityTheory.uniformOn Set.univ iSup ConditionallyCompletePartialOrderSup.toSupSet	—	essSup_eq_ciSup ProbabilityTheory.cond_apply MeasureTheory.Measure.count_univ Set.inter_singleton_of_mem MeasureTheory.Measure.count_singleton' mul_one
le_essInf_of_ae_le 📖	mathematical	Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	essInf CompleteLattice.toConditionallyCompleteLattice	—	MeasureTheory.Measure.instOuterMeasureClass essSup_le_of_ae_le
meas_essSup_lt 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	DFunLike.coe Set ENNReal setOf Preorder.toLT essSup instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass ae_le_essSup
meas_lt_essInf 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	DFunLike.coe Set ENNReal setOf Preorder.toLT essInf instZeroENNReal	—	MeasureTheory.Measure.instOuterMeasureClass ae_essInf_le

---

← Back to Index