Documentation Verification Report

LiminfLimsup

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

Statistics

Metric	Count
Definitions `BoundedGENhdsClass`, `BoundedLENhdsClass`	2
Theorems `liminf_nhdsGT_eq_iSup₂`, `liminf_nhdsGT_eq_iSup₂_of_exists_gt`, `limsup_nhdsLT_eq_iInf₂`, `limsup_nhdsLT_eq_iInf₂_of_exists_lt`, `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`, `liminf_nhdsLT_eq_iSup₂`, `liminf_nhdsLT_eq_iSup₂_of_exists_lt`, `limsup_nhdsGT_eq_iInf₂`, `limsup_nhdsGT_eq_iInf₂_of_exists_gt`, `map_liminf_of_continuousAt`, `map_limsInf_of_continuousAt`, `map_limsSup_of_continuousAt`, `map_limsup_of_continuousAt`, `tendsto_iSup_of_tendsto_limsup`, `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_iSup_of_tendsto_limsup`, `tendsto_of_le_liminf_of_limsup_le`, `tendsto_of_liminf_eq_limsup`, `tendsto_of_no_upcrossings`	56
Total	58

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liminf_nhdsGT_eq_iSup₂` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Filter.liminf` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`liminf_nhdsGT_eq_iSup₂_of_exists_gt` `NoMaxOrder.exists_gt`
`liminf_nhdsGT_eq_iSup₂_of_exists_gt` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLT`	`Filter.liminf` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`Filter.HasBasis.liminf_eq_iSup_iInf` `nhdsGT_basis_of_exists_gt` `le_antisymm` `iSup₂_mono'` `exists_between` `iInf₂_le` `le_iInf₂` `LT.lt.le` `Set.mem_Ioo`
`limsup_nhdsLT_eq_iInf₂` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Filter.limsup` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`limsup_nhdsLT_eq_iInf₂_of_exists_lt` `NoMinOrder.exists_lt`
`limsup_nhdsLT_eq_iInf₂_of_exists_lt` 📖	mathematical	`Antitone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLT`	`Filter.limsup` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`Filter.HasBasis.limsup_eq_iInf_iSup` `nhdsLT_basis_of_exists_lt` `le_antisymm` `iInf₂_mono'` `iSup₂_le` `LT.lt.le` `Set.mem_Ioo` `exists_between` `le_iSup₂_of_le` `le_rfl`
`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.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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.limsInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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.limsSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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`	—	—

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
`liminf_nhdsLT_eq_iSup₂` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Filter.liminf` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`liminf_nhdsLT_eq_iSup₂_of_exists_lt` `NoMinOrder.exists_lt`
`liminf_nhdsLT_eq_iSup₂_of_exists_lt` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLT`	`Filter.liminf` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Iio` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`Filter.HasBasis.liminf_eq_iSup_iInf` `nhdsLT_basis_of_exists_lt` `le_antisymm` `iSup₂_mono'` `exists_between` `iInf₂_le` `le_iInf₂` `LT.lt.le` `Set.mem_Ioo`
`limsup_nhdsGT_eq_iInf₂` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice`	`Filter.limsup` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`limsup_nhdsGT_eq_iInf₂_of_exists_gt` `NoMaxOrder.exists_gt`
`limsup_nhdsGT_eq_iInf₂_of_exists_gt` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Preorder.toLT`	`Filter.limsup` `CompleteLattice.toConditionallyCompleteLattice` `nhdsWithin` `Set.Ioi` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `iInf` `ConditionallyCompletePartialOrderInf.toInfSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `Preorder.toLT`	—	`Filter.HasBasis.limsup_eq_iInf_iSup` `nhdsGT_basis_of_exists_gt` `le_antisymm` `iInf₂_mono'` `iSup₂_le` `LT.lt.le` `Set.mem_Ioo` `exists_between` `le_iSup₂_of_le` `le_rfl`
`map_liminf_of_continuousAt` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousAt` `Filter.liminf` `Filter.IsCoboundedUnder` `Preorder.toLE` `Filter.IsBoundedUnder`	`Filter.liminf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`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.limsInf` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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.limsSup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `Filter.limsup`	—	`Antitone.map_limsSup_of_continuousAt` `instOrderTopologyOrderDual`
`map_limsup_of_continuousAt` 📖	mathematical	`Monotone` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ContinuousAt` `Filter.limsup` `Filter.IsBoundedUnder` `Preorder.toLE` `Filter.IsCoboundedUnder`	`Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice`	—	`map_limsSup_of_continuousAt` `Filter.map_neBot`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tendsto_iSup_of_tendsto_limsup` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `nhds` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `instPreorder` `Antitone`	`Filter.Tendsto` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `nhds`	—	`tendsto_iSup_of_tendsto_limsup` `cofinite_eq_atTop`

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`	`BoundedGENhdsClass` `preorder` `topologicalSpace`	—	`BoundedLENhdsClass.isBounded_le_nhds` `instBoundedLENhdsClass` `instBoundedLENhdsClassOrderDual`
`instBoundedLENhdsClass` 📖	mathematical	`BoundedLENhdsClass`	`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	5 math math: `instBoundedGENhdsClassOrderDual`, `OrderBot.to_BoundedGENhdsClass`, `Pi.instBoundedGENhdsClass`, `Prod.instBoundedGENhdsClass`, `BoundedGENhdsClass.of_closedIicTopology`
`BoundedLENhdsClass` 📖	CompData	5 math math: `BoundedLENhdsClass.of_closedIciTopology`, `Pi.instBoundedLENhdsClass`, `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` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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` `Preorder.toLE` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `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` `Preorder.toLE` `PartialOrder.toPreorder` `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_iSup_of_tendsto_limsup` 📖	mathematical	`Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `nhds` `Filter.limsup` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Filter.cofinite` `Antitone`	`Filter.Tendsto` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Filter.atTop` `PartialOrder.toPreorder` `ConditionallyCompletePartialOrderSup.toPartialOrder` `nhds`	—	`isEmpty_or_nonempty` `ciSup_of_empty` `T2Space.t1Space` `OrderClosedTopology.to_t2Space` `OrderTopology.to_orderClosedTopology` `Filter.atTop_neBot` `SemilatticeSup.instIsDirectedOrder` `supSet_to_nonempty` `Filter.cofinite_eq_bot` `Finite.of_subsingleton` `IsEmpty.instSubsingleton` `Filter.limsup_bot` `tendsto_order` `Filter.univ_mem'` `Antitone.le_of_tendsto` `LT.lt.trans_le` `LE.le.trans` `le_iSup_iff` `Set.Nonempty.some_mem` `Filter.mp_mem` `LT.lt.le` `Mathlib.Tactic.Contrapose.contrapose₂` `Set.eq_empty_or_nonempty` `le_rfl` `Filter.eventually_lt_of_limsup_lt` `LE.le.trans_lt` `Filter.isBounded_le_of_top` `Mathlib.Tactic.Contrapose.contrapose₁` `lt_of_le_of_lt` `iSup_le` `le_ciSup` `Finite.bddAbove_range` `le_sup_right` `le_sup_left` `not_lt`
`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