liminf_eq_iSup_iInf — Mathlib

English

Let α be a complete lattice, f a filter with HasBasis p s on β, and u : β → α. Then bliminf u f p = ⨆ i (_ : p i), ⨅ a ∈ s i, u a.

Русский

Пусть α — полная решетка, f — фильтр HasBasis p s на β, и u : β → α. Тогда bliminf u f p = ⨆ i (p(i)) ⨅ a ∈ s(i), u(a).

LaTeX

$$$\\displaystyle \\operatorname{bliminf} u f p = \\big\\uparrow_i (\\; p(i) \\\\Rightarrow \\inf_{a \\in s(i)} u(a) \\;)$$$

Lean4

theorem liminf_eq_iSup_iInf {p : ι → Prop} {s : ι → Set β} {f : Filter β} {u : β → α} (h : f.HasBasis p s) :
    liminf u f = ⨆ (i) (_ : p i), ⨅ a ∈ s i, u a :=
  HasBasis.limsup_eq_iInf_iSup (α := αᵒᵈ) h

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