mathlib3
2738f9b4 - chore(topology/*): @uniformity α _ becomes 𝓤 α (#814)

Commit

6 years ago

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

References

Author

PatrickMassot

Committer

johoelzl

Parents