congr — Mathlib

English

If f is Multipliable with respect to L and f and g agree pointwise, then g is Multipliable with respect to L.

Русский

Если f является Multipliable по отношению к L и f и g согласованы точечно, тогда g также Multipliable по отношению к L.

LaTeX

$$$hf : Multipliable f L \\Rightarrow (\\forall b, f b = g b) \\Rightarrow Multipliable g L$$$

Lean4

/-- See `Multipliable.congr_cofinite` for a version allowing the functions to
disagree on a finite set. -/
@[to_additive /-- See `Summable.congr_cofinite` for a version allowing the functions to
    disagree on a finite set. -/
    ]
theorem congr (hf : Multipliable f L) (hfg : ∀ b, f b = g b) : Multipliable g L :=
  (multipliable_congr hfg).mp hf

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