Commit 2024-12-23 08:37 38b244b7

View on Github →

chore(*): rename lemmas about 𝓝[≥] a etc (#20188) See Zulip poll Also slightly golf some proofs that were broken by the renames and drop unneeded typeclass assumptions in lemmas Set.OrdConnected.mem_nhds*.

Estimated changes

deleted theorem tendsto_norm_one'
deleted theorem Ordinal.nhdsBasis_Ioc
added theorem Ordinal.nhdsLE_eq_nhds
deleted theorem Ordinal.nhds_left_eq_nhds
deleted theorem Ordinal.nhds_right'
added theorem tendsto_inv_nhdsGE
added theorem tendsto_inv_nhdsGE_inv
added theorem tendsto_inv_nhdsGT
added theorem tendsto_inv_nhdsGT_inv
added theorem tendsto_inv_nhdsLE
added theorem tendsto_inv_nhdsLE_inv
added theorem tendsto_inv_nhdsLT
added theorem tendsto_inv_nhdsLT_inv
added theorem inv_nhdsGT_zero
deleted theorem inv_nhdsWithin_Ioi_zero
deleted theorem tendsto_inv_atTop_zero'
deleted theorem tendsto_inv_zero_atTop
added theorem ENNReal.nhdsLT_neBot
added theorem nhdsGE_basis
added theorem nhdsLE_basis
deleted theorem nhdsWithin_Ici_basis'
deleted theorem nhdsWithin_Ici_basis
deleted theorem nhdsWithin_Ici_eq''
deleted theorem nhdsWithin_Ici_eq'
deleted theorem nhdsWithin_Iic_basis'
deleted theorem nhdsWithin_Iic_basis
deleted theorem nhdsWithin_Iic_eq''
deleted theorem nhdsWithin_Iic_eq'
added theorem comap_coe_Iio_nhdsLT
added theorem comap_coe_Ioi_nhdsGT
added theorem comap_coe_Ioo_nhdsGT
added theorem comap_coe_Ioo_nhdsLT
added theorem nhdsGT_le_nhdsNE
added theorem nhdsLE_sup_nhdsGE
added theorem nhdsLE_sup_nhdsGT
added theorem nhdsLT_le_nhdsNE
added theorem nhdsLT_sup_nhdsGE
added theorem nhdsLT_sup_nhdsGT
deleted theorem nhds_left'_le_nhds_ne
deleted theorem nhds_left'_sup_nhds_right
deleted theorem nhds_left_sup_nhds_right'
deleted theorem nhds_left_sup_nhds_right
deleted theorem nhds_right'_le_nhds_ne
added theorem TFAE_mem_nhdsGE
added theorem TFAE_mem_nhdsGT
added theorem TFAE_mem_nhdsLE
added theorem TFAE_mem_nhdsLT
deleted theorem TFAE_mem_nhdsWithin_Ici
deleted theorem TFAE_mem_nhdsWithin_Iic
deleted theorem TFAE_mem_nhdsWithin_Iio
deleted theorem TFAE_mem_nhdsWithin_Ioi
added theorem nhdsGE_basis_Icc
added theorem nhdsGE_basis_Ico
added theorem nhdsGT_basis
added theorem nhdsGT_eq_bot_iff
added theorem nhdsLE_basis_Icc
added theorem nhdsLT_basis
added theorem nhdsLT_eq_bot_iff
deleted theorem nhdsWithin_Ici_basis_Icc
deleted theorem nhdsWithin_Ici_basis_Ico
deleted theorem nhdsWithin_Iic_basis_Icc
deleted theorem nhdsWithin_Iio_basis'
deleted theorem nhdsWithin_Iio_basis
deleted theorem nhdsWithin_Iio_eq_bot_iff
deleted theorem nhdsWithin_Ioi_basis'
deleted theorem nhdsWithin_Ioi_basis
deleted theorem nhdsWithin_Ioi_eq_bot_iff
added theorem Icc_mem_nhdsGE
added theorem Icc_mem_nhdsGE_of_mem
added theorem Icc_mem_nhdsGT
added theorem Icc_mem_nhdsGT_of_mem
added theorem Icc_mem_nhdsLE
added theorem Icc_mem_nhdsLE_of_mem
added theorem Icc_mem_nhdsLT
added theorem Icc_mem_nhdsLT_of_mem
deleted theorem Icc_mem_nhdsWithin_Ici'
deleted theorem Icc_mem_nhdsWithin_Ici
deleted theorem Icc_mem_nhdsWithin_Iic'
deleted theorem Icc_mem_nhdsWithin_Iic
deleted theorem Icc_mem_nhdsWithin_Iio'
deleted theorem Icc_mem_nhdsWithin_Iio
deleted theorem Icc_mem_nhdsWithin_Ioi'
deleted theorem Icc_mem_nhdsWithin_Ioi
added theorem Ico_mem_nhdsGE
added theorem Ico_mem_nhdsGE_of_mem
added theorem Ico_mem_nhdsGT
added theorem Ico_mem_nhdsGT_of_mem
added theorem Ico_mem_nhdsLE_of_mem
added theorem Ico_mem_nhdsLT
added theorem Ico_mem_nhdsLT_of_mem
deleted theorem Ico_mem_nhdsWithin_Ici'
deleted theorem Ico_mem_nhdsWithin_Ici
deleted theorem Ico_mem_nhdsWithin_Iic
deleted theorem Ico_mem_nhdsWithin_Iio'
deleted theorem Ico_mem_nhdsWithin_Iio
deleted theorem Ico_mem_nhdsWithin_Ioi'
deleted theorem Ico_mem_nhdsWithin_Ioi
added theorem Ioc_mem_nhdsGE_of_mem
added theorem Ioc_mem_nhdsGT
added theorem Ioc_mem_nhdsGT_of_mem
added theorem Ioc_mem_nhdsLE
added theorem Ioc_mem_nhdsLE_of_mem
added theorem Ioc_mem_nhdsLT
added theorem Ioc_mem_nhdsLT_of_mem
deleted theorem Ioc_mem_nhdsWithin_Ici
deleted theorem Ioc_mem_nhdsWithin_Iic'
deleted theorem Ioc_mem_nhdsWithin_Iic
deleted theorem Ioc_mem_nhdsWithin_Iio'
deleted theorem Ioc_mem_nhdsWithin_Iio
deleted theorem Ioc_mem_nhdsWithin_Ioi'
deleted theorem Ioc_mem_nhdsWithin_Ioi
added theorem Ioo_mem_nhdsGE_of_mem
added theorem Ioo_mem_nhdsGT
added theorem Ioo_mem_nhdsGT_of_mem
added theorem Ioo_mem_nhdsLE_of_mem
added theorem Ioo_mem_nhdsLT
added theorem Ioo_mem_nhdsLT_of_mem
deleted theorem Ioo_mem_nhdsWithin_Ici
deleted theorem Ioo_mem_nhdsWithin_Iic
deleted theorem Ioo_mem_nhdsWithin_Iio'
deleted theorem Ioo_mem_nhdsWithin_Iio
deleted theorem Ioo_mem_nhdsWithin_Ioi'
deleted theorem Ioo_mem_nhdsWithin_Ioi