Commit 2024-03-20 13:11 3a427de2

View on Github →

refactor(UniformSpace): change the definition (#10901)

  • replace isOpen_uniformity with nhds_eq_comap_uniformity as I suggested in #2028
  • don't extend UniformSpace.Core so that we can drop refl, as it follows from nhds_eq_comap_uniformity;
  • drop UniformSpace.mk' - can't be a match_pattern anymore;
  • deprecate UniformSpace.ofNhdsEqComap.

Estimated changes

modified def UniformSpace.comap
deleted def UniformSpace.mk'
modified def UniformSpace.ofCore
modified theorem nhds_eq_comap_uniformity