English
Given a symmetric generating set S of a permutation group and a nonempty proper subset T of an orbit, there exists a generator in S that sends some element of T outside T.
Русский
Пусть S – симметричный набор генерирующих перестановок группы по орбитам. Если T непустое, proper подмножество орбиты, то найдётся σ ∈ S такой, что σ•a ∉ T для некоторого a ∈ T.
LaTeX
$$$\\exists \\sigma \\in S, \\exists a \\in T, \\sigma \\cdot a \\notin T$$$
Lean4
/-- 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. -/
theorem exists_smul_notMem_of_subset_orbit_closure (S : Set G) (T : Set α) {a : α} (hS : ∀ g ∈ S, g⁻¹ ∈ S)
(subset : T ⊆ orbit (closure S) a) (notMem : a ∉ T) (nonempty : T.Nonempty) : ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T :=
by
have key0 : ¬closure S ≤ stabilizer G T := by
have ⟨b, hb⟩ := nonempty
obtain ⟨σ, rfl⟩ := subset hb
contrapose! notMem with h
exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)
contrapose! key0
refine (closure_le _).mpr fun σ hσ ↦ ?_
simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]
exact fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩
