tendsto_div_nhds_one_iff — Mathlib

English

For a topological group G (commutative with zero in the multiplicative notation), Tendsto (u(k) / x) to 1 is equivalent to Tendsto u(k) to x.

Русский

Для топологической группы G (с нулём в единичной системе умножения) Tendsto (u(k)/x) к 1 эквивалентно Tendsto u(k) к x.

LaTeX

$$$\text{Tendsto}(u(\cdot) / x)_{l}(\mathcal{N}(1)) \iff \text{Tendsto}(u(\cdot))_{l}(\mathcal{N}(x)).$$$

Lean4

@[to_additive]
theorem tendsto_div_nhds_one_iff {α : Type*} {l : Filter α} {x : G} {u : α → G} :
    Tendsto (u · / x) l (𝓝 1) ↔ Tendsto u l (𝓝 x) :=
  haveI A : Tendsto (fun _ : α => x) l (𝓝 x) := tendsto_const_nhds
  ⟨fun h => by simpa using h.mul A, fun h => by simpa using h.div' A⟩

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