is_two_pretransitive'

Mathlib.GroupTheory.GroupAction.Jordan

URI: https://scilib.ai/kg/mathlib#IsPreprimitive.is_two_pretransitive'

Lean4

axiom is_two_pretransitive' (hG : IsPreprimitive G α) {s : Set α} {n : ℕ} (hsn : Nat.card s = n + 1)
    (hsn' : n + 1 < Nat.card α) (hs_trans : IsPretransitive (fixingSubgroup G s) (SubMulAction.ofFixingSubgroup G s)) :
    IsMultiplyPretransitive (Subgroup.normalClosure (fixingSubgroup G s : Set G)) α 2

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru