Dense orbit
HasDenseOrbitdef
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)Builds on
From Mathlib
import Conjectura.Defs.Mathematics.Analysis.Dynamics.DenseOrbit · 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