biSup_finset — Mathlib

English

A more general form: if every P_i is FG, then the biSup over i in a finite set is FG.

Русский

Обобщение: если каждый P_i — FG, то их двунаправленный суп по конечному набору FG.

LaTeX

$$FG (iSup over i ∈ s of P_i)$$

Lean4

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

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