limsSup_principal_eq_sSup — Mathlib

English

The blimsup of a principal filter equals the closed sup over the set: blimsup (principal s) = sSup s.

Русский

Блимсуп у фильтра-принципала равен верхней суперограниченности множества: blimsup (principal s) = sSup s.

LaTeX

$$$\\mathrm{blimsup}(\\text{principal } s) = sSup\, s$$$

Lean4

theorem limsSup_principal_eq_sSup (s : Set α) : limsSup (𝓟 s) = sSup s := by
  simpa only [limsSup, eventually_principal] using sInf_upperBounds_eq_csSup s

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