noetherianSpace — Mathlib

English

If β is a topological space and i: β → α is an inducing map, and α is Noetherian, then β is Noetherian too.

Русский

Если β — пространство с вложением i в α и α Ноetherian, то β тоже Ноetherian.

LaTeX

$$$[\\text{NoetherianSpace } \\alpha]\\;\\Rightarrow\\;[\\text{IsInducing } i]\\;\\Rightarrow\\;\\text{NoetherianSpace } \\beta .$$$

Lean4

protected theorem _root_.Topology.IsInducing.noetherianSpace [NoetherianSpace α] {i : β → α} (hi : IsInducing i) :
    NoetherianSpace β :=
  (noetherianSpace_iff_opens _).2 fun _ => hi.isCompact_iff.2 (NoetherianSpace.isCompact _)

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