iSup

Mathlib.GroupTheory.Finiteness

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

← MathLib Explorer

English

If ι is finite and each P_i is FG, then iSup P is FG.

Русский

Если индексы ι конечны и каждый P_i FG, то iSup P FG.

LaTeX

$$iSup (P) FG$$

Lean4

@[to_additive]
theorem iSup {ι : Sort*} [Finite ι] (P : ι → Submonoid M) (hP : ∀ i, (P i).FG) : (iSup P).FG := by
  simpa [iSup_plift_down] using biSup Set.finite_univ (P ∘ PLift.down) fun i _ => hP i.down

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

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

Разделы

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

Аффилиация

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