Theorems · Theorem · group theory

MulAction.orbitRel.Quotient.orbit_eq_orbit_out

∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α)
  {φ : MulAction.orbitRel.Quotient G α → α}, Function.RightInverse φ Quotient.mk' → x.orbit = MulAction.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

GroupMulAction