isBlock_iff_pairwiseDisjoint_range_smul

Mathlib.GroupTheory.GroupAction.Blocks

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

← MathLib Explorer

English

IsBlock G B is equivalent to the pairwise disjointness of the sets {g • B} as g runs over G.

Русский

IsBlock эквивалентно парному/disjoint набору образов {g•B}.

LaTeX

$$IsBlock G B ↔ (range fun g : G => g • B).PairwiseDisjoint id$$

Lean4

@[to_additive]
theorem isBlock_iff_pairwiseDisjoint_range_smul : IsBlock G B ↔ (range fun g : G ↦ g • B).PairwiseDisjoint id :=
  pairwiseDisjoint_range_iff.symm

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

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

Разделы

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

Аффилиация

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