pseudoMetrizableSpace — Mathlib

English

If f: X → Y is an inducing map and Y is pseudo-metrizable, then X is pseudo-metrizable.

Русский

Если отображение f: X → Y является индуцирующим и Y псевдометризуемо, то X тоже псевдометризуемо.

LaTeX

$$$\text{IsInducing}(f) \Rightarrow (\text{PseudoMetrizableSpace } Y \Rightarrow \text{PseudoMetrizableSpace } X)$$$

Lean4

/-- Given an inducing map of a topological space into a pseudo metrizable space, the source space
is also pseudo metrizable. -/
theorem _root_.Topology.IsInducing.pseudoMetrizableSpace [PseudoMetrizableSpace Y] {f : X → Y} (hf : IsInducing f) :
    PseudoMetrizableSpace X :=
  letI : PseudoMetricSpace Y := pseudoMetrizableSpacePseudoMetric Y
  ⟨⟨hf.comapPseudoMetricSpace, rfl⟩⟩

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