limsup_congr — Mathlib

English

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

Русский

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

LaTeX

$$$ \\text{If } (u =^\\text{a.e.}_f v) \\text{ then } \\limsup u f = \\limsup v f $$$

Lean4

theorem limsup_congr {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} {u v : α → β}
    (h : ∀ᶠ a in f, u a = v a) : limsup u f = limsup v f :=
  by
  rw [limsup_eq]
  congr with b
  exact eventually_congr (h.mono fun x hx => by simp [hx])

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