Mathlib Map

Theorems · Definition · dynamical systems

Dynamics.dynEntourage

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

The dynamical entourage associated to a transformation T, entourage U and time n is the entourage where x and y are close iff T^[k] x and T^[k] y are U-close for all k < n, i.e. iff they are U-close up to time n.

Defined in
Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Cited by
28 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Dynamics.IsDynCoverOf · cited by 36Dynamics.IsDynCoverOfDynamics.IsDynNetIn · cited by 18Dynamics.IsDynNetInDynamics.dynEntourage_comp_subset · cited by 3Dynamics.dynEntourage_com…Dynamics.dynEntourage_eq_inter_Ico · cited by 3Dynamics.dynEntourage_eq_…Dynamics.dynEntourage_monotone · cited by 3Dynamics.dynEntourage_mon…Dynamics.dynEntourage_antitone · cited by 2Dynamics.dynEntourage_ant…Dynamics.dynEntourage_mono · cited by 2Dynamics.dynEntourage_monoDynamics.dynEntourage_univ · cited by 2Dynamics.dynEntourage_univDynamics.dynEntourage_zero · cited by 2Dynamics.dynEntourage_zeroFunction.Semiconj.preimage_dynEntourage · cited by 2Semiconj.preimage_dynEnto…Dynamics.netMaxcard_univ · cited by 2Dynamics.netMaxcard_univDynamics.coverMincard_le_netMaxcard · cited by 2Dynamics.coverMincard_le_…Dynamics.IsDynCoverOf.iterate_le_pow · cited by 2IsDynCoverOf.iterate_le_p…Dynamics.IsDynCoverOf.preimage · cited by 1IsDynCoverOf.preimageDynamics.dynEntourage_mem_uniformity · cited by 1Dynamics.dynEntourage_mem…Set.preimage · cited by 4946Set.preimageSet.iInter · cited by 1084Set.iInterNat.iterate · cited by 740Nat.iterateSetRel · cited by 581SetRelDynamics.dynEntourageCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by30

Results whose statement or proof uses this declaration.