Fixed blocks of pretransitive actions #
A set fixed by every element of a group acting pretransitively is empty or the whole space:
any point of the set reaches every point of the space inside the set. This is the triviality
lemma for MulAction.IsFixedBlock missing next to mathlib's MulAction.IsBlock API.
Main results #
MulAction.IsFixedBlock.eq_empty_or_univ: a fixed block of a pretransitive action is∅orSet.univ.
theorem
MulAction.IsFixedBlock.eq_empty_or_univ
{G : Type u_1}
{X : Type u_2}
[Group G]
[MulAction G X]
[IsPretransitive G X]
{B : Set X}
(hB : IsFixedBlock G B)
:
B = ∅ ∨ B = Set.univ
A fixed block of a pretransitive action is empty or the whole space.