comapPseudoMetricSpace — Mathlib

English

Pull back a pseudometric space structure by an inducing map.

Русский

Восстановить псевдометрическое пространство на области через индуцирующее отображение.

LaTeX

$$$\\text{comapPseudoMetricSpace}(f, hf)$ определяет псевдометрическое пространство на домене так, чтобы метрика соответствовала метрике целевого пространства через f.$$

Lean4

/-- Pull back a pseudometric space structure by an inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `TopologicalSpace`
structure. -/
def comapPseudoMetricSpace {α β : Type*} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β}
    (hf : IsInducing f) : PseudoMetricSpace α :=
  .replaceTopology (.induced f m) hf.eq_induced

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