multipliable_congr_cofinite — Mathlib

English

If f and g are cofinally equivalent (differ on only a finite set) then f is multipliable iff g is multipliable.

Русский

Если f и g совпадают за пределами конечного множества, то их умножаемость эквивалентна.

LaTeX

$$$f =^{\mathrm{cofinite}} g \Rightarrow (\operatorname{Multipliable}(f) \iff \operatorname{Multipliable}(g)).$$$

Lean4

/-- A more general version of `multipliable_congr`, allowing the functions to
disagree on a finite set. -/
@[to_additive /-- A more general version of `summable_congr`, allowing the functions to
    disagree on a finite set. -/
    ]
theorem multipliable_congr_cofinite (hfg : f =ᶠ[cofinite] g) : Multipliable f ↔ Multipliable g :=
  ⟨fun h ↦ h.congr_cofinite hfg, fun h ↦ h.congr_cofinite (hfg.mono fun _ h' ↦ h'.symm)⟩

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