gluing): use `⨅` notation (#5772)

Commit

4 years ago

chore(topology/metric_space/gluing): use `⨅` notation (#5772) Also use `exists_lt_of_cinfi_lt` to golf one proof.

Author

urkud

Parents