iSup — Mathlib

English

A finite iSup of finitely generated subgroups is finitely generated.

Русский

Пусть iSup над конечным индексным набором FG-подгрупп — FG.

LaTeX

$$$\forall {G : Type*} [Group G] {ι : Sort*} [Finite ι] (P : ι \to Subgroup G), (\forall i, (P i).FG) \to (iSup P).FG$$$

Lean4

@[to_additive]
theorem iSup {ι : Sort*} [Finite ι] (P : ι → Subgroup G) (hP : ∀ i, (P i).FG) : (iSup P).FG := by
  simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

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