mapsTo_smul_orbit — Mathlib

English

The map sending a quotient element to its orbit is injective.

Русский

Отображение, отправляющее элемент квотиента в его орбиту, инъективно.

LaTeX

$$Injective (MulAction.orbitRel.Quotient.orbit)$$

Lean4

@[to_additive]
nonrec theorem mapsTo_smul_orbit (g : G) (x : orbitRel.Quotient G α) : Set.MapsTo (g • ·) x.orbit x.orbit :=
  by
  rw [orbitRel.Quotient.orbit_eq_orbit_out x Quotient.out_eq']
  exact mapsTo_smul_orbit g x.out

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