Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-21 15:23 5776f4c0

View on Github →

feat(topology): more lemmas about Ici and Iic neighborhoods (#3474) Main feature : add tfae_mem_nhds_within_Ici and tfae_mem_nhds_within_Iic, analogous to the existing tfae_mem_nhds_within_Ioi and tfae_mem_nhds_within_Iio, as well as related lemmas (again imitating the open case) I also added a few lemmas in data/set/intervals/basic.lean that were useful for this and a few upcoming PRs

Estimated changes

Modified src/data/set/intervals/basic.lean

added theorem set.Icc_subset_Ici_self

added theorem set.Icc_subset_Iic_self

added theorem set.Icc_subset_Ioo

added theorem set.Ioc_subset_Ioo_right

Modified src/topology/algebra/ordered.lean

added theorem Icc_mem_nhds_within_Ici

added theorem Icc_mem_nhds_within_Iic

added theorem Ico_mem_nhds_within_Ici

added theorem Ico_mem_nhds_within_Iic

added theorem Ioc_mem_nhds_within_Ici

added theorem Ioc_mem_nhds_within_Iic

added theorem Ioo_mem_nhds_within_Ici

added theorem Ioo_mem_nhds_within_Iic

added theorem mem_nhds_within_Ici_iff_exists_Icc_subset'

added theorem mem_nhds_within_Ici_iff_exists_mem_Ioc_Ico_subset

added theorem mem_nhds_within_Iic_iff_exists_Icc_subset'

added theorem mem_nhds_within_Iic_iff_exists_mem_Ico_Ioc_subset

added theorem nhds_within_Icc_eq_nhds_within_Ici

added theorem nhds_within_Icc_eq_nhds_within_Iic

added theorem nhds_within_Ici_ne_bot

added theorem nhds_within_Ici_self_ne_bot

added theorem nhds_within_Ico_eq_nhds_within_Ici

added theorem nhds_within_Iic_ne_bot

added theorem nhds_within_Iic_self_ne_bot

added theorem nhds_within_Ioc_eq_nhds_within_Iic

added theorem tfae_mem_nhds_within_Ici

added theorem tfae_mem_nhds_within_Iic