Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-12 13:53 2738f9b4

View on Github →

chore(topology/*): @uniformity α _ becomes 𝓤 α (#814) This is a binder type change and a local notation

Estimated changes

modified theorem uniformity_translate
modified theorem metric.uniformity_dist'
modified theorem metric.uniformity_dist
modified theorem uniformity_edist
modified theorem uniformity_edist''
modified theorem uniformity_edist'
modified theorem comp_le_uniformity
modified theorem comp_mem_uniformity_sets
modified theorem comp_symm_of_uniformity
modified theorem interior_mem_uniformity
modified theorem mem_nhds_left
modified theorem mem_nhds_right
modified theorem mem_uniformity_is_closed
modified theorem nhds_eq_comap_uniformity
modified theorem nhds_eq_uniformity
modified theorem nhdset_of_mem_uniformity
modified theorem refl_le_uniformity
modified theorem refl_mem_uniformity
modified theorem symm_le_uniformity
modified theorem symm_of_uniformity
modified theorem tendsto_const_uniformity
modified theorem tendsto_swap_uniformity
modified def uniformity
modified theorem uniformity_eq_symm
modified theorem uniformity_le_symm
modified def cauchy
modified theorem cauchy_iff
modified theorem cauchy_map_iff