Commit 2023-02-03 23:53 0a2e56f9

View on Github →

feat: Port/Topology.UniformSpace.Pi (#2048) port of topology.uniform_space.pi all simple fixes

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/UniformSpace/Pi.lean

added theorem Pi.uniformContinuous_proj

added theorem Pi.uniformity

added theorem uniformContinuous_pi