nontrivial_of_fixedPoints_ne_univ

English

If the fixed-point set is not all of α, then α is Nontrivial.

Русский

Если множество фиксированных точек не равно всему α, то пространство не тривиально.

LaTeX

$$fixedPoints G α \neq univ \Rightarrow Nontrivial α$$

Lean4

/-- If a group acts nontrivially, then the type is nontrivial -/
@[to_additive /-- If a subgroup acts nontrivially, then the type is nontrivial. -/
    ]
theorem nontrivial_of_fixedPoints_ne_univ (h : fixedPoints G α ≠ .univ) : Nontrivial α :=
  (subsingleton_or_nontrivial α).resolve_left fun _ ↦ h fixedPoints_of_subsingleton

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