Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_nhds.comm

Modification history

2022-09-27 17:24
src/topology/separation.lean
chore(topology/separation): rename `separated` to `separated_nhds` (#16604) …
Added separated_nhds.commView on Github →