LiminfLimsup

📁 Source: Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Statistics

Metric	Count
Definitions	0
Theorems le_liminf_add, le_liminf_mul, le_limsup_add, le_limsup_mul, liminf_add_const, liminf_add_le, liminf_const_add, liminf_const_sub, liminf_mul_le, liminf_sub_const, limsup_add_const, limsup_add_le, limsup_const_add, limsup_const_sub, limsup_mul_le, limsup_sub_const	16
Total	16

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_liminf_add 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Filter.liminf Pi.instAdd	—	Filter.isCoboundedUnder_ge_add covariant_swap_add_of_covariant_add Filter.isBoundedUnder_ge_add add_le_of_forall_lt Filter.le_liminf_iff Filter.mp_mem Filter.eventually_lt_of_lt_liminf Filter.univ_mem' LT.lt.trans add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
le_liminf_mul 📖	mathematical	Filter.EventuallyLE Real Real.instLE Pi.instZero Real.instZero Filter.IsBoundedUnder Filter.IsCoboundedUnder	Real.instMul Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder Pi.instMul	—	Filter.isCoboundedUnder_ge_mul_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Filter.isBoundedUnder_of_eventually_ge Filter.Eventually.mono Filter.Eventually.and mul_nonneg mul_le_of_forall_lt_of_nonneg Real.instIsStrictOrderedRing Filter.le_liminf_of_le Filter.IsBoundedUnder.isCoboundedUnder_ge Filter.le_liminf_iff Filter.mp_mem Filter.eventually_lt_of_lt_liminf Filter.univ_mem' LT.lt.trans_le mul_le_mul LT.lt.le LE.le.trans
le_limsup_add 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Filter.limsup Filter.liminf Pi.instAdd	—	Filter.isCoboundedUnder_le_add covariant_swap_add_of_covariant_add Filter.isBoundedUnder_le_add add_le_of_forall_lt Filter.le_limsup_iff add_comm Filter.Frequently.mono Filter.Frequently.and_eventually Filter.frequently_lt_of_lt_limsup Filter.eventually_lt_of_lt_liminf LT.lt.trans add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
le_limsup_mul 📖	mathematical	Filter.Frequently Real Real.instLE Real.instZero Filter.IsBoundedUnder Filter.EventuallyLE Pi.instZero	Real.instMul Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder Filter.liminf Pi.instMul	—	Filter.IsCoboundedUnder.of_frequently_ge Filter.Frequently.mono Filter.Frequently.and_eventually mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Filter.isBoundedUnder_le_mul_of_nonneg IsOrderedRing.toMulPosMono Filter.le_limsup_of_frequently_le mul_le_of_forall_lt_of_nonneg Real.instIsStrictOrderedRing Filter.le_limsup_iff Filter.frequently_lt_of_lt_limsup Filter.eventually_lt_of_lt_liminf Filter.isBoundedUnder_of_eventually_ge Filter.Eventually.and LT.lt.trans_le mul_le_mul LT.lt.le LE.le.trans
liminf_add_const 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsBoundedUnder	Filter.liminf	—	Monotone.map_limsInf_of_continuousAt Filter.map_neBot add_le_add_left Continuous.continuousAt continuous_add_right
liminf_add_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.liminf Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid Filter.limsup	—	Filter.isCoboundedUnder_ge_add covariant_swap_add_of_covariant_add Filter.isBoundedUnder_ge_add le_add_of_forall_lt Filter.liminf_le_iff Filter.Frequently.mono Filter.Frequently.and_eventually Filter.frequently_lt_of_liminf_lt Filter.eventually_lt_of_limsup_lt LT.lt.trans add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
liminf_const_add 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsBoundedUnder	Filter.liminf	—	Monotone.map_limsInf_of_continuousAt Filter.map_neBot add_le_add_right Continuous.continuousAt continuous_add_left
liminf_const_sub 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.liminf Filter.limsup	—	Antitone.map_limsSup_of_continuousAt Filter.map_neBot tsub_le_tsub_left Continuous.continuousAt continuous_sub_left
liminf_mul_le 📖	mathematical	Filter.EventuallyLE Real Real.instLE Pi.instZero Real.instZero Filter.IsBoundedUnder Filter.IsCoboundedUnder	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder Pi.instMul Real.instMul Filter.limsup	—	Filter.isCoboundedUnder_ge_mul_of_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono Filter.isBoundedUnder_of_eventually_ge Filter.Eventually.mono Filter.Eventually.and mul_nonneg le_mul_of_forall_lt₀ Real.instIsStrictOrderedRing Filter.liminf_le_iff Filter.Frequently.mono Filter.Frequently.and_eventually Filter.frequently_lt_of_liminf_lt Filter.eventually_lt_of_limsup_lt LE.le.trans_lt mul_le_mul LT.lt.le LE.le.trans
liminf_sub_const 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsBoundedUnder	Filter.liminf	—	Monotone.map_limsInf_of_continuousAt Filter.map_neBot tsub_le_tsub_right Continuous.continuousAt continuous_sub_right
limsup_add_const 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.limsup	—	Monotone.map_limsSup_of_continuousAt Filter.map_neBot add_le_add_left Continuous.continuousAt continuous_add_right
limsup_add_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.limsup Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	Filter.isCoboundedUnder_le_add covariant_swap_add_of_covariant_add Filter.isBoundedUnder_le_add le_add_of_forall_lt Filter.limsup_le_iff Filter.mp_mem Filter.eventually_lt_of_limsup_lt Filter.univ_mem' LT.lt.trans add_lt_add IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd
limsup_const_add 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.limsup	—	Monotone.map_limsSup_of_continuousAt Filter.map_neBot add_le_add_right Continuous.continuousAt continuous_add_left
limsup_const_sub 📖	mathematical	Filter.IsCoboundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsBoundedUnder	Filter.limsup Filter.liminf	—	Filter.eq_or_neBot Filter.map_bot LE.le.antisymm csInf_le mem_lowerBounds tsub_le_iff_tsub_le Set.mem_univ le_csSup mem_upperBounds Antitone.map_limsInf_of_continuousAt Filter.map_neBot tsub_le_tsub_left Continuous.continuousAt continuous_sub_left
limsup_mul_le 📖	mathematical	Filter.Frequently Real Real.instLE Real.instZero Filter.IsBoundedUnder Filter.EventuallyLE Pi.instZero	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Real.instConditionallyCompleteLinearOrder Pi.instMul Real.instMul	—	Filter.IsCoboundedUnder.of_frequently_ge Filter.Frequently.mono Filter.Frequently.and_eventually mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing Filter.isBoundedUnder_le_mul_of_nonneg IsOrderedRing.toMulPosMono le_mul_of_forall_lt₀ Real.instIsStrictOrderedRing Filter.limsup_le_iff Filter.mp_mem Filter.eventually_lt_of_limsup_lt Filter.univ_mem' lt_of_le_of_lt lt_or_ge LE.le.trans mul_nonpos_of_nonpos_of_nonneg LT.lt.le Filter.le_limsup_of_frequently_le mul_le_mul
limsup_sub_const 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsCoboundedUnder	Filter.limsup	—	Filter.eq_or_neBot csInf_le Filter.map_bot mem_lowerBounds Set.mem_univ LE.le.antisymm tsub_le_iff_right Monotone.map_limsSup_of_continuousAt Filter.map_neBot tsub_le_tsub_right Continuous.continuousAt continuous_sub_right

---

← Back to Index