English
In a commutative topological group with continuous division, for a fixed b, the map f ↦ b / f is continuous in f, and hence Tendsto (f) to c implies Tendsto (k ↦ b / f(k)) to b / c, and conversely in the appropriate setting.
Русский
В коммутативной топологической группе с непрерывным делением отображение f ↦ b / f непрерывно по f; следовательно, Tendsto f к c влечёт Tendsto (k ↦ b / f(k)) к b / c, и наоборот.
LaTeX
$$$\forall b,\; \text{Continuous}\bigl(\lambda x. b / x\bigr) \quad\Longrightarrow\quad \text{Tendsto}\bigl(f(k)\bigr)_{l}(\mathcal{N}(c)) \Rightarrow \text{Tendsto}\bigl(b / f(k)\bigr)_{l}(\mathcal{N}(b / c)).$$$
Lean4
@[to_additive]
theorem tendsto_const_div_iff {G : Type*} [CommGroup G] [TopologicalSpace G] [ContinuousDiv G] (b : G) {c : G}
{f : α → G} {l : Filter α} : Tendsto (fun k : α ↦ b / f k) l (𝓝 (b / c)) ↔ Tendsto f l (𝓝 c) :=
by
refine ⟨fun h ↦ ?_, Filter.Tendsto.const_div' b⟩
convert h.const_div' b with k <;> rw [div_div_cancel]
