Mathlib v3 is deprecated. Go to Mathlib v4

Theorem prod_uniformity

Modification history

2018-07-30 10:41

analysis/topology/uniform_space.lean

chore(analysis/topology/uniform_space): remove redundant prod_uniformity (redundant to uniformity_prod)

Deleted prod_uniformity View on Github →

2018-01-12 13:08

analysis/topology/uniform_space.lean

feat(analysis/metric_space): sup metric for product of metric spaces

Added prod_uniformity View on Github →