LiminfLimsup

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

Statistics

Metric	Count
Definitions BoundedGENhdsClass, BoundedLENhdsClass	2
Theorems map_liminf_of_continuousAt, map_limsInf_of_continuousAt, map_limsSup_of_continuousAt, map_limsup_of_continuousAt, isBounded_ge_nhds, of_closedIicTopology, isBounded_le_nhds, of_closedIciTopology, bddAbove_range, bddAbove_range_of_cofinite, bddBelow_range, bddBelow_range_of_cofinite, isBoundedUnder_ge, isBoundedUnder_le, isCoboundedUnder_ge, isCoboundedUnder_le, liminf_eq, limsup_eq, map_liminf_of_continuousAt, map_limsInf_of_continuousAt, map_limsSup_of_continuousAt, map_limsup_of_continuousAt, to_BoundedGENhdsClass, to_BoundedLENhdsClass, instBoundedGENhdsClass, instBoundedLENhdsClass, instBoundedGENhdsClass, instBoundedLENhdsClass, eventually_le_limsup, eventually_liminf_le, instBoundedGENhdsClassOrderDual, instBoundedLENhdsClassOrderDual, isBounded_ge_nhds, isBounded_le_nhds, isCobounded_ge_nhds, isCobounded_le_nhds, le_nhds_of_limsSup_eq_limsInf, liminf_eq_top, limsInf_eq_of_le_nhds, limsInf_nhds, limsSup_eq_of_le_nhds, limsSup_nhds, limsup_eq_bot, tendsto_of_le_liminf_of_limsup_le, tendsto_of_liminf_eq_limsup, tendsto_of_no_upcrossings	46
Total	48

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_liminf_of_continuousAt 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.liminf Filter.IsCoboundedUnder Preorder.toLE Filter.IsBoundedUnder	Filter.limsup	—	map_limsInf_of_continuousAt Filter.map_neBot
map_limsInf_of_continuousAt 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsInf Filter.IsCobounded Preorder.toLE Filter.IsBounded	Filter.limsup	—	map_limsSup_of_continuousAt instOrderTopologyOrderDual dual
map_limsSup_of_continuousAt 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsSup Filter.IsBounded Preorder.toLE Filter.IsCobounded	Filter.liminf	—	le_antisymm Filter.limsSup.eq_1 map_csInf_of_continuousAt OrderTopology.to_orderClosedTopology le_of_forall_lt exists_lt_of_lt_csSup Set.mem_image_of_mem lt_csSup_of_lt isCoboundedUnder_ge_of_isCobounded Filter.mp_mem Filter.univ_mem' Filter.Frequently.mono Filter.frequently_lt_of_lt_limsSup Filter.liminf_le_of_frequently_le Filter.IsBounded.isBoundedUnder lt_irrefl lt_of_le_of_lt Filter.Frequently.of_forall exists_Ioc_subset_of_mem_nhds tendsto_order ContinuousAt.tendsto Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq Mathlib.Tactic.Push.not_and_eq LT.lt.le LE.le.trans_lt
map_limsup_of_continuousAt 📖	mathematical	Antitone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsup Filter.IsBoundedUnder Preorder.toLE Filter.IsCoboundedUnder	Filter.liminf	—	map_limsSup_of_continuousAt Filter.map_neBot

BoundedGENhdsClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_ge_nhds 📖	mathematical	—	Filter.IsBounded Preorder.toLE nhds	—	—
of_closedIicTopology 📖	mathematical	—	BoundedGENhdsClass PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	instBoundedGENhdsClassOrderDual BoundedLENhdsClass.of_closedIciTopology instClosedIciTopologyOrderDual

BoundedLENhdsClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBounded_le_nhds 📖	mathematical	—	Filter.IsBounded Preorder.toLE nhds	—	—
of_closedIciTopology 📖	mathematical	—	BoundedLENhdsClass PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	isTop_or_exists_gt SemilatticeSup.instIsDirectedOrder Filter.Eventually.of_forall eventually_le_nhds

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bddAbove_range 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds	BddAbove Preorder.toLE Set.range	—	Filter.IsBoundedUnder.bddAbove_range isBoundedUnder_le
bddAbove_range_of_cofinite 📖	mathematical	Filter.Tendsto Filter.cofinite nhds	BddAbove Preorder.toLE Set.range	—	Filter.IsBoundedUnder.bddAbove_range_of_cofinite isBoundedUnder_le
bddBelow_range 📖	mathematical	Filter.Tendsto Filter.atTop Nat.instPreorder nhds	BddBelow Preorder.toLE Set.range	—	Filter.IsBoundedUnder.bddBelow_range isBoundedUnder_ge
bddBelow_range_of_cofinite 📖	mathematical	Filter.Tendsto Filter.cofinite nhds	BddBelow Preorder.toLE Set.range	—	Filter.IsBoundedUnder.bddBelow_range_of_cofinite isBoundedUnder_ge
isBoundedUnder_ge 📖	mathematical	Filter.Tendsto nhds	Filter.IsBoundedUnder Preorder.toLE	—	Filter.IsBounded.mono isBounded_ge_nhds
isBoundedUnder_le 📖	mathematical	Filter.Tendsto nhds	Filter.IsBoundedUnder Preorder.toLE	—	Filter.IsBounded.mono isBounded_le_nhds
isCoboundedUnder_ge 📖	mathematical	Filter.Tendsto nhds	Filter.IsCoboundedUnder Preorder.toLE	—	Filter.IsBounded.isCobounded_flip instIsTransLe Filter.map_neBot isBoundedUnder_le
isCoboundedUnder_le 📖	mathematical	Filter.Tendsto nhds	Filter.IsCoboundedUnder Preorder.toLE	—	Filter.IsBounded.isCobounded_flip instIsTransGe Filter.map_neBot isBoundedUnder_ge
liminf_eq 📖	mathematical	Filter.Tendsto nhds	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	limsInf_eq_of_le_nhds Filter.map_neBot
limsup_eq 📖	mathematical	Filter.Tendsto nhds	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	limsSup_eq_of_le_nhds Filter.map_neBot

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_liminf_of_continuousAt 📖	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.liminf Filter.IsCoboundedUnder Preorder.toLE Filter.IsBoundedUnder	—	—	map_limsInf_of_continuousAt Filter.map_neBot
map_limsInf_of_continuousAt 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsInf Filter.IsCobounded Preorder.toLE Filter.IsBounded	Filter.liminf	—	Antitone.map_limsSup_of_continuousAt instOrderTopologyOrderDual dual
map_limsSup_of_continuousAt 📖	mathematical	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsSup Filter.IsBounded Preorder.toLE Filter.IsCobounded	Filter.limsup	—	Antitone.map_limsSup_of_continuousAt instOrderTopologyOrderDual
map_limsup_of_continuousAt 📖	—	Monotone PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ContinuousAt Filter.limsup Filter.IsBoundedUnder Preorder.toLE Filter.IsCoboundedUnder	—	—	map_limsSup_of_continuousAt Filter.map_neBot

OrderBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_BoundedGENhdsClass 📖	mathematical	—	BoundedGENhdsClass	—	Filter.isBounded_ge_of_bot

OrderTop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_BoundedLENhdsClass 📖	mathematical	—	BoundedLENhdsClass	—	Filter.isBounded_le_of_top

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBoundedGENhdsClass 📖	mathematical	BoundedGENhdsClass	preorder topologicalSpace	—	BoundedLENhdsClass.isBounded_le_nhds instBoundedLENhdsClass instBoundedLENhdsClassOrderDual
instBoundedLENhdsClass 📖	mathematical	BoundedLENhdsClass	preorder topologicalSpace	—	nhds_pi Filter.eventually_pi isBounded_le_nhds

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instBoundedGENhdsClass 📖	mathematical	—	BoundedGENhdsClass instPreorder instTopologicalSpaceProd	—	BoundedLENhdsClass.isBounded_le_nhds instBoundedLENhdsClass instBoundedLENhdsClassOrderDual
instBoundedLENhdsClass 📖	mathematical	—	BoundedLENhdsClass instPreorder instTopologicalSpaceProd	—	isBounded_le_nhds nhds_prod_eq

(root)

Definitions

