English
Let α be a complete lattice, f a filter with HasBasis p s on β, and u : β → α. Then the liminf of u with respect to f equals the supremum over i with p(i) of the infimum of u over s(i): liminf u f = ⨆ i (i has p) ⨅ a ∈ s(i), u(a).
Русский
Пусть α — полная решетка, f — фильтр с базисом HasBasis p s на β, и u : β → α. Тогда liminf u f = ⨆ i, (если p(i)) ⨅ a ∈ s(i), u(a).
LaTeX
$$$\\displaystyle \\liminf u f = \\big\\varnothing\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\\\displaystyle \\sup_{i:\\, p(i)} \\inf_{a \\in s(i)} u(a) $$$$
Lean4
/-- In a complete lattice, the liminf of a function is the infimum over sets `s` in the filter
of the supremum of the function over `s` -/
theorem liminf_eq_iSup_iInf {f : Filter β} {u : β → α} : liminf u f = ⨆ s ∈ f, ⨅ a ∈ s, u a :=
limsup_eq_iInf_iSup (α := αᵒᵈ)
