iUnion — Mathlib

English

If α is Noetherian and each f i is a Noetherian space, then the union of finitely many f i is Noetherian.

Русский

Если α Ноetherian и каждый f_i — это пространство Ноetherian, то объединение конечного числа f_i — Ноetherian.

LaTeX

$$$[\\text{Finite } ι]\\to \\text{NoetherianSpace}(\\bigcup_i f_i).$$

Lean4

theorem iUnion {ι : Type*} (f : ι → Set α) [Finite ι] [hf : ∀ i, NoetherianSpace (f i)] : NoetherianSpace (⋃ i, f i) :=
  by
  simp_rw [noetherianSpace_set_iff] at hf ⊢
  intro t ht
  rw [← Set.inter_eq_left.mpr ht, Set.inter_iUnion]
  exact isCompact_iUnion fun i => hf i _ Set.inter_subset_right

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