edist_continuousRestrict_of_singleton

English

In the singleton case, the same edist equality holds for continuous restrictions on the singleton subset.

Русский

В случае единичного множества та же равенство edist сохраняется для непрерывных ограничений на синглтон.

LaTeX

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

Lean4

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

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