continuous_dist

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#continuous_dist

English

If f,g: β→α are continuous, then b ↦ dist(f(b), g(b)) is continuous.

Русский

Если f,g: β→α непрерывны, то b↦dist(f(b), g(b)) непрерывна.

LaTeX

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

Lean4

@[continuity]
theorem continuous_dist : Continuous fun p : α × α ↦ dist p.1 p.2 :=
  uniformContinuous_dist.continuous

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru