Theorems · Theorem · group theory

MulAction.IsPreprimitive.exists_mem_smul_and_notMem_smul

∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [MulAction.IsPreprimitive G X] {A : Set X},
  A.Finite → A.Nonempty → A ≠ Set.univ → ∀ {a b : X}, a ≠ b → ∃ g, a ∈ g • A ∧ b ∉ g • A

Theorem of Rudio (Wielandt, 1964, Th. 8.1) For a preprimitive action, a subset which is neither empty nor full has a translate which contains a given point and avoids another one.

Defined in

Mathlib.GroupTheory.GroupAction.Primitive

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulActionMulAction.IsPreprimitive