limsInf_principal_eq_csSup — Mathlib

English

If s is bounded below and nonempty, then the limsInf of the principal filter generated by s equals the infimum of s.

Русский

Если множество s ограничено снизу и непусто, то limsInf (𝓟 s) равен sInf s.

LaTeX

$$$ \\operatorname{limsInf} (\\mathcal{P} s) = \\operatorname{sInf} s $$$

Lean4

theorem limsInf_principal_eq_csSup (h : BddBelow s) (hs : s.Nonempty) : limsInf (𝓟 s) = sInf s :=
  limsSup_principal_eq_csSup (α := αᵒᵈ) h hs

Похожие утверждения