Mathlib Changelog
v3
Changelog
About
Github
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'