Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-08-28 10:14 721d67a7

View on Github →

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

Estimated changes

Modified src/topology/uniform_space/basic.lean

modified theorem mem_uniformity_is_closed

modified theorem sum.uniformity

modified theorem to_topological_space_prod

Modified src/topology/uniform_space/cauchy.lean

modified theorem cauchy_iff_exists_le_nhds

modified theorem cauchy_map_iff_exists_tendsto

modified def cauchy_seq

modified theorem cauchy_seq_tendsto_of_complete

modified theorem cauchy_seq_tendsto_of_is_complete

modified theorem totally_bounded_closure

modified theorem totally_bounded_empty

modified theorem totally_bounded_image

modified theorem totally_bounded_subset

Modified src/topology/uniform_space/completion.lean

Modified src/topology/uniform_space/separation.lean

modified theorem uniform_space.uniform_continuous_quotient_lift₂

Modified src/topology/uniform_space/uniform_embedding.lean

added theorem uniform_inducing.mk'

deleted def uniform_inducing.mk'