Theorems · Theorem · group theory

AddAction.quotient_preimage_image_eq_union_add

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (U : Set α),
  Quotient.mk' ⁻¹' Quotient.mk' '' U = ⋃ g, (fun x => g +ᵥ x) '' U

When you take a set U in α, push it down to the quotient, and pull back, you get the union of the orbit of U under G.

Defined in

Mathlib.GroupTheory.GroupAction.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction