English
If the fixed points are not top and the trivial blocks condition holds for all blocks, then the action is preprimitive.
Русский
Если множество фиксированных точек не равно универсуму и условие тривиальных блоков выполняется для всех блоков, то действие предпримитивно.
LaTeX
$$theorem mk' (Hnt : fixedPoints G X ≠ ⊤) (H : ∀ {B : Set X} (_ : IsBlock G B), IsTrivialBlock B) : IsPreprimitive G X$$
Lean4
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) -/
@[to_additive /-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) -/
]
theorem mk' (Hnt : fixedPoints G X ≠ ⊤) (H : ∀ {B : Set X} (_ : IsBlock G B), IsTrivialBlock B) : IsPreprimitive G X :=
by
simp only [Set.top_eq_univ, Set.ne_univ_iff_exists_notMem] at Hnt
obtain ⟨_, ha⟩ := Hnt
exact .of_isTrivialBlock_of_notMem_fixedPoints ha fun {B} _ ↦ H
