Theorems · Theorem · group theory

AddAction.set_mem_fixedBy_of_subset_fixedBy

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

If s ⊆ fixedBy α g, then g +ᵥ s = s, which means that s ∈ fixedBy (Set α) g. Note that the reverse implication is in general not true, as s ∈ fixedBy (Set α) g is a weaker statement (it allows for points x ∈ s for which g +ᵥ x ≠ x and g +ᵥ x ∈ s).

Defined in

Mathlib.GroupTheory.GroupAction.FixedPoints

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddAction