mathlib
76f15230
- Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_generated_bornology
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
Merge remote-tracking branch 'origin/master' into AD_uniform_convergence_generated_bornology
References
AD_uniform_convergence_generated_bornology
#18009 - feat(topology/uniform_space/uniform_convergence_topology): `𝔖`-convergence depends only on the bornology generated by `𝔖`
Author
ADedecker
Parents
8fd8f445
9a48a083
Loading