Forward orbit
forwardOrbitdef
The forward orbit of a point is everything reachable by iterating the map.
def forwardOrbit {X : Type*} (f : X → X) (x : X) : Set X := {y | ∃ n : ℕ, f^[n] x = y}Used by
From Mathlib
import Conjectura.Defs.Mathematics.Analysis.Dynamics.Orbit · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors