Theorems · Theorem · dynamical systems

Dynamics.coverEntropy_restrict_subset

∀ {X : Type u_1} [inst : UniformSpace X] {T : X → X} {F G : Set X},
  F ⊆ G →
    ∀ (hG : Set.MapsTo T G G),
      Dynamics.coverEntropy (Set.MapsTo.restrict T G G hG) (Subtype.val ⁻¹' F) = Dynamics.coverEntropy T F

Defined in: Mathlib.Dynamics.TopologicalEntropy.Semiconj
Cited by: 2 results in Mathlib
Foundations: Depth 180 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: UniformSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites12

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
Set.Elemstatement · cited by 7,166
Set.preimagestatement and proof · cited by 4,946
UniformSpacestatement and proof · cited by 2,040
ERealstatement and proof · cited by 793
Set.MapsTostatement and proof · cited by 732
Set.MapsTo.restrictstatement · cited by 57
Set.inter_eq_rightproof · cited by 41
Subtype.image_preimage_coeproof · cited by 37
Dynamics.coverEntropystatement and proof · cited by 22
Set.MapsTo.val_restrict_applyproof · cited by 4
Dynamics.coverEntropy_image_of_comapproof · cited by 2

Cited by2

Results whose statement or proof uses this declaration.

Dynamics.coverEntropy_image_le_of_uniformContinuousOn_invariantproof · cited by 0
Dynamics.coverEntropy_restrictproof · cited by 0