Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-29 14:38 49f700c7

View on Github →

feat(analysis/topology/uniform_space): prepare for completions (#297)

Estimated changes

Modified analysis/topology/uniform_space.lean

added theorem eq_of_separated_of_uniform_continuous

added theorem separated_of_uniform_continuous

added theorem separation_prod

modified theorem uniform_continuous.prod_mk

added theorem uniform_continuous.prod_mk_left

added theorem uniform_continuous.prod_mk_right

added theorem uniform_continuous_quotient

added theorem uniform_continuous_quotient_lift

added theorem uniform_continuous_quotient_lift₂

added theorem uniformity_quotient