mathlib
b7655704 - chore(topology): rename interior_eq_of_open (#3614)

Commit

5 years ago

chore(topology): rename interior_eq_of_open (#3614) This allows to use dot notation and is more consistent with its closed twin is_closed.closure_eq

Author

PatrickMassot

Parents