dist — Mathlib

English

If f,g tend to a,b along a filter, then dist(f,g) tends to dist(a,b) along that filter.

Русский

Если f,g стремятся к a,b вдоль фильтра, то dist(f,g) стремится к dist(a,b) вдоль того же фильтра.

LaTeX

$$$\mathrm{Tendsto}\ (f,g)\ x\to (a,b)\Rightarrow \mathrm{Tendsto}\ (\lambda x, \operatorname{dist}(f(x),g(x)))\ x\to \operatorname{dist}(a,b)$$$

Lean4

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

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