edist_continuousMapMk — Mathlib

English

If f,g are UniformFun, and hf,hg are the continuous structures, then the edist computed via ContinuousMapMk agrees with edist f g.

Русский

Для f,g ∈ UniformFun и непрерывных структур hf,hg расстояние edist от полученной карты Mk совпадает с edist f g.

LaTeX

$$edist ((⟨-, hf⟩) : C(α,β)) ((⟨-, hg⟩) : C(α,β)) = edist f g$$

Lean4

theorem edist_continuousMapMk [TopologicalSpace α] [CompactSpace α] {f g : α →ᵤ β} (hf : Continuous (toFun f))
    (hg : Continuous (toFun g)) : edist (⟨_, hf⟩ : C(α, β)) ⟨_, hg⟩ = edist f g := by
  simp [← isometry_ofFun_continuousMap.edist_eq]

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