instPseudoMetricSpaceOfBoundedSpace

Mathlib.Topology.MetricSpace.UniformConvergence

URI: https://scilib.ai/kg/mathlib#UniformFun.instPseudoMetricSpaceOfBoundedSpace

Lean4

noncomputable instance [BoundedSpace β] : PseudoMetricSpace (α →ᵤ β) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun f g ↦ ⨆ x, dist (toFun f x) (toFun g x))
    (fun _ _ ↦ by
      have := BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top
      refine (iSup_le fun x ↦ EMetric.edist_le_diam_of_mem ?_ ?_).trans_lt this |>.ne
      all_goals trivial)
    (fun _ _ ↦ by simp [edist_def, ENNReal.toReal_iSup (fun _ ↦ edist_ne_top _ _), dist_edist])

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru