multipliable_congr_atTop — Mathlib

English

If f and g are atTop-equivalent, then f multipliable iff g multipliable.

Русский

Если f и g равны далее по порядку на atTop, то их умножаемость равна между собой.

LaTeX

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

Lean4

@[to_additive]
theorem multipliable_congr_atTop {f₁ g₁ : ℕ → α} (hfg : f₁ =ᶠ[atTop] g₁) : Multipliable f₁ ↔ Multipliable g₁ :=
  multipliable_congr_cofinite (Nat.cofinite_eq_atTop ▸ hfg)

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