mathlib3
33c6eeae - chore(topology/separation): rename `separated` to `separated_nhds` (#16604)

Commit

3 years ago

chore(topology/separation): rename `separated` to `separated_nhds` (#16604) E.g., Wikipedia uses "separated" for `disjoint (closure s) t ∧ disjoint s (closure t)`.

Author

urkud

Parents

dc1ac244

mathlib3 33c6eeae - chore(topology/separation): rename `separated` to `separated_nhds` (#16604)

mathlib3
33c6eeae - chore(topology/separation): rename `separated` to `separated_nhds` (#16604)