Commit 2025-12-01 12:02 45cd8ef1

View on Github →

chore(Order/ULift): use @[to_dual] (#32088)

Estimated changes

Modified Mathlib/Order/ULift.lean

deleted theorem ULift.down_inf

modified theorem ULift.down_le

modified theorem ULift.down_lt

modified theorem ULift.down_sup

deleted theorem ULift.up_inf

modified theorem ULift.up_le

modified theorem ULift.up_lt

modified theorem ULift.up_sup