Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-21 19:09 eff9ed3a

View on Github →

feat(topology/uniform_space): some basic lemmas (#3123) This is the second PR on the road to Heine. It contains various elementary lemmas about uniform spaces.

Estimated changes

Modified src/topology/uniform_space/basic.lean

added theorem closure_eq_uniformity

added theorem comp_comp_symm_mem_uniformity_sets

added theorem comp_rel_mono

added theorem comp_symm_mem_uniformity_sets

added theorem mem_comp_comp

added theorem mem_comp_of_mem_ball

added theorem subset_comp_self

added theorem subset_comp_self_of_mem_uniformity

added theorem symmetric_rel_inter

added theorem uniform_space.ball_mem_nhds

added theorem uniform_space.has_basis_nhds

added theorem uniform_space.has_basis_nhds_prod

added theorem uniform_space.mem_nhds_iff

added theorem uniform_space.mem_nhds_iff_symm

added theorem uniformity_comap

added theorem uniformity_has_basis_closed

added theorem uniformity_has_basis_closure