English
For a fixed b in a topological group G with continuous division, the map x ↦ x / b is continuous. Consequently, if a function f: α → G tends to c, then the function k ↦ f(k) / b tends to c / b.
Русский
Для фиксированного b в топологической группе G с непрерывным делением отображение x ↦ x / b непрерывно. Следовательно, если f(k) → c, то f(k)/b → c/b.
LaTeX
$$$\text{Continuous}(\lambda x. x / b) \quad\Rightarrow\quad \text{Tendsto}(f)_{l}(\mathcal{N}(c)) \Rightarrow \text{Tendsto}(\lambda k. f(k)/b)_{l}(\mathcal{N}(c/b)).$$$
Lean4
@[to_additive sub_const]
theorem div_const' {c : G} {f : α → G} {l : Filter α} (h : Tendsto f l (𝓝 c)) (b : G) :
Tendsto (f · / b) l (𝓝 (c / b)) :=
h.div' tendsto_const_nhds
