Theorems · Theorem · general topology

limsInf_eq_of_le_nhds

∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {a : α} [f.NeBot], f ≤ nhds a → f.limsInf = a

If a filter is converging, its limsup coincides with its limit.

Defined in

Mathlib.Topology.Order.LiminfLimsup

Cited by

2 results in Mathlib

Foundations

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

Assumes

ConditionallyCompleteLinearOrderTopologicalSpaceOrderTopologyFilter.NeBot