Commit 2025-03-05 19:53 f67561d6

View on Github →

chore(Topology): rename to IsSymmetricRel to indicate prop nature (#22594) Came up in discussion in #22580

Estimated changes

Modified Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean

Modified Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

modified theorem Dynamics.mem_ball_dynEntourage_comp

added theorem IsSymmetricRel.dynEntourage

deleted theorem SymmetricRel.dynEntourage

Modified Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean

modified theorem Dynamics.netMaxcard_le_coverMincard

Modified Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean

Modified Mathlib/MeasureTheory/Measure/RegularityCompacts.lean

Modified Mathlib/Topology/Metrizable/Uniformity.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

Modified Mathlib/Topology/UniformSpace/Cauchy.lean

Modified Mathlib/Topology/UniformSpace/Defs.lean

added theorem IsSymmetricRel.eq

added theorem IsSymmetricRel.inter

added theorem IsSymmetricRel.mk_mem_comm

added def IsSymmetricRel

deleted theorem SymmetricRel.eq

deleted theorem SymmetricRel.inter

deleted theorem SymmetricRel.mk_mem_comm

deleted def SymmetricRel

modified theorem UniformSpace.ball_eq_of_symmetry

modified theorem UniformSpace.mem_ball_symmetry

modified theorem UniformSpace.mem_comp_comp

modified theorem UniformSpace.mem_comp_of_mem_ball

modified theorem symmetric_symmetrizeRel

Modified Mathlib/Topology/UniformSpace/Separation.lean

Modified Mathlib/Topology/UniformSpace/UniformEmbedding.lean