Mathlib v3 is deprecated. Go to Mathlib v4

Def separated_nhds

Modification history

2022-09-27 17:24

src/topology/separation.lean

chore(topology/separation): rename `separated` to `separated_nhds` (#16604) …

Added separated_nhds View on Github →