disjoint_smul_left

Mathlib.GroupTheory.GroupAction.Blocks

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

English

A block is characterized by: for every g, either g·B = B or g·B is disjoint from B.

Русский

Блок охарактеризуется: для каждого g либо g·B = B, либо g·B дисjoint с B.

LaTeX

$$$IsBlock(G,B) \leftrightarrow \forall g,\; (g\cdot B = B) \lor Disjoint(g\cdot B,B).$$$

Lean4

@[to_additive]
theorem disjoint_smul_left (hB : IsBlock M B) (hs : ¬B ⊆ s • B) : Disjoint (s • B) B :=
  (hB.disjoint_smul_right hs).symm

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

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

Разделы

Аффилиация

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