Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-03 09:38 c3aba261

View on Github →

feat(topology/uniform_space/pi): indexed products of uniform spaces (#845)

  • feat(topology/uniform_space/pi): indexed products of uniform spaces
  • fix(topology/uniform_space/pi): defeq topology
  • fix(src/topology/uniform_space/pi): typo Co-Authored-By: PatrickMassot patrickmassot@free.fr

Estimated changes

modified theorem uniformity_prod
added theorem Pi.uniformity