Theorems · Theorem · group theory

exists_smul_notMem_of_subset_orbit_closure

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (S : Set G) (T : Set α) {a : α},
  (∀ g ∈ S, g⁻¹ ∈ S) → T ⊆ MulAction.orbit (↥(Subgroup.closure S)) a → a ∉ T → T.Nonempty → ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Given a symmetric generating set of a permutation group, if T is a nonempty proper subset of an orbit, then there exists a generator that sends some element of T into the complement of T.

Defined in

Mathlib.GroupTheory.Perm.ClosureSwap

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupMulAction