regularSpace — Mathlib

English

If f: Y → X is inducing and X is regular, then Y is regular.

Русский

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

LaTeX

$$$[IsInducing\ f] \Rightarrow RegularSpace(Y)$ при условии RegularSpace(X)$$

Lean4

protected theorem regularSpace [TopologicalSpace Y] {f : Y → X} (hf : IsInducing f) : RegularSpace Y :=
  .of_hasBasis (fun b => by rw [hf.nhds_eq_comap b]; exact (closed_nhds_basis _).comap _) fun b s hs => by
    exact hs.2.preimage hf.continuous

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