instEMetricSpaceSeparationQuotient

Mathlib.Topology.EMetricSpace.Basic

URI: https://scilib.ai/kg/mathlib#instEMetricSpaceSeparationQuotient

Lean4

instance [PseudoEMetricSpace X] : EMetricSpace (SeparationQuotient X) :=
  @EMetricSpace.ofT0PseudoEMetricSpace (SeparationQuotient X)
    { edist_self := surjective_mk.forall.2 edist_self, edist_comm := surjective_mk.forall₂.2 edist_comm,
      edist_triangle := surjective_mk.forall₃.2 edist_triangle, toUniformSpace := inferInstance,
      uniformity_edist :=
        comap_injective (surjective_mk.prodMap surjective_mk) <| by
          simp [comap_mk_uniformity, PseudoEMetricSpace.uniformity_edist] }
    _

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

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

Разделы

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

Аффилиация

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