isInvariant_orbit — Mathlib

English

For any x ∈ α, the orbit of x under ϕ is invariant under ϕ; equivalently, for all t ∈ τ, ϕ(t) maps the orbit of x into itself.

Русский

Для любого x ∈ α орбита x под действием ϕ инвариантна относительно ϕ; то есть для каждого t ∈ τ отображение ϕ(t) отправляет орбиту x в саму орбиту.

LaTeX

$$$IsInvariant\\\\ ϕ\\\\ (orbit\\\\ ϕ\\\\ x).$$$

Lean4

/-- The orbit of a point under a flow `ϕ` is invariant under `ϕ`. -/
theorem isInvariant_orbit (x : α) : IsInvariant ϕ (orbit ϕ x) := fun t _ => ϕ.toAddAction.mem_orbit_of_mem_orbit t

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