Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-30 13:18 e7075b84

View on Github →

chore(topology/algebra/ordered): fix assumptions in some lemmas (#3629)

Some nhds_within_I??_eq_nhds_within_I?? lemmas assumed strict inequalities when this was not needed.
Remove TFAEs that only stated equality of three nhds_withins. Prove equality of nhds_withins instead.
Genralize I??_mem_nhds_within_I?? to order_closed_topology.

Estimated changes

Modified src/topology/algebra/ordered.lean

modified theorem Icc_mem_nhds_within_Ici

modified theorem Icc_mem_nhds_within_Iic

modified theorem Icc_mem_nhds_within_Iio

modified theorem Ico_mem_nhds_within_Ici

modified theorem Ico_mem_nhds_within_Iic

modified theorem Ico_mem_nhds_within_Iio

modified theorem Ioc_mem_nhds_within_Iic

modified theorem Ioc_mem_nhds_within_Iio

modified theorem Ioo_mem_nhds_within_Iic

modified theorem Ioo_mem_nhds_within_Iio

modified theorem continuous_within_at_Icc_iff_Ici

modified theorem continuous_within_at_Icc_iff_Iic

modified theorem continuous_within_at_Ico_iff_Ici

modified theorem continuous_within_at_Ioc_iff_Iic

modified theorem continuous_within_at_Ioc_iff_Ioi

modified theorem continuous_within_at_Ioo_iff_Ioi

modified theorem nhds_within_Ico_eq_nhds_within_Ici

modified theorem nhds_within_Ioo_eq_nhds_within_Ioi

deleted theorem tfae_mem_nhds_within_Ici'

deleted theorem tfae_mem_nhds_within_Iic'

deleted theorem tfae_mem_nhds_within_Iio'

deleted theorem tfae_mem_nhds_within_Ioi'