Topological transitivity

Conjectura.Defs.Mathematics.Analysis.Dynamics.TopologicallyTransitive

/-
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.Topology.Defs.Basic

/-! # Topological transitivity -/

namespace Conjectura.Dynamics

/-- A map is **topologically transitive** when any two non-empty open sets are eventually
connected by iteration. Equivalent to having a dense orbit on nice spaces, but stated without
reference to a particular point. -/
def TopologicallyTransitive {X : Type*} [TopologicalSpace X] (f : X → X) : Prop :=
  ∀ U V : Set X, IsOpen U → IsOpen V → U.Nonempty → V.Nonempty →
    ∃ n : ℕ, (f^[n] '' U ∩ V).Nonempty

end Conjectura.Dynamics