Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separated_nhds.empty_right

Modification history

2022-09-27 17:24

src/topology/separation.lean

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

Added separated_nhds.empty_right View on Github →