ENNReal

📁 Source: Mathlib/Order/Filter/ENNReal.lean

Statistics

Metric	Count
Definitions	0
Theorems eventually_le_limsup, limsup_add_le, limsup_const_mul, limsup_const_mul_of_ne_top, limsup_eq_zero_iff, limsup_liminf_le_liminf_limsup, limsup_mul_le, ofReal_limsup, toReal_limsup, isBoundedUnder_ge_toReal, isBoundedUnder_le_toReal, isCoboundedUnder_ge_toReal, isCoboundedUnder_le_toReal, liminf_of_not_isCoboundedUnder, limsInf_of_not_isCobounded, limsSup_of_not_isBounded, limsup_of_not_isBoundedUnder, toReal_liminf, toReal_limsup, liminf_of_not_isBoundedUnder, liminf_of_not_isCoboundedUnder, limsInf_of_not_isBounded, limsInf_of_not_isCobounded, limsSup_of_not_isBounded, limsSup_of_not_isCobounded, limsup_of_not_isBoundedUnder, limsup_of_not_isCoboundedUnder	27
Total	27

ENNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_le_limsup 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	eventually_le_limsup instOrderTopology TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace instMetrizableSpace Filter.isBounded_le_of_top
limsup_add_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	sInf_le Filter.Eventually.mp eventually_le_limsup Filter.Eventually.mono add_le_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
limsup_const_mul 📖	mathematical	—	Filter.limsup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	limsup_const_mul_of_ne_top Filter.Eventually.mono MulZeroClass.mul_zero Filter.limsup_congr Filter.limsup_const_bot bot_eq_zero' instCanonicallyOrderedAdd Filter.Frequently.mono Filter.not_eventually Filter.EventuallyEq.eq_1 Pi.zero_apply eq_top_iff Filter.le_limsup_of_frequently_le Filter.isBounded_le_of_top limsup_eq_zero_iff top_mul'
limsup_const_mul_of_ne_top 📖	mathematical	—	Filter.limsup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	MulZeroClass.zero_mul Filter.limsup_const_bot mul_right_strictMono mul_inv_cancel_left OrderIso.limsup_apply Filter.isBounded_le_of_top Filter.isCobounded_le_of_bot
limsup_eq_zero_iff 📖	mathematical	—	Filter.limsup ENNReal ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder instZeroENNReal Filter.EventuallyEq Pi.instZero	—	limsup_eq_bot TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace instMetrizableSpace instOrderTopology
limsup_liminf_le_liminf_limsup 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Filter.liminf	—	eventually_countable_forall eventually_le_limsup sInf_le Filter.Eventually.mono Filter.liminf_le_liminf Filter.Eventually.of_forall Filter.isBounded_ge_of_bot Filter.isCobounded_ge_of_top
limsup_mul_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder instPartialOrder Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiring	—	Filter.limsup_le_limsup Filter.mp_mem eventually_le_limsup Filter.univ_mem' mul_le_mul' IsOrderedMonoid.toMulLeftMono instIsOrderedMonoid covariant_swap_mul_of_covariant_mul le_rfl Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top limsup_const_mul
ofReal_limsup 📖	mathematical	Filter.IsCoboundedUnder Real Real.instLE Filter.IsBoundedUnder	ofReal Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder ENNReal ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder	—	eq_of_forall_le_nnreal_iff Filter.limsup_le_iff Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top Filter.mp_mem Filter.univ_mem' le_total ofReal_of_nonpos bot_eq_zero' instCanonicallyOrderedAdd LT.lt.bot_lt LT.lt.trans_le' toReal_lt_of_lt_ofReal
toReal_limsup 📖	mathematical	Filter.Eventually ENNReal Top.top instTopENNReal Filter.IsBoundedUnder Real Real.instLE toReal	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot instCompleteLinearOrder Real.instConditionallyCompleteLinearOrder	—	Filter.eq_or_neBot Filter.map_bot sInf_univ bot_eq_zero' instCanonicallyOrderedAdd csInf_of_not_bddBelow instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.sInf_empty Filter.IsCoboundedUnder.of_frequently_ge eq_of_forall_ge_iff lt_or_ge LT.lt.not_ge LT.lt.trans_le toReal_nonneg Filter.le_limsup_of_frequently_le le_ofReal_iff_toReal_le Filter.Eventually.exists Filter.eventually_map LE.le.trans Filter.mp_mem Filter.univ_mem' Filter.limsup_le_iff Filter.isCobounded_le_of_bot Filter.isBounded_le_of_top LT.lt.trans_le' toReal_lt_of_lt_ofReal ofReal_lt_coe_iff lt_ofReal_iff_toReal_lt ofReal_coe_nnreal

