Lean4
/-- The natural `EMetric` structure on `α →ᵤ β` given by `edist f g = ⨆ x, edist (f x) (g x)`. -/
noncomputable instance : PseudoEMetricSpace (α →ᵤ β)
where
edist_self := by simp [edist_def]
edist_comm := by simp [edist_def, edist_comm]
edist_triangle f₁ f₂
f₃ :=
calc
⨆ x, edist (f₁ x) (f₃ x) ≤ ⨆ x, edist (f₁ x) (f₂ x) + edist (f₂ x) (f₃ x) :=
iSup_mono fun _ ↦ edist_triangle _ _ _
_ ≤ (⨆ x, edist (f₁ x) (f₂ x)) + (⨆ x, edist (f₂ x) (f₃ x)) := iSup_add_le _ _
toUniformSpace := inferInstance
uniformity_edist :=
by
suffices 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0) by
simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]
rw [ENNReal.nhds_zero_basis_Iic.comap _ |>.eq_biInf]
rw [UniformFun.hasBasis_uniformity_of_basis α β uniformity_basis_edist_le |>.eq_biInf]
simp [UniformFun.gen, edist_le, Set.Iic]
