Commit 2026-03-21 16:01 a499e409

View on Github →

chore(Order/UpperLower/Principal): use to_dual (#36945) This PR uses to_dual on intervals like UpperSet.Ici. The prerequisite file Order.Interval.Set.OrderIso is also tagged with to_dual.

Estimated changes

deleted def OrderIso.IciBot
deleted theorem OrderIso.image_Ici
deleted theorem OrderIso.image_Ico
deleted theorem OrderIso.image_Ioi
deleted theorem OrderIso.preimage_Ici
deleted theorem OrderIso.preimage_Ioc
deleted theorem OrderIso.preimage_Ioi
deleted theorem LowerSet.Iic_iInf
deleted theorem LowerSet.Iic_iInf₂
deleted theorem LowerSet.Iic_inf
deleted theorem LowerSet.Iic_inj
deleted theorem LowerSet.Iic_le
deleted theorem LowerSet.Iic_ne_Iic
deleted theorem LowerSet.Iic_ne_bot
deleted theorem LowerSet.Iic_sInf
deleted theorem LowerSet.Iic_strictMono
deleted theorem LowerSet.Iio_eq_bot
deleted theorem LowerSet.Iio_strictMono
deleted theorem LowerSet.Ioi_le_Ici
deleted theorem LowerSet.bot_lt_Iic
deleted theorem LowerSet.coe_Iic
deleted theorem LowerSet.coe_Iio
deleted theorem LowerSet.map_Iic
deleted theorem LowerSet.map_Iio
deleted theorem LowerSet.mem_Iic_iff
deleted theorem LowerSet.mem_Iio_iff
added def UpperSet.Ici
modified theorem UpperSet.Ici_inj
added theorem UpperSet.Ici_injective
modified theorem UpperSet.Ici_lt_top
modified theorem UpperSet.Ici_ne_top
added def UpperSet.Ioi
modified theorem UpperSet.le_Ici