biSup_finset — Mathlib

English

If a finite set is given and each P_i is FG, then the supremum over i in s is FG.

Русский

Для конечного множества s и функций P, где каждая P_i FG, супремум по i ∈ s FG.

LaTeX

$$$\forall {G : Type*} [Group G] {ι : Type*} (s : Finset ι) (P : ι \to Subgroup G), (\forall i ∈ s, (P i).FG) \to (s.\sup P).FG$$$

Lean4

@[to_additive]
theorem biSup_finset {ι : Type*} (s : Finset ι) (P : ι → Subgroup G) (hP : ∀ i ∈ s, (P i).FG) : (⨆ i ∈ s, P i).FG := by
  simpa only [Finset.sup_eq_iSup] using finset_sup s P hP

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