Commit 2026-02-21 12:45 90f65323

View on Github →

chore(Order/UpperLower/Basic): use to_dual (#34640)

Estimated changes

deleted theorem Set.compl_Ici
deleted theorem Set.compl_Ioi
deleted theorem Set.notMem_Iic
deleted theorem Set.notMem_Iio
modified theorem OrderEmbedding.preimage_Ici
modified theorem OrderEmbedding.preimage_Ioi
deleted theorem IsLowerSet.Iio_subset
deleted theorem IsLowerSet.not_bddBelow
deleted theorem IsUpperSet.eq_univ_or_Ioi
deleted theorem OrderEmbedding.image_Iic
deleted theorem OrderEmbedding.image_Iio
deleted theorem isLowerSet_Iic
deleted theorem isLowerSet_Iio
deleted theorem isLowerSet_iff_Iic_subset
deleted theorem isLowerSet_iff_Iio_subset
modified theorem isUpperSet_Ici
modified theorem isUpperSet_Ioi
deleted theorem not_bddBelow_Iic
deleted theorem not_bddBelow_Iio