Theorems · Theorem · group theory

AddAction.set_mem_fixedBy_of_movedBy_subset

∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {g : G},
  (AddAction.fixedBy α g)ᶜ ⊆ s → s ∈ AddAction.fixedBy (Set α) g

If (fixedBy α g)ᶜ ⊆ s, then g cannot move a point of s outside of s.

Defined in

Mathlib.GroupTheory.GroupAction.FixedPoints

Cited by

1 results in Mathlib

Foundations

Depth 19 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddGroupAddAction