liminf_comp — Mathlib

English

The liminf of a composition equals the liminf of the outer function after mapping the filter through the inner function.

Русский

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

LaTeX

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

Lean4

theorem liminf_comp (u : β → α) (v : γ → β) (f : Filter γ) : liminf (u ∘ v) f = liminf u (map v f) :=
  rfl

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