nndist — Mathlib

English

If f,g tend to a,b along a filter x, then nndist(f,g) tends to nndist(a,b) along x.

Русский

Если f,g сходятся к a,b вдоль фильтра, то nndist(f,g) сходится к nndist(a,b) вдоль этого фильтра.

LaTeX

$$$\mathrm{Tendsto}\ f\ x\ (\mathcal{N}(a)) \rightarrow \mathrm{Tendsto}\ g\ x\ (\mathcal{N}(b)) \Rightarrow \mathrm{Tendsto}(\lambda t, \mathrm{nndist}(f(t), g(t)))\ x\ (\mathcal{N}(\mathrm{nndist}(a,b)))$$$

Lean4

protected theorem nndist {f g : β → α} {x : Filter β} {a b : α} (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) :
    Tendsto (fun x => nndist (f x) (g x)) x (𝓝 (nndist a b)) :=
  (continuous_nndist.tendsto (a, b)).comp (hf.prodMk_nhds hg)

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