bliminf_eq_iSup_biInf — Mathlib

English

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

Русский

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

LaTeX

$$$\\displaystyle \\operatorname{bliminf} u f p = \\big\\sup_{s \\in f} \\bigl( \\inf_{b \\in s,\\ p(b)} u(b) \\bigr)$$$

Lean4

theorem bliminf_eq_iSup_biInf {f : Filter β} {p : β → Prop} {u : β → α} :
    bliminf u f p = ⨆ s ∈ f, ⨅ (b) (_ : p b ∧ b ∈ s), u b :=
  @blimsup_eq_iInf_biSup αᵒᵈ β _ f p u

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