instNoetherianSpaceCofiniteTopology

English

If α and β are homeomorphic, then α is Noetherian if and only if β is Noetherian.

Русский

Если пространства образуются гомеоморфизмом, то свойство Ноetherian сохраняется между ними.

LaTeX

$$$\\forall (f : \\alpha \\simeq_t\\beta), NoetherianSpace \\alpha \\iff NoetherianSpace \\beta$$$

Lean4

instance {α} : NoetherianSpace (CofiniteTopology α) :=
  by
  simp only [noetherianSpace_iff_isCompact, isCompact_iff_ultrafilter_le_nhds, CofiniteTopology.nhds_eq,
    Ultrafilter.le_sup_iff, Filter.le_principal_iff]
  intro s f hs
  rcases f.le_cofinite_or_eq_pure with (hf | ⟨a, rfl⟩)
  · rcases Filter.nonempty_of_mem hs with ⟨a, ha⟩
    exact ⟨a, ha, Or.inr hf⟩
  · exact ⟨a, hs, Or.inl le_rfl⟩

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