congr_atTop — Mathlib

English

If HasProd f a along atTop and f and g are eventually equal atTop, then g is multipliable.

Русский

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

LaTeX

$$$\text{HasProd}(f,a,L) \land f=^{atTop} g \Rightarrow \text{Multipliable}(g).$$$

Lean4

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

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