isBlock

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.IsFixedBlock.isBlock

← MathLib Explorer

English

The empty set is a block.

Русский

Пустое множество является блоком.

LaTeX

$$$IsBlock(G, \emptyset).$$$

Lean4

/-- A fixed block is a block. -/
@[to_additive /-- A fixed block is a block. -/
    ]
theorem isBlock (hfB : IsFixedBlock G B) : IsBlock G B := by simp [IsBlock, hfB _]

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

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

Разделы

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

Аффилиация

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