Theorems · Theorem · group theory

AddAction.orbitRel.Quotient.orbit_eq_orbit_out

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (x : AddAction.orbitRel.Quotient G α)
  {φ : AddAction.orbitRel.Quotient G α → α}, Function.RightInverse φ Quotient.mk' → x.orbit = AddAction.orbit G (φ x)

Note that hφ = Quotient.out_eq' is a useful choice here.

Defined in

Mathlib.GroupTheory.GroupAction.Defs

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddGroupAddAction