edist_continuousRestrict — Mathlib

English

Let f,g ∈ α →ᵤ[𝔖] β with [CompactSpace ⋃₀ 𝔖]. If the restrictions to 𝔖 are continuous on ⋃₀ 𝔖, then the edistance between the continuous extensions to C(⋃₀ 𝔖, β) equals edist(f,g).

Русский

Пусть f,g: α →ᵤ[𝔖] β и [CompactSpace ⋃₀ 𝔖]. Если ограничения на 𝔖 непрерывны на ⋃₀ 𝔖, то расстояние edist между соответствующими непрерывными отображениями совпадает с edist(f,g).

LaTeX

$$$edist(\langle -, hf.restrict \rangle : C(⋃₀ 𝔖, β), \langle -, hg.restrict \rangle) = edist(f,g)$$$

Lean4

theorem edist_continuousRestrict [TopologicalSpace α] {f g : α →ᵤ[𝔖] β} [CompactSpace (⋃₀ 𝔖)]
    (hf : ContinuousOn (toFun 𝔖 f) (⋃₀ 𝔖)) (hg : ContinuousOn (toFun 𝔖 g) (⋃₀ 𝔖)) :
    edist (⟨_, hf.restrict⟩ : C(⋃₀ 𝔖, β)) ⟨_, hg.restrict⟩ = edist f g := by
  simp [ContinuousMap.edist_eq_iSup, iSup_subtype, edist_def]

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