mem_orbit_of_mem_orbit — Mathlib

English

For any M acting on α, the orbit of a is the set {m • a | m ∈ M}. This is the range of the action map m ↦ m • a.

Русский

Для действия группы M на множество α орбита элемента a — это множество {m • a | m ∈ M}. Это образ отображения m ↦ m • a.

LaTeX

$$$\operatorname{orbit}(a) = \{ m \cdot a \mid m \in M \}$$$

Lean4

@[to_additive]
theorem mem_orbit_of_mem_orbit {a₁ a₂ : α} (m : M) (h : a₂ ∈ orbit M a₁) : m • a₂ ∈ orbit M a₁ :=
  by
  obtain ⟨x, rfl⟩ := mem_orbit_iff.mp h
  simp [smul_smul]

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