pairwiseDisjoint

Mathlib.GroupTheory.GroupAction.Blocks

URI: https://scilib.ai/kg/mathlib#MulAction.orbit.pairwiseDisjoint

← MathLib Explorer

English

The family of orbits { orbit_G(a) } over a in X forms a partition of X.

Русский

Семейство орбит образует разбиение множества X.

LaTeX

$$$\\text{IsPartition}(\\{\\operatorname{orbit}(G,a) : a \\in X\\})$$$

Lean4

@[to_additive]
theorem pairwiseDisjoint : (Set.range fun x : X => orbit G x).PairwiseDisjoint id :=
  by
  rintro s ⟨x, rfl⟩ t ⟨y, rfl⟩ h
  contrapose! h
  exact (orbit.eq_or_disjoint x y).resolve_right h

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

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

Разделы

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

Аффилиация

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