English
If a dense inducing embedding e: β → α exists, then the tendsto along abscissa translates to uniform continuity of the composed map.
Русский
Если существует плотная индукционная вложенность e: β → α, то переход по оси x в композиции переводит в равномерную непрерывность композиции.
LaTeX
$$$tendsto\\_div\\_comap\\_self (de) (x_0) : \\dots$$$
Lean4
@[to_additive]
theorem tendsto_div_comap_self (de : IsDenseInducing e) (x₀ : α) :
Tendsto (fun t : β × β => t.2 / t.1) ((comap fun p : β × β => (e p.1, e p.2)) <| 𝓝 (x₀, x₀)) (𝓝 1) :=
by
have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) = e ∘ fun t : β × β => t.2 / t.1 :=
by
ext t
simp
have lim : Tendsto (fun x : α × α => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1)) := by
simpa using (continuous_div'.comp (@continuous_swap α α _ _)).tendsto (x₀, x₀)
simpa using de.tendsto_comap_nhds_nhds lim comm
