Commit 2026-06-03 10:30 48c7ceba

View on Github →

chore: use to_dual for SupClosed/InfClosed (#40175) This PR tags lemmas about SupClosed with the to_dual attribute.

Estimated changes

deleted theorem InfClosed.codirectedOn
deleted theorem InfClosed.finsetInf'_mem
deleted theorem InfClosed.finsetInf_mem
deleted theorem InfClosed.image
deleted theorem InfClosed.inter
deleted theorem InfClosed.preimage
deleted theorem InfClosed.prod
deleted def InfClosed
deleted theorem IsLowerSet.infClosed
deleted theorem infClosed_empty
deleted theorem infClosed_iInter
deleted theorem infClosed_pi
deleted theorem infClosed_range
deleted theorem infClosed_sInter
deleted theorem infClosed_singleton
deleted theorem infClosed_univ
modified theorem supClosed_empty
modified theorem supClosed_singleton
modified theorem supClosed_univ