English
As above, the same isometry holds starting from continuous maps.
Русский
Как выше, та же изометрия существует для непрерывных отображений.
LaTeX
$$Isometry (Function.comp (EquivLike.toFunLike.coe UniformFun.ofFun) ContinuousMap.instFunLike.coe)$$
Lean4
/-- The natural `EMetric` structure on `α →ᵤ[𝔖] β` when `𝔖` is finite given by
`edist f g = ⨆ x ∈ ⋃₀ 𝔖, edist (f x) (g x)`. -/
noncomputable instance : PseudoEMetricSpace (α →ᵤ[𝔖] β)
where
edist_self f := by simp [edist_eq_restrict_sUnion]
edist_comm := by simp [edist_eq_restrict_sUnion, edist_comm]
edist_triangle f₁ f₂ f₃ := by simp [edist_eq_restrict_sUnion, edist_triangle]
toUniformSpace := inferInstance
uniformity_edist := by let _ := Fintype.ofFinite 𝔖;
simp_rw [← isUniformInducing_pi_restrict.comap_uniformity, PseudoEMetricSpace.uniformity_edist, comap_iInf,
comap_principal, edist_eq_pi_restrict, Set.preimage_setOf_eq]
