Theorems · Theorem · group theory

AddAction.IsPreprimitive.exists_mem_vadd_and_notMem_vadd

∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [AddAction.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 additive 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

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddActionAddAction.IsPreprimitive