limsSup_eq_iInf_sSup — Mathlib

English

If f has a basis given by p and s, then limsSup f equals the infimum over i with p(i) of sSup(s(i)).

Русский

Если у фильтра f имеется базис \n p(i) и s(i), то limsSup f равно инфимуму по i над p(i) от sSup(s(i)).

LaTeX

$$$\\operatorname{limsSup} f = \\bigwedge_{i: ι} \\bigwedge_{(h: p(i))} \\operatorname{sSup}(s(i))$$$

Lean4

theorem limsSup_eq_iInf_sSup {ι} {p : ι → Prop} {s} {f : Filter α} (h : f.HasBasis p s) :
    limsSup f = ⨅ (i) (_ : p i), sSup (s i) :=
  le_antisymm (le_iInf₂ fun i hi => sInf_le <| h.eventually_iff.2 ⟨i, hi, fun _ => le_sSup⟩)
    (le_sInf fun _ ha =>
      let ⟨_, hi, ha⟩ := h.eventually_iff.1 ha
      iInf₂_le_of_le _ hi <| sSup_le ha)

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