mathlib3
refactor(topology/*): define and use dense_inducing
#1193

Merged

Commits

refactor(topology/*): define and dense_inducing

PatrickMassot committed 7 years ago
Apply suggestions from code review

PatrickMassot committed 7 years ago
minor fixes following review

PatrickMassot committed 7 years ago
Some more dot notation, consistent naming and field naming

PatrickMassot committed 7 years ago
Merge branch 'master' into extension

mergify[bot] committed 7 years ago