Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_nhds_iff_disjoint

Modification history

2022-09-27 17:24

src/topology/separation.lean

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

Added separated_nhds_iff_disjoint View on Github →