Forward orbit

Conjectura.Defs.Mathematics.Analysis.Dynamics.Orbit

/-
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
-/
import Mathlib.Logic.Function.Iterate
import Mathlib.Data.Set.Defs

/-! # Forward orbit -/

namespace Conjectura.Dynamics

/-- 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}

end Conjectura.Dynamics