orbit_smul — Mathlib

English

For a group G acting on α, the orbit of g•a equals the orbit of a: orbit G (g•a) = orbit G a.

Русский

Для группы G, действующей на α, орбита g•a равна орбите a: orbit G (g•a) = orbit G a.

LaTeX

$$$$ \\operatorname{orbit}(G, g \\cdot a) = \\operatorname{orbit}(G, a). $$$$

Lean4

@[to_additive (attr := simp)]
theorem orbit_smul (g : G) (a : α) : orbit G (g • a) = orbit G a :=
  (orbit_smul_subset g a).antisymm <|
    calc
      orbit G a = orbit G (g⁻¹ • g • a) := by rw [inv_smul_smul]
      _ ⊆ orbit G (g • a) := orbit_smul_subset _ _

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