Mathlib v3 is deprecated. Go to Mathlib v4

Theorem to_topological_space_prod

Modification history

2019-08-28 10:14

src/topology/uniform_space/basic.lean

fix(topology/uniform_space): sanity_check pass (#1364)

Modified to_topological_space_prod View on Github →

2017-08-10 16:36

topology/uniform_space.lean

construct reals as complete, linear ordered field

Added to_topological_space_prod View on Github →