snd_mem_orbit_of_mem_orbit — Mathlib

English

If (x1,x2) remains in the orbit of y=(y1,y2) under M, then x2 lies in the orbit of y2 under M.

Русский

Если (x1,x2) принадлежит орбите y=(y1,y2) по действию M, то x2 принадлежит орбите y2 по M.

LaTeX

$$$$x=(x_1,x_2),\\; y=(y_1,y_2),\\; x \\in \\operatorname{Orbit}_M(y) \\Rightarrow x_2 \\in \\operatorname{Orbit}_M(y_2).$$$$

Lean4

@[to_additive]
theorem snd_mem_orbit_of_mem_orbit {x y : α × β} (h : x ∈ MulAction.orbit M y) : x.2 ∈ MulAction.orbit M y.2 :=
  by
  rcases h with ⟨g, rfl⟩
  exact mem_orbit _ _

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