fst_mem_orbit_of_mem_orbit — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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