Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-01-12 13:08 c39b43fb

View on Github →

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

Estimated changes

Modified algebra/linear_algebra/multivariate_polynomial.lean

Modified analysis/metric_space.lean

added theorem dist_le_zero_iff

Modified analysis/topology/topological_space.lean

Modified analysis/topology/uniform_space.lean

added theorem prod_uniformity

Modified data/equiv.lean

Modified data/prod.lean

added theorem prod.ext

modified theorem prod.mk.eta

Modified order/complete_lattice.lean

modified theorem lattice.infi_inf_eq