NNReal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedUnder_ge_toReal 📖	mathematical	—	Filter.IsBoundedUnder Real Real.instLE toReal NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	—	—
isBoundedUnder_le_toReal 📖	mathematical	—	Filter.IsBoundedUnder Real Real.instLE toReal NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	—	Filter.mp_mem Filter.univ_mem'
isCoboundedUnder_ge_toReal 📖	mathematical	—	Filter.IsCoboundedUnder Real Real.instLE toReal NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	—	le_total LE.le.trans
isCoboundedUnder_le_toReal 📖	mathematical	—	Filter.IsCoboundedUnder Real Real.instLE toReal NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	—	LE.le.trans' Filter.Eventually.exists
liminf_of_not_isCoboundedUnder 📖	mathematical	Filter.IsCoboundedUnder NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNNReal	—	limsInf_of_not_isCobounded
limsInf_of_not_isCobounded 📖	mathematical	Filter.IsCobounded NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	Filter.limsInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNNReal	—	Filter.limsInf.eq_1 sSup_of_not_bddAbove
limsSup_of_not_isBounded 📖	mathematical	Filter.IsBounded NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	Filter.limsSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNNReal	—	Filter.limsSup.eq_1 bot_eq_zero sInf_empty
limsup_of_not_isBoundedUnder 📖	mathematical	Filter.IsBoundedUnder NNReal Preorder.toLE PartialOrder.toPreorder instPartialOrderNNReal	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot instZeroNNReal	—	limsSup_of_not_isBounded
toReal_liminf 📖	mathematical	—	Filter.liminf Real ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder toReal NNReal ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	eq_of_forall_le_iff Real.toNNReal_le_iff_le_coe Filter.le_liminf_iff Filter.isBounded_ge_of_bot forall_swap Filter.Eventually.of_forall LT.lt.trans_le le_or_gt Real.liminf_of_not_isCoboundedUnder liminf_of_not_isCoboundedUnder
toReal_limsup 📖	mathematical	—	Filter.limsup Real ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder toReal NNReal ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	Filter.eq_or_neBot Filter.map_bot csInf_of_not_bddBelow instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Real.sInf_empty csInf_univ bot_eq_zero' instCanonicallyOrderedAdd Filter.isCobounded_le_of_bot eq_of_forall_le_iff Real.toNNReal_le_iff_le_coe Filter.le_limsup_iff forall_swap Filter.Frequently.of_forall LT.lt.trans_le le_or_gt Real.limsup_of_not_isBoundedUnder limsup_of_not_isBoundedUnder

Real

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
liminf_of_not_isBoundedUnder 📖	mathematical	Filter.IsBoundedUnder Real instLE	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	limsInf_of_not_isBounded
liminf_of_not_isCoboundedUnder 📖	mathematical	Filter.IsCoboundedUnder Real instLE	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	limsInf_of_not_isCobounded
limsInf_of_not_isBounded 📖	mathematical	Filter.IsBounded Real instLE	Filter.limsInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	Filter.limsInf.eq_1 sSup_empty
limsInf_of_not_isCobounded 📖	mathematical	Filter.IsCobounded Real instLE	Filter.limsInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	Filter.limsInf.eq_1 sSup_of_not_bddAbove
limsSup_of_not_isBounded 📖	mathematical	Filter.IsBounded Real instLE	Filter.limsSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	Filter.limsSup.eq_1 sInf_empty
limsSup_of_not_isCobounded 📖	mathematical	Filter.IsCobounded Real instLE	Filter.limsSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	Filter.limsSup.eq_1 sInf_of_not_bddBelow
limsup_of_not_isBoundedUnder 📖	mathematical	Filter.IsBoundedUnder Real instLE	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	limsSup_of_not_isBounded
limsup_of_not_isCoboundedUnder 📖	mathematical	Filter.IsCoboundedUnder Real instLE	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice instConditionallyCompleteLinearOrder instZero	—	limsSup_of_not_isCobounded

---

← Back to Index