finset_sup — Mathlib

English

If finite s and subfamilies P i are FG for all i ∈ s, then the finite supremum of these submonoids is FG.

Русский

Если конечный набор индексов s таит FG-подмножества P_i, то их конечная верхняя граница FG.

LaTeX

$$FG(⨆ i ∈ s, P_i)$$

Lean4

@[to_additive]
theorem finset_sup {ι : Type*} (s : Finset ι) (P : ι → Submonoid M) (hP : ∀ i ∈ s, (P i).FG) : (s.sup P).FG :=
  Finset.sup_induction bot (fun _ ha _ hb => ha.sup hb) hP

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