liminf — Mathlib

English

Similarly, the limsup of a composition equals the limsup of the outer function after mapping the filter through the inner function.

Русский

Предел верхний композиции равен пределу верхнему внешней функции после отображения фильтра через внутреннюю.

LaTeX

$$$\limsup (u \circ v) f = \limsup u (map v f)$$$

Lean4

/-- The `liminf` of a function `u` along a filter `f` is the supremum of the `a` such that
the inequality `u x ≥ a` eventually holds for `f`. -/
def liminf (u : β → α) (f : Filter β) : α :=
  limsInf (map u f)

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