Theorems · Theorem · group theory

MulAction.isSimpleOrder_blockMem_iff_isPreprimitive

∀ (G : Type u_3) [inst : Group G] {X : Type u_4} [inst_1 : MulAction G X] [MulAction.IsPretransitive G X] [Nontrivial X]
  (a : X), IsSimpleOrder (MulAction.BlockMem G a) ↔ MulAction.IsPreprimitive G X

A pretransitive action on a nontrivial type is preprimitive iff the set of blocks containing a given element is a simple order

Defined in

Mathlib.GroupTheory.GroupAction.Primitive

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPretransitiveNontrivial