liminf_eq_iSup_iInf_of_nat' — Mathlib

English

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

Русский

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

LaTeX

$$$\\displaystyle \\liminf u f = \\big\\uparrow_i (\\,p(i)\\, ) \\, \\bigl( \\inf_{a \\in s(i)} u(a) \\bigr)$$$

Lean4

theorem liminf_eq_iSup_iInf_of_nat' {u : ℕ → α} : liminf u atTop = ⨆ n : ℕ, ⨅ i : ℕ, u (i + n) :=
  @limsup_eq_iInf_iSup_of_nat' αᵒᵈ _ _

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