comapPseudoMetricSpace

Mathlib.Topology.MetricSpace.Pseudo.Constructions

URI: https://scilib.ai/kg/mathlib#IsUniformInducing.comapPseudoMetricSpace

Lean4

/-- Pull back a pseudometric space structure by a uniform inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `UniformSpace`
structure. -/
def comapPseudoMetricSpace {α β} [UniformSpace α] [m : PseudoMetricSpace β] (f : α → β) (h : IsUniformInducing f) :
    PseudoMetricSpace α :=
  .replaceUniformity (.induced f m) h.comap_uniformity.symm

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

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

Разделы

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

Аффилиация

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