alternatingGroup_le_of_index_le_two

English

If G is a subgroup of Perm α with index ≤ 2, then A_α ≤ G.

Русский

Если G — подгруппа Perm α с индексом ≤ 2, то A_α ⊆ G.

LaTeX

$$$$G.\\operatorname{index} \\le 2 \\Rightarrow \\operatorname{alternatingGroup}(\\alpha) \\le G.$$$$

Lean4

/-- A subgroup of the permutation group of index ≤ 2 contains the alternating group. -/
theorem alternatingGroup_le_of_index_le_two {G : Subgroup (Equiv.Perm α)} (hG : G.index ≤ 2) : alternatingGroup α ≤ G :=
  by
  rcases G.index.eq_zero_or_pos with h | h
  · exact (index_ne_zero_of_finite h).elim
  rcases (Nat.succ_le_iff.mpr h).eq_or_lt' with h | h
  · exact index_eq_one.mp h ▸ le_top
  rw [eq_alternatingGroup_of_index_eq_two (hG.antisymm h)]

Похожие утверждения