is_two_preprimitive_strong_jordan

English

If hG IsPreprimitive and s has cardinality n+1 with n+2 < |α|, and hprim is IsPreprimitive of fixingSubgroup, then IsMultiplyPreprimitive G α (n+2).

Русский

Если hG IsPreprimitive, |s| = n+1, n+2 < |α|, и hprim — IsPreprimitive фиксирующей подгруппы, то IsMultiplyPreprimitive G α (n+2).

LaTeX

$$IsMultiplyPreprimitive G α (n+2)$$

Lean4

axiom is_two_preprimitive_strong_jordan (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : s.ncard = n + 1)
    (hsn' : n + 2 < Nat.card α) (hs_prim : IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s)) :
    IsMultiplyPreprimitive (Subgroup.normalClosure (fixingSubgroup G s : Set G)) α 2

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