Theorems · Definition · dynamical systems

Dynamics.netMaxcard

{X : Type u_1} → (X → X) → Set X → SetRel X X → ℕ → ℕ∞

The largest cardinality of a (U, n)-dynamical net of F. Takes values in ℕ∞, and is infinite if and only if F admits nets of arbitrarily large size.

Defined in

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Cited by

23 results in Mathlib

Foundations

Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound