blimsup_eq_iInf_iSup — Mathlib

English

For a HasBasis f with p and s, blimsup u f = ⨅ i (p i), ⨆ a ∈ s i, ⨆ (·) (·), u a.

Русский

Для HasBasis f с p и s, blimsup u f = ⨅ i (p i), ⨆ a ∈ s i, ⨆ (·) (·), u a.

LaTeX

$$$\\mathrm{blimsup}(u,f) = \\inf_{i: p(i)}\\, \\sup_{a\\in s(i)}\\, \\sup_{\\_ : \\cdot} u(a)$$$

Lean4

theorem blimsup_eq_iInf_iSup {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (hf : f.HasBasis p s)
    {q : β → Prop} : blimsup u f q = ⨅ (i) (_ : p i), ⨆ a ∈ s i, ⨆ (_ : q a), u a := by
  simp only [blimsup_eq_limsup, (hf.inf_principal _).limsup_eq_iInf_iSup, mem_inter_iff, iSup_and, mem_setOf_eq]

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