Commit 2026-06-09 16:55 8b8a27ce

View on Github →

chore(Order/SupClosed): use to_dual (#36219)

Estimated changes

deleted theorem InfClosed.biInf_mem
deleted theorem InfClosed.iInf_mem
deleted theorem InfClosed.sInf_mem
deleted theorem finsetInf'_mem_infClosure
deleted theorem infClosed_infClosure
deleted theorem infClosed_preimage_ofDual
deleted theorem infClosed_preimage_toDual
deleted def infClosure
deleted theorem infClosure_empty
deleted theorem infClosure_eq_self
deleted theorem infClosure_idem
deleted theorem infClosure_min
deleted theorem infClosure_mono
deleted theorem infClosure_prod
deleted theorem infClosure_singleton
deleted theorem infClosure_supClosure
deleted theorem infClosure_univ
deleted theorem inf_mem_infClosure
deleted theorem isGLB_infClosure
modified theorem isLUB_supClosure
deleted theorem lowerBounds_infClosure
deleted theorem subset_infClosure
modified theorem subset_supClosure
modified theorem supClosed_preimage_ofDual
modified theorem supClosed_preimage_toDual
modified theorem supClosed_supClosure
modified theorem supClosure_empty
modified theorem supClosure_eq_self
modified theorem supClosure_infClosure
modified theorem supClosure_prod
modified theorem supClosure_singleton
modified theorem supClosure_univ
modified theorem upperBounds_supClosure