Theorems · Theorem · group theory

MulAction.IsBlock.isBlockSystem

∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X}
  [hGX : MulAction.IsPretransitive G X],
  MulAction.IsBlock G B → B.Nonempty → MulAction.IsBlockSystem G (Set.range fun g => g • B)

Translates of a block form a block system

Defined in

Mathlib.GroupTheory.GroupAction.Blocks

Cited by

1 results in Mathlib

Foundations

Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulActionMulAction.IsPretransitive