Commit 2025-03-14 10:34 4a709c3e

View on Github →

feat(Topology/UniformSpace): define nonarchimedean uniformity (#22580) prove basic result that such a space is topologically zero dimensional leave todos for future directions

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Ultra.lean

added theorem IsTransitiveRel.ball_subset_of_mem

added theorem IsTransitiveRel.comp_eq_of_idRel_subset

added theorem IsTransitiveRel.comp_subset_self

added theorem IsTransitiveRel.isOpen_ball_of_mem_uniformity

added theorem IsTransitiveRel.symmetrizeRel

added def IsTransitiveRel

added theorem IsUltraUniformity.mk_of_hasBasis

added theorem TopologicalSpace.isTopologicalBasis_clopens

added theorem UniformSpace.ball_eq_of_mem_of_isSymmetricRel_of_isTransitiveRel

added theorem UniformSpace.isClopen_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity

added theorem UniformSpace.isClosed_ball_of_isSymmetricRel_of_isTransitiveRel_of_mem_uniformity

added theorem UniformSpace.nhds_basis_clopens

added theorem isTransitiveRel_empty

added theorem isTransitiveRel_iff_comp_subset_self

added theorem isTransitiveRel_singleton

added theorem isTransitiveRel_univ

Modified docs/references.bib