Dense orbit

Conjectura.Defs.Mathematics.Analysis.Dynamics.DenseOrbit

/-
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 Conjectura.Defs.Mathematics.Analysis.Dynamics.Orbit
import Mathlib.Topology.Defs.Basic

/-! # Dense orbit -/

namespace Conjectura.Dynamics

/-- A point has a **dense orbit** when its `forwardOrbit` comes arbitrarily close to every
point of the space. A single dense orbit is the usual working definition of chaos. -/
def HasDenseOrbit {X : Type*} [TopologicalSpace X] (f : X → X) (x : X) : Prop :=
  Dense (forwardOrbit f x)

end Conjectura.Dynamics