fg_iSup — Mathlib

English

If each S_i is finitely generated, then the supremum over i is finitely generated (under suitable finiteness conditions).

Русский

Если каждоe S_i конечнопорождено, то наибольший верхний предел по i тоже конечнопорожден.

LaTeX

$$$(\forall i, (S_i).FG) \Rightarrow (\bigsqcup_i S_i).FG$$$

Lean4

theorem fg_iSup {ι : Sort*} [Finite ι] {S : ι → IntermediateField F E} (h : ∀ i, (S i).FG) : (⨆ i, S i).FG :=
  by
  choose s hs using h
  simp_rw [← hs, ← adjoin_iUnion]
  exact fg_adjoin_of_finite (Set.finite_iUnion fun _ ↦ Finset.finite_toSet _)

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