edist_eq_restrict_sUnion — Mathlib

English

For finite 𝔖, edist f g equals the edist between the UniformFun of restricted values on ⋃₀ 𝔖.

Русский

Для конечного 𝔖 евдист между f и g равен евдисту между UniformFun ограниченных значений на ⋃₀ 𝔖.

LaTeX

$$edist f g = edist (UniformFun.ofFun ((⋃₀ 𝔖).restrict (toFun 𝔖 f))) (UniformFun.ofFun ((⋃₀ 𝔖).restrict (toFun 𝔖 g)))$$

Lean4

theorem edist_eq_restrict_sUnion [Finite 𝔖] {f g : α →ᵤ[𝔖] β} :
    edist f g =
      edist (UniformFun.ofFun ((⋃₀ 𝔖).restrict (toFun 𝔖 f))) (UniformFun.ofFun ((⋃₀ 𝔖).restrict (toFun 𝔖 g))) :=
  iSup_subtype'

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