Topological transitivity

TopologicallyTransitivedef

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

From Mathlib

Logic.Function.Iterate
Topology.Defs.Basic

import Conjectura.Defs.Mathematics.Analysis.Dynamics.TopologicallyTransitive · 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

Full credits