English
If a conditionally complete linear order α has order topology and a filter f is bounded both above and below, and its limsup equals its liminf equals a, then f converges to a.
Русский
Пусть α — условно завершимый линейный порядок с порядком; если фильтр f ограничен сверху и снизу и limsup f = liminf f = a, то f сходится к a.
LaTeX
$$$ (\text{hl}: fIsBounded (\le) f) (hg: fIsBounded (\ge) f) (hs: f.limsSup = a) (hi: f.limsInf = a) : f \le 𝓝 a. $$$
Lean4
/-- If the liminf and the limsup of a filter coincide, then this filter converges to
their common value, at least if the filter is eventually bounded above and below. -/
theorem le_nhds_of_limsSup_eq_limsInf {f : Filter α} {a : α} (hl : f.IsBounded (· ≤ ·)) (hg : f.IsBounded (· ≥ ·))
(hs : f.limsSup = a) (hi : f.limsInf = a) : f ≤ 𝓝 a :=
tendsto_order.2
⟨fun _ hb ↦ gt_mem_sets_of_limsInf_gt hg <| hi.symm ▸ hb, fun _ hb ↦ lt_mem_sets_of_limsSup_lt hl <| hs.symm ▸ hb⟩
