Commit 2025-04-24 17:34 d9004fd6

View on Github →

feat(Dynamics/TopologicalEntropy): Topological entropy and subsets (#24262) This file implements basic facts about the topological entropy of subsets of a dynamical system: monotonicity, closure, unions.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

added theorem Dynamics.ball_dynEntourage_mem_nhds

Created Mathlib/Dynamics/TopologicalEntropy/Subset.lean

added theorem Dynamics.IsDynCoverOf.closure

added theorem Dynamics.IsDynCoverOf.monotone_subset

added theorem Dynamics.IsDynCoverOf.union

added theorem Dynamics.IsDynNetIn.monotone_subset

added theorem Dynamics.coverEntropyEntourage_closure

added theorem Dynamics.coverEntropyEntourage_monotone

added theorem Dynamics.coverEntropyEntourage_union

added theorem Dynamics.coverEntropyInfEntourage_closure

added theorem Dynamics.coverEntropyInfEntourage_monotone

added theorem Dynamics.coverEntropyInf_biUnion_le

added theorem Dynamics.coverEntropyInf_closure

added theorem Dynamics.coverEntropyInf_iUnion_le

added theorem Dynamics.coverEntropyInf_monotone

added theorem Dynamics.coverEntropy_biUnion_finset

added theorem Dynamics.coverEntropy_biUnion_le

added theorem Dynamics.coverEntropy_closure

added theorem Dynamics.coverEntropy_iUnion_le

added theorem Dynamics.coverEntropy_iUnion_of_finite

added theorem Dynamics.coverEntropy_monotone

added theorem Dynamics.coverEntropy_union

added theorem Dynamics.coverMincard_closure_le

added theorem Dynamics.coverMincard_monotone_subset

added theorem Dynamics.coverMincard_union_le

added theorem Dynamics.netEntropyEntourage_monotone

added theorem Dynamics.netEntropyInfEntourage_monotone

added theorem Dynamics.netMaxcard_monotone_subset

Modified Mathlib/Topology/UniformSpace/Defs.lean

added theorem UniformSpace.ball_iInter