Theorems · Theorem · general topology

Filter.Tendsto.bddBelow_range_of_cofinite

∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] {u : ι → α}
  {a : α} [IsCodirectedOrder α], Filter.Tendsto u Filter.cofinite (nhds a) → BddBelow (Set.range u)

Defined in

Mathlib.Topology.Order.LiminfLimsup

Cited by

0 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreorderTopologicalSpaceBoundedGENhdsClassIsCodirectedOrder