forwardOrbit_subset_orbit — Mathlib

English

The forward orbit is contained in the full orbit: forwardOrbit ϕ x ⊆ orbit ϕ x.

Русский

Прямая орбита включена в полную орбиту: forwardOrbit ϕ x ⊆ orbit ϕ x.

LaTeX

$$$forwardOrbit\\\\ ϕ x \\subseteq orbit\\\\ ϕ x.$$$

Lean4

/-- The forward orbit of a point `x` is contained in the orbit of `x`. -/
theorem forwardOrbit_subset_orbit (x : α) : forwardOrbit ϕ x ⊆ orbit ϕ x :=
  ϕ.toAddAction.orbit_addSubmonoid_subset (AddSubmonoid.nonneg τ) x

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