multipliable_congr — Mathlib

English

If f and g are equal pointwise, then Multipliable f L ↔ Multipliable g L.

Русский

Если f и g равны по каждой точке, тогда Multipliable f L эквивалентно Multipliable g L.

LaTeX

$$$\\forall b,\\ f b = g b \\Rightarrow (Multipliable f L) \\Leftrightarrow (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 multipliable_congr (hfg : ∀ b, f b = g b) : Multipliable f L ↔ Multipliable g L :=
  iff_of_eq (congr_arg (Multipliable · L) <| funext hfg)

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