mathlib3
b40ac2af - chore(topology): make topological_space fields protected (#2867)

Commit

5 years ago

chore(topology): make topological_space fields protected (#2867) This uses the recent `protect_proj` attribute (#2855).

Author

rwbarton

Parents