mathlib
ea9dae21 - refactor(topology/*): Use `disjoint` (#14950)

Commit

3 years ago

refactor(topology/*): Use `disjoint` (#14950) Replace uses of `s ∩ t = ∅` by `disjoint s t` in the topology library. This shortens proofs.

Author

YaelDillies

Parents