Theorems · Theorem · dynamical systems
Dynamics.coverEntropy_image_of_comap
∀ {X : Type u_1} {Y : Type u_2} (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y},
Function.Semiconj φ S T → ∀ (F : Set X), Dynamics.coverEntropy T (φ '' F) = Dynamics.coverEntropy S FThe entropy of φ '' F equals the entropy of F if X is endowed with the pullback by φ
of the uniform structure of Y.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites27
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
- Filterproof · cited by 8,121
- Set.imagestatement and proof · cited by 5,609
- Set.preimageproof · cited by 4,946
- LE.le.transproof · cited by 3,151
- le_antisymmproof · cited by 2,068
- UniformSpacestatement and proof · cited by 2,040
- ERealstatement · cited by 793
- uniformityproof · cited by 765
- Set.Subset.rflproof · cited by 255
- SetRel.compproof · cited by 136
- iSup₂_leproof · cited by 96
Cited by2
Results whose statement or proof uses this declaration.
- Dynamics.coverEntropy_restrict_subsetproof · cited by 2
- Dynamics.coverEntropy_image_le_of_uniformContinuousproof · cited by 1