Commit 2021-10-23 14:30 82896b53
View on Github →feat(topology): add a few lemmas (#9885)
Add is_topological_basis.is_open_map_iff,
is_topological_basis.exists_nonempty_subset, and
interior_{s,b,}Inter_subset.
Motivated by lemmas from flypitch.