noetherianSpace_iff_of_homeomorph

English

If α is Noetherian and f: α → β is continuous and surjective, then β is Noetherian.

Русский

Если α Ноetherian и есть непрерывное сюръективное отображение f: α → β, то β Ноetherian.

LaTeX

$$$[NoetherianSpace \\alpha]\\;\\Rightarrow\\;[\\text{Continuous } f]\\;[\\text{Surjective } f]\\;\\Rightarrow\\; \\text{NoetherianSpace } \\beta$$$

Lean4

theorem noetherianSpace_iff_of_homeomorph (f : α ≃ₜ β) : NoetherianSpace α ↔ NoetherianSpace β :=
  ⟨fun _ => noetherianSpace_of_surjective f f.continuous f.surjective, fun _ =>
    noetherianSpace_of_surjective f.symm f.symm.continuous f.symm.surjective⟩

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