singleton

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.IsBlock.singleton

English

Subsingletons are blocks.

Русский

Подмножества из одного элемента являются блоками.

LaTeX

$$$(B \text{ is subsingleton}) \Rightarrow IsBlock(G,B).$$$

Lean4

/-- A singleton is a block. -/
@[to_additive /-- A singleton is a block. -/
    ]
theorem singleton : IsBlock G ({ a } : Set X) := by simp [IsBlock]

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

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

Разделы

Аффилиация

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