liminf_congr — Mathlib

English

If two functions u and v are eventually equal with respect to a filter f, then their liminf with respect to f are equal.

Русский

Если функции u и v совпадают вплоть до некоторого момента в фильтре f, то liminf u f = liminf v f.

LaTeX

$$$ \\text{If } \\forall^\\infty a \\in f, u(a) = v(a) \\text{ then } \\liminf u f = \\liminf v f $$$

Lean4

theorem liminf_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β}
    (h : ∀ᶠ a in f, u a = v a) : liminf u f = liminf v f :=
  limsup_congr (β := βᵒᵈ) h

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