Commit 2026-02-05 04:02 4e498b83

View on Github →

feat(to_dual): use the new to_dual_cast framework (#34042) This PR uses the new to_dual_cast features introduced in #32438 in various places.

Estimated changes

deleted theorem WCovBy.of_le_of_le'
deleted theorem GaloisConnection.l_bot
deleted theorem GaloisConnection.l_eq
deleted theorem GaloisConnection.l_eq_bot
deleted theorem GaloisConnection.l_u_bot
deleted theorem GaloisConnection.l_u_le
deleted theorem GaloisConnection.l_unique
deleted theorem GaloisConnection.le_u
modified theorem Set.Icc_def
modified theorem Set.Ico_def
modified theorem Set.Ioc_def
modified theorem Set.Ioo_def
modified theorem Set.mem_Icc
modified theorem Set.mem_Ico
modified theorem Set.mem_Iic
modified theorem Set.mem_Iio
modified theorem Set.mem_Ioc
modified theorem Set.mem_Ioo