mathlib3
feat(topology/uniform_space/uniform_convergence_topology): `𝔖`-convergence depends only on the bornology generated by `𝔖`
#18009
Open

Commits
  • Initial commit
    ADedecker committed 3 years ago
  • First part done
    ADedecker committed 3 years ago
  • Initial commit
    ADedecker committed 3 years ago
  • More progress
    ADedecker committed 3 years ago
  • Done?
    ADedecker committed 3 years ago
  • Done?
    ADedecker committed 3 years ago
  • Fix
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_generated_bornology
    ADedecker committed 3 years ago
  • Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_generated_bornology
    ADedecker committed 3 years ago
Loading