Name	Category	Theorems
BoundedGENhdsClass 📖	CompData	4 math math: instBoundedGENhdsClassOrderDual, OrderBot.to_BoundedGENhdsClass, Prod.instBoundedGENhdsClass, BoundedGENhdsClass.of_closedIicTopology
BoundedLENhdsClass 📖	CompData	4 math math: BoundedLENhdsClass.of_closedIciTopology, Prod.instBoundedLENhdsClass, instBoundedLENhdsClassOrderDual, OrderTop.to_BoundedLENhdsClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_le_limsup 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Eventually Filter.limsup	—	isTop_or_exists_gt SemilatticeSup.instIsDirectedOrder Filter.Eventually.of_forall IsGLB.exists_seq_antitone_tendsto FirstCountableTopology.nhds_generated_countable Filter.eventually_lt_of_limsup_lt Filter.Eventually.mono eventually_countable_forall instCountableNat ge_of_tendsto instClosedIciTopology OrderTopology.to_orderClosedTopology Filter.atTop_neBot LT.lt.le le_of_lt Filter.mp_mem Filter.univ_mem' Mathlib.Tactic.Contrapose.contrapose₁
eventually_liminf_le 📖	mathematical	Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	Filter.Eventually Filter.liminf	—	eventually_le_limsup instOrderTopologyOrderDual instFirstCountableTopologyOrderDual
instBoundedGENhdsClassOrderDual 📖	mathematical	—	BoundedGENhdsClass OrderDual OrderDual.instPreorder OrderDual.instTopologicalSpace	—	isBounded_le_nhds
instBoundedLENhdsClassOrderDual 📖	mathematical	—	BoundedLENhdsClass OrderDual OrderDual.instPreorder OrderDual.instTopologicalSpace	—	isBounded_ge_nhds
isBounded_ge_nhds 📖	mathematical	—	Filter.IsBounded Preorder.toLE nhds	—	BoundedGENhdsClass.isBounded_ge_nhds
isBounded_le_nhds 📖	mathematical	—	Filter.IsBounded Preorder.toLE nhds	—	BoundedLENhdsClass.isBounded_le_nhds
isCobounded_ge_nhds 📖	mathematical	—	Filter.IsCobounded Preorder.toLE nhds	—	Filter.IsBounded.isCobounded_flip instIsTransLe nhds_neBot isBounded_le_nhds
isCobounded_le_nhds 📖	mathematical	—	Filter.IsCobounded Preorder.toLE nhds	—	Filter.IsBounded.isCobounded_flip instIsTransGe nhds_neBot isBounded_ge_nhds
le_nhds_of_limsSup_eq_limsInf 📖	mathematical	Filter.IsBounded Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.limsSup Filter.limsInf	Filter Filter.instPartialOrder nhds	—	tendsto_order Filter.gt_mem_sets_of_limsInf_gt Filter.lt_mem_sets_of_limsSup_lt
liminf_eq_top 📖	mathematical	—	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedCoheytingAlgebra.toLattice CoheytingAlgebra.toGeneralizedCoheytingAlgebra Order.Coframe.toCoheytingAlgebra CompleteDistribLattice.toCoframe CompletelyDistribLattice.toCompleteDistribLattice CompleteLinearOrder.toCompletelyDistribLattice CoheytingAlgebra.toOrderTop Filter.EventuallyEq Pi.instTopForall	—	limsup_eq_bot instFirstCountableTopologyOrderDual instOrderTopologyOrderDual
limsInf_eq_of_le_nhds 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	Filter.limsInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	Filter.IsBounded.mono isBounded_ge_nhds BoundedGENhdsClass.of_closedIicTopology instClosedIicTopology OrderTopology.to_orderClosedTopology isBounded_le_nhds BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology le_antisymm Filter.limsInf_le_limsSup Filter.limsSup_le_limsSup_of_le Filter.IsBounded.isCobounded_flip instIsTransGe limsSup_nhds limsInf_nhds Filter.limsInf_le_limsInf_of_le instIsTransLe
limsInf_nhds 📖	mathematical	—	Filter.limsInf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice nhds	—	limsSup_nhds instOrderTopologyOrderDual
limsSup_eq_of_le_nhds 📖	mathematical	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder nhds	Filter.limsSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice	—	limsInf_eq_of_le_nhds instOrderTopologyOrderDual
limsSup_nhds 📖	mathematical	—	Filter.limsSup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice nhds	—	csInf_eq_of_forall_ge_of_forall_gt_exists_lt isBounded_le_nhds BoundedLENhdsClass.of_closedIciTopology instClosedIciTopology OrderTopology.to_orderClosedTopology mem_of_mem_nhds dense_or_discrete ge_mem_nhds Filter.sets_of_superset gt_mem_nhds
limsup_eq_bot 📖	mathematical	—	Filter.limsup ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup GeneralizedHeytingAlgebra.toLattice HeytingAlgebra.toGeneralizedHeytingAlgebra Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompletelyDistribLattice.toCompleteDistribLattice CompleteLinearOrder.toCompletelyDistribLattice HeytingAlgebra.toOrderBot Filter.EventuallyEq Pi.instBotForall	—	Filter.Eventually.mono Filter.EventuallyLE.trans eventually_le_limsup Filter.isBounded_le_of_top Filter.Eventually.of_forall Eq.le le_antisymm bot_le Filter.limsup_congr Filter.limsup_const_bot
tendsto_of_le_liminf_of_limsup_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.liminf Filter.limsup Filter.IsBoundedUnder	Filter.Tendsto nhds	—	Filter.eq_or_neBot Filter.tendsto_bot tendsto_of_liminf_eq_limsup le_antisymm le_trans Filter.liminf_le_limsup
tendsto_of_liminf_eq_limsup 📖	mathematical	Filter.liminf ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.limsup Filter.IsBoundedUnder Preorder.toLE PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder	Filter.Tendsto nhds	—	le_nhds_of_limsSup_eq_limsInf
tendsto_of_no_upcrossings 📖	mathematical	Dense Filter.Frequently Preorder.toLT PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice Filter.IsBoundedUnder Preorder.toLE	Filter.Tendsto nhds	—	Filter.eq_or_neBot Filter.tendsto_bot tendsto_of_le_liminf_of_limsup_le dense_iff_inter_open isOpen_Ioo OrderTopology.to_orderClosedTopology Set.nonempty_Ioo Filter.frequently_lt_of_liminf_lt Filter.IsBounded.isCobounded_ge Filter.map_neBot Filter.frequently_lt_of_lt_limsup Filter.IsBounded.isCobounded_le le_rfl

---

← Back to Index