rw — Mathlib · SciLib

English

If f and g are equal frequently, then any predicate p preserved by changing f to g holds frequently for g whenever it held for f.

Русский

Если f и g часто равны, то любое свойство p, устойчивое к переходу от f к g, сохраняется часто для g при частоте для f.

LaTeX

$$$\\Big(f =^{{l}} g\\Big) \\Rightarrow \\big(\\forall p, (\\forall^{{\\text{freq}}}_{x\\in l} p(x,f(x))) \\to (\\forall^{{\\text{freq}}}_{x\\in l} p(x,g(x)))\\big)$$$

Lean4

theorem rw {l : Filter α} {f g : α → β} (h : f =ᶠ[l] g) (p : α → β → Prop) (hf : ∀ᶠ x in l, p x (f x)) :
    ∀ᶠ x in l, p x (g x) :=
  hf.congr <| h.mono fun _ hx => hx ▸ Iff.rfl

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