isBlock_iff_smul_eq_of_mem

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.isBlock_iff_smul_eq_of_mem

← MathLib Explorer

English

If B is a G-block, then B is an H-block for any subgroup H ≤ G.

Русский

Если B — G-блок, то B является H-блоком для всякой подгруппы H ≤ G.

LaTeX

$$$(H \le G) \; \Rightarrow \ IsBlock(H,B).$$$

Lean4

@[to_additive]
theorem isBlock_iff_smul_eq_of_mem : IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B := by
  simp [isBlock_iff_smul_eq_of_nonempty, Set.Nonempty, mem_smul_set]

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

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

Разделы

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

Аффилиация

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