tendsto_atTop_one — Mathlib

English

If f: ℕ → G is multipliable in a topological group G, then f(n) tends to 1 along the sequence n → ∞.

Русский

Если f: ℕ → G мультиплируема в топологической группе G, то элементы f(n) стремятся к единице при n → ∞.

LaTeX

$$$\text{Tendsto}\_{n\to\infty} f(n) = 1$$$

Lean4

@[to_additive]
theorem tendsto_atTop_one {f : ℕ → G} (hf : Multipliable f) : Tendsto f atTop (𝓝 1) :=
  by
  rw [← Nat.cofinite_eq_atTop]
  exact hf.tendsto_cofinite_one

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