orbit — Mathlib

English

The orbit of the class of a with Quotient.mk'' equals the G-orbit of a.

Русский

Орбита класса a по отношению к mk'' равна орбите a по действию G.

LaTeX

$$$\text{MulAction.orbitRel.Quotient.orbit}(\text{Quotient.mk'' } a) = \operatorname{Orb}_G(a)$$$

Lean4

/-- The orbit corresponding to an element of the quotient by `MulAction.orbitRel` -/
@[to_additive /-- The orbit corresponding to an element of the quotient by `AddAction.orbitRel` -/
    ]
nonrec def orbit (x : orbitRel.Quotient G α) : Set α :=
  Quotient.liftOn' x (orbit G) fun _ _ => MulAction.orbit_eq_iff.2

Похожие утверждения