Theorems · Definition · dynamical systems
Dynamics.coverEntropyInf
{X : Type u_1} → [UniformSpace X] → (X → X) → Set X → ERealThe entropy of T restricted to F, obtained by taking the supremum
of coverEntropyInfEntourage over entourages. Note that this supremum is approached by taking
small entourages. This second version uses a liminf, and is chosen as an alternative
definition for topological entropy.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- UniformSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- iSupproof · cited by 2,415
- UniformSpacestatement and proof · cited by 2,040
- ERealstatement · cited by 793
- uniformityproof · cited by 765
- Dynamics.coverEntropyInfEntourageproof · cited by 15
Cited by18
Results whose statement or proof uses this declaration.
- Dynamics.coverEntropyInf_monotonestatement · cited by 3
- Dynamics.coverEntropyInfEntourage_le_coverEntropyInfstatement · cited by 2
- Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntouragestatement · cited by 2
- Dynamics.coverEntropyInf_image_of_comapstatement · cited by 2
- Dynamics.coverEntropyInf_le_coverEntropystatement · cited by 2
- Dynamics.coverEntropyInf_antitonestatement · cited by 1
- Dynamics.coverEntropyInf_image_le_of_uniformContinuousstatement and proof · cited by 1
- Dynamics.coverEntropyInf_nonnegstatement · cited by 1
- Dynamics.coverEntropyInf_restrict_subsetstatement and proof · cited by 1
- Dynamics.coverEntropyInf_biUnion_lestatement · cited by 0
- Dynamics.coverEntropyInf_closurestatement · cited by 0
- Dynamics.coverEntropyInf_emptystatement · cited by 0