dist — Mathlib

English

If f,g are continuous with respect to β→α, then b ↦ dist(f b, g b) is continuous; this is a standard consequence of continuity of dist.

Русский

Если f,g непрерывны, то b↦dist(f(b), g(b)) непрерывна; это стандартное следствие непрерывности функции dist.

LaTeX

$$$\text{Continuous}(\lambda b, \operatorname{dist}(f(b), g(b)))$$$

Lean4

@[continuity, fun_prop]
protected theorem dist [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => dist (f b) (g b) :=
  continuous_dist.comp₂ hf hg

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