bliminf_congr — Mathlib

English

If eventually p a implies u a = v a, then blimsup u f p = blimsup v f p.

Русский

Если вплоть до некоторого момента выполняется p(a) ⇒ u(a) = v(a), то blimsup u f p = blimsup v f p.

LaTeX

$$$ \\mathrm{blimsup}\,u\,f\,p = \\mathrm{blimsup}\,v\,f\,p $$$

Lean4

theorem bliminf_congr {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) :
    bliminf u f p = bliminf v f p :=
  blimsup_congr (α := αᵒᵈ) h

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