limsup_eq_sInf_univ_of_empty — Mathlib

English

Under a HasBasis hv, if for some i we have p i and s i = ∅, then limsup f v equals sInf univ.

Русский

При hv и существовании i с p i и s i = ∅, limsup f v = sInf univ.

LaTeX

$$$ \\operatorname{limsup} f v = \\operatorname{sInf} \\operatorname{Set}.univ $$$

Lean4

theorem limsup_eq_sInf_univ_of_empty {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s)
    (i : ι') (hi : p i) (h'i : s i = ∅) : limsup f v = sInf univ :=
  HasBasis.liminf_eq_sSup_univ_of_empty (α := αᵒᵈ) hv i hi h'i

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