limsSup_principal_eq_csSup — Mathlib

English

If s is bounded above and nonempty, then the limsSup of the principal filter generated by s equals the supremum of s.

Русский

Если множество s ограничено сверху и непусто, то limsSup (𝓟 s) равен sSup s.

LaTeX

$$$ \\operatorname{limsSup} (\\mathcal{P} s) = \\operatorname{sSup} s $$$

Lean4

theorem limsSup_principal_eq_csSup (h : BddAbove s) (hs : s.Nonempty) : limsSup (𝓟 s) = sSup s := by
  simp only [limsSup, eventually_principal]; exact csInf_upperBounds_eq_csSup h hs

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