Quotient — Mathlib

English

The orbit corresponding to an element of the quotient by the orbit relation equals the ordinary G-orbit of a representative.

Русский

Орбита элемента в фактор-множество по отношению орбит равна обычной орбите элемента под действием G.

LaTeX

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

Lean4

/-- The quotient by `MulAction.orbitRel`, given a name to enable dot notation. -/
@[to_additive /-- The quotient by `AddAction.orbitRel`, given a name to enable dot notation. -/
    ]
abbrev Quotient : Type _ :=
  _root_.Quotient <| orbitRel G α

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