mem_orbit_iff — Mathlib

English

For any x1, x2, x2 ∈ orbit x1 iff ∃ t with ϕ(t)(x1) = x2.

Русский

Для любых x1, x2: x2 принадлежит орбите x1 тогда и только тогда, когда существует t, такое что ϕ(t)(x1) = x2.

LaTeX

$$$x_2 \in \mathrm{orbit}(\varphi, x_1) \iff \exists t \in \tau,\ \varphi(t)(x_1) = x_2$$$

Lean4

theorem mem_orbit_iff {x₁ x₂ : α} : x₂ ∈ orbit ϕ x₁ ↔ ∃ t : τ, ϕ t x₁ = x₂ :=
  ϕ.toAddAction.mem_orbit_iff

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