noetherianSpace_of_surjective — Mathlib

English

The cofinite topology on any set α is Noetherian.

Русский

Кофинитная топология на любом множество α является Noetherian.

LaTeX

$$$[TopologicalSpace.NoetherianSpace (CofiniteTopology\\,\\alpha)].$$$

Lean4

theorem noetherianSpace_of_surjective [NoetherianSpace α] (f : α → β) (hf : Continuous f)
    (hf' : Function.Surjective f) : NoetherianSpace β :=
  noetherianSpace_iff_isCompact.2 <|
    (Set.image_surjective.mpr hf').forall.2 fun s => (NoetherianSpace.isCompact s).image hf

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