Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-24 23:37 3e54e977

View on Github →

chore(topology/separation): prove that {y | y ≠ x} is open (#2506)

Estimated changes

Modified src/analysis/calculus/deriv.lean

Modified src/data/set/basic.lean

added theorem set.compl_singleton_eq

Modified src/topology/instances/ennreal.lean

modified theorem ennreal.is_open_ne_top

Modified src/topology/separation.lean

added theorem is_open_ne