Commit 2026-07-17 22:50 121d7591

View on Github →

chore(Order/ConditionallyCompletePartialOrder/Indexed): use to_dual more to kill TODO (#41589) This PR uses to_dual to translate some theorems about ConditionallyCompletePartialOrder and kill TODO.

Estimated changes

Modified Mathlib/Order/ConditionallyCompletePartialOrder/Indexed.lean

deleted theorem GaloisConnection.u_ciInf_of_directed

deleted theorem GaloisConnection.u_ciInf_set_of_directedOn

deleted theorem GaloisConnection.u_csInf_of_directedOn'

deleted theorem GaloisConnection.u_csInf_of_directedOn

deleted theorem OrderIso.map_ciInf_of_directed

deleted theorem OrderIso.map_ciInf_set_of_directedOn

deleted theorem OrderIso.map_csInf_of_directedOn'

deleted theorem OrderIso.map_csInf_of_directedOn