noetherianSpace_set_iff — Mathlib

English

A space is Noetherian if and only if every subset is compact, equivalently the subspace topology on any subset is Noetherian.

Русский

Пространство Ноetherian iff каждое подмножество компактно; эквивалентно сохранению Noetherian на подпространствах.

LaTeX

$$$\\forall s: Set\\,\\alpha,\\; NoetherianSpace s \\iff \\forall t \\subseteq s, IsCompact t$$$

Lean4

theorem noetherianSpace_set_iff (s : Set α) : NoetherianSpace s ↔ ∀ t, t ⊆ s → IsCompact t := by
  simp only [noetherianSpace_iff_isCompact, IsEmbedding.subtypeVal.isCompact_iff, Subtype.forall_set_subtype]

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