edist — Mathlib

English

If f and g tend to a and b respectively, then Tendsto (x ↦ edist (f x) (g x)) to edist(a,b).

Русский

Если f и g сходятся к a и b, то функция edist(f x, g x) сходится к edist(a,b).

LaTeX

$$$\text{Tendsto } f x (\mathcal{N} a) \land \text{Tendsto } g x (\mathcal{N} b) \Rightarrow \text{Tendsto } (\lambda x. edist (f x) (g x)) x (\mathcal{N} (edist a b)).$$$

Lean4

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

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