English
In a commutative topological group with continuous division, fixing b ∈ G, the map f ↦ b / f is a homeomorphism near any limit point. Consequently, for any f: α → G and l a filter, Tendsto (k ↦ b / f(k)) to b / c holds iff Tendsto f to c.
Русский
В коммутативной топологической группе с непрерывным делением фиксируем b ∈ G. Отображение f ↦ b / f является домашоморфизмом; следовательно, для любых f: α → G и l—фильтр, Tendsto (k ↦ b / f(k)) к b / c эквивалентно Tendsto f к c.
LaTeX
$$$\forall b\in G,\; \text{Tendsto}\bigl(\lambda k. \tfrac{b}{f(k)}\bigr)_{l} (\mathcal{N}(\tfrac{b}{c})) \quad\iff\quad \text{Tendsto}\bigl(f(k)\bigr)_{l} (\mathcal{N}(c)).$$$
Lean4
@[to_additive const_sub]
theorem const_div' (b : G) {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (𝓝 c)) :
Tendsto (fun k : α => b / f k) l (𝓝 (b / c)) :=
tendsto_const_nhds.div' h
