continuous_dist — Mathlib

English

The distance on the completion is a continuous extension; in particular, for f,g : β → Completion α which are continuous, the map x ↦ dist (f x) (g x) is continuous.

Русский

Расстояние на завершении является непрерывным продолжением; если f,g : β → Completion α непрерывны, то x ↦ dist(f x, g x) непрерывно.

LaTeX

$$$\text{Continuous}\, f \to \text{Continuous}\, g \; \Rightarrow \; \text{Continuous}\, (\lambda x, \operatorname{dist}(f x)(g x))$$$

Lean4

/-- The new distance is continuous. -/
protected theorem continuous_dist [TopologicalSpace β] {f g : β → Completion α} (hf : Continuous f)
    (hg : Continuous g) : Continuous fun x ↦ dist (f x) (g x) :=
  Completion.uniformContinuous_dist.continuous.comp (hf.prodMk hg :)

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