Commit 2025-10-24 14:57 c65bb0b8

View on Github →

refactor(Topology/UniformSpace): use SetRel (#23181) What's left in UniformSpace.Defs is precisely the theory of the uniformity filter. The motivation is that the theory of coverings and packings in both high dimensional probability and dynamics can be based on entourages, while they have little to do with the uniformity filter (indeed, entourages are in a sense a quantitative version of the uniformity filter).

Estimated changes

modified theorem Dynamics.IsDynCoverOf.of_le
modified def Dynamics.IsDynCoverOf
modified theorem Dynamics.coverMincard_empty
modified theorem Dynamics.coverMincard_zero
modified theorem Dynamics.isDynCoverOf_empty
modified theorem Dynamics.isDynCoverOf_zero
modified def Dynamics.dynEntourage
modified theorem Dynamics.dynEntourage_one
modified theorem Dynamics.dynEntourage_zero
modified theorem Dynamics.mem_dynEntourage
modified theorem Dynamics.IsDynNetIn.of_le
modified def Dynamics.IsDynNetIn
modified theorem Dynamics.isDynNetIn_empty
modified theorem Dynamics.netMaxcard_empty
modified theorem Dynamics.netMaxcard_univ
modified theorem Dynamics.netMaxcard_zero
modified theorem Dynamics.IsDynCoverOf.image
modified theorem UniformSpace.isClosed_ball
modified theorem UniformSpace.isOpen_ball
modified theorem ball_entourageProd
modified theorem ball_preimage
modified theorem bot_uniformity
modified theorem closure_eq_inter_uniformity
modified def entourageProd
modified theorem interior_mem_uniformity
modified theorem mem_entourageProd
modified theorem mem_uniformity_isClosed
modified theorem nhdset_of_mem_uniformity
modified theorem uniformity_hasBasis_closure
modified theorem uniformity_hasBasis_open
modified theorem union_mem_uniformity_sum
modified theorem CauchySeq.subseq_mem
modified theorem CauchySeq.subseq_subseq_mem
modified theorem Filter.HasBasis.cauchy_iff
modified theorem cauchySeq_of_controlled
modified def interUnionBalls
modified def CauchyFilter.gen
modified theorem CauchyFilter.monotone_gen
modified theorem IsSymmetricRel.eq
modified theorem IsSymmetricRel.iInter
modified theorem IsSymmetricRel.inter
modified theorem IsSymmetricRel.mk_mem_comm
modified theorem IsSymmetricRel.sInter
modified def IsSymmetricRel
modified theorem Monotone.compRel
modified theorem UniformSpace.ball_mem_nhds
modified theorem UniformSpace.mem_ball_self
modified theorem UniformSpace.mem_comp_comp
modified theorem comp3_mem_uniformity
modified def compRel
modified theorem compRel_assoc
deleted theorem compRel_mono
modified theorem comp_le_uniformity3
modified theorem comp_le_uniformity
modified theorem comp_mem_uniformity_sets
modified theorem comp_symm_of_uniformity
modified theorem idRel_subset
modified theorem id_compRel
deleted theorem isSymmetricRel_idRel
deleted theorem isSymmetricRel_univ
modified theorem left_subset_compRel
modified theorem lift'_comp_uniformity
modified theorem mem_compRel
modified theorem mem_nhds_left
modified theorem mem_nhds_right
modified theorem mem_uniformity_of_eq
modified theorem nhds_basis_uniformity'
modified theorem nhds_basis_uniformity
deleted theorem prodMk_mem_compRel
modified theorem refl_le_uniformity
modified theorem refl_mem_uniformity
modified theorem right_subset_compRel
modified theorem subset_comp_self
modified theorem subset_iterate_compRel
modified theorem symm_of_uniformity
modified theorem symmetric_symmetrizeRel
modified def symmetrizeRel
modified theorem symmetrizeRel_subset_self
modified theorem symmetrize_mem_uniformity
modified theorem symmetrize_mono
modified theorem uniformity_lift_le_comp
modified theorem uniformity_lift_le_swap
modified theorem IsTransitiveRel.iInter
modified theorem IsTransitiveRel.inter
modified theorem IsTransitiveRel.sInter
modified def IsTransitiveRel
added theorem ball_eq_of_mem
added theorem ball_subset_of_mem
deleted theorem isTransitiveRel_idRel