continuous_iff_continuous_dist — Mathlib

English

For any β with a topology, a function f: β→α is continuous iff the map x↦dist(f(x1), f(x2)) on β×β is continuous.

Русский

Для любой β с топологией функция f:β→α непрерывна тогда и только тогда, когда отображение x↦dist(f(x1), f(x2)) на β×β непрерывно.

LaTeX

$$$\text{Continuous}(f) \iff \text{Continuous}(\lambda x: (f(x_1), f(x_2))\mapsto \operatorname{dist}(f(x_1), f(x_2)))$$$

Lean4

theorem continuous_iff_continuous_dist [TopologicalSpace β] {f : β → α} :
    Continuous f ↔ Continuous fun x : β × β => dist (f x.1) (f x.2) :=
  ⟨fun h => h.fst'.dist h.snd', fun h =>
    continuous_iff_continuousAt.2 fun _ =>
      tendsto_iff_dist_tendsto_zero.2 <| (h.comp (.prodMk_left _)).tendsto' _ _ <| dist_self _⟩

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