Commit 2025-12-19 15:37 87f53667

View on Github →

refactor(Dynamics): use SetRel notions of separation and cover (#31259) ... instead of the handmade ones.

Estimated changes

Modified Mathlib/Data/Rel/Cover.lean

added theorem SetRel.IsCover.union

added theorem SetRel.isCover_id

deleted theorem SetRel.isCover_relId

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

modified theorem Dynamics.IsDynCoverOf.coverEntropyEntourage_le_log_card_div

modified theorem Dynamics.IsDynCoverOf.coverMincard_le_card

modified theorem Dynamics.IsDynCoverOf.iterate_le_pow

deleted theorem Dynamics.IsDynCoverOf.nonempty

modified theorem Dynamics.IsDynCoverOf.nonempty_inter

modified theorem Dynamics.IsDynCoverOf.of_entourage_subset

modified theorem Dynamics.IsDynCoverOf.of_le

modified theorem Dynamics.coverEntropyEntourage_empty

modified theorem Dynamics.coverEntropyEntourage_finite_of_isCompact_invariant

modified theorem Dynamics.coverEntropyEntourage_le_coverEntropy

modified theorem Dynamics.coverEntropyEntourage_le_coverEntropyInfEntourage

modified theorem Dynamics.coverEntropyEntourage_le_log_coverMincard_div

modified theorem Dynamics.coverEntropyEntourage_nonneg

modified theorem Dynamics.coverEntropyEntourage_univ

modified theorem Dynamics.coverEntropyInfEntourage_empty

modified theorem Dynamics.coverEntropyInfEntourage_le_coverEntropyInf

modified theorem Dynamics.coverEntropyInfEntourage_nonneg

modified theorem Dynamics.coverEntropyInfEntourage_univ

modified theorem Dynamics.coverEntropyInf_empty

modified theorem Dynamics.coverEntropyInf_eq_coverEntropy

modified theorem Dynamics.coverEntropyInf_nonneg

modified theorem Dynamics.coverEntropy_empty

modified theorem Dynamics.coverEntropy_nonneg

modified theorem Dynamics.coverMincard_empty

modified theorem Dynamics.coverMincard_finite_of_isCompact_invariant

modified theorem Dynamics.coverMincard_finite_of_isCompact_uniformContinuous

modified theorem Dynamics.coverMincard_le_pow

modified theorem Dynamics.coverMincard_mul_le_pow

modified theorem Dynamics.coverMincard_univ

modified theorem Dynamics.coverMincard_zero

modified theorem Dynamics.exists_isDynCoverOf_of_isCompact_invariant

modified theorem Dynamics.exists_isDynCoverOf_of_isCompact_uniformContinuous

modified theorem Dynamics.isDynCoverOf_empty

added theorem Dynamics.isDynCoverOf_empty_right

modified theorem Dynamics.isDynCoverOf_univ

modified theorem Dynamics.isDynCoverOf_zero

modified theorem Dynamics.nonempty_inter_of_coverMincard

Modified Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

added theorem Dynamics.dynEntourage_mono

Modified Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

modified theorem Dynamics.IsDynNetIn.card_le_card_of_isDynCoverOf

modified theorem Dynamics.netEntropyEntourage_le_coverEntropyEntourage

modified theorem Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage

modified theorem Dynamics.netMaxcard_le_coverMincard

Modified Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean

Modified Mathlib/Dynamics/TopologicalEntropy/Subset.lean

modified theorem Dynamics.IsDynCoverOf.closure

modified theorem Dynamics.IsDynCoverOf.monotone_subset

modified theorem Dynamics.IsDynCoverOf.union

modified theorem Dynamics.IsDynNetIn.monotone_subset

modified theorem Dynamics.coverEntropyEntourage_closure

modified theorem Dynamics.coverEntropyEntourage_monotone

modified theorem Dynamics.coverEntropyEntourage_union

modified theorem Dynamics.coverEntropyInfEntourage_closure

modified theorem Dynamics.coverEntropyInfEntourage_monotone

modified theorem Dynamics.coverEntropyInf_closure

modified theorem Dynamics.coverEntropy_closure

modified theorem Dynamics.coverEntropy_union

modified theorem Dynamics.coverMincard_closure_le

modified theorem Dynamics.coverMincard_monotone_subset

modified theorem Dynamics.coverMincard_union_le

modified theorem Dynamics.netEntropyEntourage_monotone

modified theorem Dynamics.netEntropyInfEntourage_monotone

modified theorem Dynamics.netMaxcard_monotone_subset

Modified Mathlib/Topology/UniformSpace/Defs.lean

added theorem UniformSpace.isCover_iff_subset_iUnion_ball