Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-24 19:29 51526aef

View on Github →

chore(topology): rename mem_nhds_sets and mem_of_nhds and mem_nhds_sets_iff (#7690) Rename mem_nhds_sets to is_open.mem_nhds, and mem_nhds_sets_iff to mem_nhds_iff, and mem_of_nhds to mem_of_mem_nhds.

Estimated changes

added theorem is_open.mem_nhds
added theorem mem_nhds_iff
deleted theorem mem_nhds_sets
deleted theorem mem_nhds_sets_iff
added theorem mem_of_mem_nhds
deleted theorem mem_of_nhds