Commit 2021-03-11 13:28 653fd292

refactor(topology): make is_closed a class (#6552) In lean-liquid, it would be useful that is_closed would be a class, to be able to infer a normed space structure on E/F when F is a closed subspace of a normed space E. This is implemented in this PR. This is mostly straightforward: the only proofs that need fixing are those abusing defeqness, so the new version makes them clearer IMHO.