Theorems · Theorem · group theory

SubAddAction.mem_ofFixingAddSubgroup_insert_iff

∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α}
  {s : Set ↥(SubAddAction.ofStabilizer M a)} {x : α},
  x ∈ SubAddAction.ofFixingAddSubgroup M (insert a ((fun x => ↑x) '' s)) ↔
    ∃ (hx : x ∈ SubAddAction.ofStabilizer M a),
      ⟨x, hx⟩ ∈ SubAddAction.ofFixingAddSubgroup (↥(AddAction.stabilizer M a)) s

Defined in

Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction