biSup

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#Submonoid.FG.biSup

← MathLib Explorer

English

Finite sup over a finite index set of FG submonoids is FG.

Русский

Конечный суп по конечному индексу FG подмножидов FG.

LaTeX

$$biSup {i ∈ s} (P_i).FG$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru