Theorems · Theorem · dynamical systems

Dynamics.IsDynNetIn.card_le_card_of_isDynCoverOf

∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {n : ℕ} {F : Set X} {s t : Finset X},
  Dynamics.IsDynNetIn T F U n ↑s → Dynamics.IsDynCoverOf T F U n ↑t → s.card ≤ t.card

Given an entourage U and a time n, a dynamical net has a smaller cardinality than a dynamical cover. This lemma is the first of two key results to compare two versions of topological entropy: with cover and with nets, the second being coverMincard_le_netMaxcard.

Defined in

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Cited by

1 results in Mathlib

Foundations

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