le_comap_mulSingle_pi

Mathlib.Algebra.Group.Submonoid.Operations

URI: https://scilib.ai/kg/mathlib#Submonoid.le_comap_mulSingle_pi

← MathLib Explorer

English

For [DecidableEq ι], S_i ≤ comap (mulSingle M i) (pi I S) holds coordinate-wise.

Русский

Для каждого i из ι выполняется S_i ≤ comap (mulSingle M i) (pi I S).

LaTeX

$$$ S i \le comap (MonoidHom.mulSingle M i) (pi I S) $$$

Lean4

@[to_additive]
theorem le_comap_mulSingle_pi [DecidableEq ι] (S : ∀ i, Submonoid (M i)) {I i} :
    S i ≤ comap (MonoidHom.mulSingle M i) (pi I S) := fun x hx => by simp [hx]

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

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

Разделы

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

Аффилиация

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