Commit 2025-03-19 05:32 ebafbdb4

View on Github →

feat(UniformSpace/Ultra): nonarchimedean uniformities of (indexed) products (#22995)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem IsSymmetricRel.entourageProd

Modified Mathlib/Topology/UniformSpace/Defs.lean

added theorem IsSymmetricRel.iInter

added theorem IsSymmetricRel.preimage_prodMap

Renamed Mathlib/Topology/UniformSpace/Ultra.lean to Mathlib/Topology/UniformSpace/Ultra/Basic.lean

added theorem IsTransitiveRel.iInter

added theorem IsTransitiveRel.inter

added theorem IsTransitiveRel.preimage_prodMap

Created Mathlib/Topology/UniformSpace/Ultra/Constructions.lean

added theorem IsTransitiveRel.entourageProd

added theorem IsUltraUniformity.comap

added theorem IsUltraUniformity.iInf

added theorem IsUltraUniformity.inf