English
If α is a preorder, then its order dual αᵒᵈ also has BoundLENhdsClass.
Русский
Если у пространства α есть предикат порядка, то и у обратного порядка αᵒᵈ сохраняется BoundLENhdsClass.
LaTeX
$$$ [Preorder \; α] \Rightarrow BoundedLENhdsClass (OrderDual \; α). $$$
Lean4
/-- If a filter is converging, its limsup coincides with its limit. -/
theorem limsInf_eq_of_le_nhds {f : Filter α} {a : α} [NeBot f] (h : f ≤ 𝓝 a) : f.limsInf = a :=
have hb_ge : IsBounded (· ≥ ·) f := (isBounded_ge_nhds a).mono h
have hb_le : IsBounded (· ≤ ·) f := (isBounded_le_nhds a).mono h
le_antisymm
(calc
f.limsInf ≤ f.limsSup := limsInf_le_limsSup hb_le hb_ge
_ ≤ (𝓝 a).limsSup := (limsSup_le_limsSup_of_le h hb_ge.isCobounded_flip (isBounded_le_nhds a))
_ = a := limsSup_nhds a)
(calc
a = (𝓝 a).limsInf := (limsInf_nhds a).symm
_ ≤ f.limsInf := limsInf_le_limsInf_of_le h (isBounded_ge_nhds a) hb_le.isCobounded_flip)
