isCoatom_stabilizer_of_isPreprimitive

English

Let G act on X with X nontrivial and the action preprimitive. Then for every a ∈ X, the stabilizer of a, denoted Stab_G(a), is a maximal subgroup of G.

Русский

Пусть G действует на X, X непусто и действие является предпримитивным. Тогда стабилизатор элемента a ∈ X, обозначаемый Stab_G(a), является максимальной подгруппой G.

LaTeX

$$$\\forall a \\in X,\\; \\operatorname{Stab}_G(a) \\le G \\land \\forall K\\;( \\operatorname{Stab}_G(a) \\le K \\le G \\Rightarrow K = \\operatorname{Stab}_G(a) \\lor K = G )$$$

Lean4

/-- In a preprimitive action, stabilizers are maximal subgroups -/
@[to_additive /-- In a preprimitive action, stabilizers are maximal subgroups. -/
    ]
theorem isCoatom_stabilizer_of_isPreprimitive [Nontrivial X] [IsPreprimitive G X] (a : X) : IsCoatom (stabilizer G a) :=
  by rwa [isCoatom_stabilizer_iff_preprimitive]

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