blimsup_congr — Mathlib

English

If there is eventual pointwise agreement between predicates that force p a → u a = v a, then blimsup u f p = blimsup v f p.

Русский

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

LaTeX

$$$ \\text{If } \\forall^\\infty a \in f, p(a) \\Rightarrow u(a)=v(a) \\text{ then } \\mathrm{blimsup}\,u\,f\,p = \\mathrm{blimsup}\,v\,f\,p $$$

Lean4

theorem blimsup_congr {f : Filter β} {u v : β → α} {p : β → Prop} (h : ∀ᶠ a in f, p a → u a = v a) :
    blimsup u f p = blimsup v f p := by
  simpa only [blimsup_eq_limsup] using limsup_congr <| eventually_inf_principal.2 h

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