smul_orbit — Mathlib

English

The action by g on the orbit of a leaves the orbit unchanged: g • orbit G a = orbit G a.

Русский

Действие g над орбитой a сохраняет орбиту: g • orbit G a = orbit G a.

LaTeX

$$$ g \cdot orbit\ G\ a = orbit\ G\ a $$$

Lean4

@[to_additive (attr := simp)]
theorem smul_orbit (g : G) (a : α) : g • orbit G a = orbit G a :=
  (smul_orbit_subset g a).antisymm <|
    calc
      orbit G a = g • g⁻¹ • orbit G a := (smul_inv_smul _ _).symm
      _ ⊆ g • orbit G a := Set.image_mono (smul_orbit_subset _ _)

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