biSup — Mathlib

English

The biSup over a finite set with FG factors is FG.

Русский

Би-верхняя граница над конечным набором FG-факторов FG.

LaTeX

$$$\forall {G : Type*} [Group G] {ι : Type*} {s : Set ι} (hs : s.Finite) (P : ι → Subgroup G) (hP : \forall i \in s, (P i).FG), (iSup (\lambda i, iSup (\lambda h, P i)).FG)$$$

Lean4

@[to_additive]
theorem biSup {ι : Type*} {s : Set ι} (hs : s.Finite) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) :
    (⨆ i ∈ s, P i).FG := by simpa using biSup_finset hs.toFinset P (by simpa)

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