liminf_eq_sSup_univ_of_empty — Mathlib

English

Under a HasBasis hv, if there exists an index i with p i and s i = ∅, then liminf f v equals sSup univ.

Русский

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

LaTeX

$$$ \\operatorname{liminf} f v = \\operatorname{sSup} \\{\\text{all elements}\\} $$$

Lean4

theorem liminf_eq_sSup_univ_of_empty {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} (hv : v.HasBasis p s)
    (i : ι') (hi : p i) (h'i : s i = ∅) : liminf f v = sSup univ := by simp [hv.eq_bot_iff.2 ⟨i, hi, h'i⟩, liminf_eq]

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