coe_bot

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.BlockMem.coe_bot

English

The bottom element of BlockMem(a) corresponds to the singleton block {a}.

Русский

Нижний элемент BlockMem(a) соответствует блоку-синглетону {a}.

LaTeX

$$coe_bot (a) : ((\\perp : BlockMem G a) : Set X) = { a }$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_bot (a : X) : ((⊥ : BlockMem G a) : Set X) = { a } :=
  rfl

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

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

Разделы

Аффилиация

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