Commit 2026-11-10 21:51 ccd6c847

View on Github →

chore(Order): remove unused hypothesis (#45693) Removes unused hypothesis from #45673 in Order.

Estimated changes

Modified Mathlib/Basic/ENNReal/Basic.lean

Modified Mathlib/Data/ENat/Lattice.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean

modified theorem ciSup_extend_le

Modified Mathlib/Order/ConditionallyCompleteLattice/WithTop.lean

modified theorem WithTop.coe_sInf

Modified Mathlib/Order/SuccPred/Basic.lean

modified theorem Order.succ_le_succ_iff_of_not_isMax

modified theorem Order.succ_lt_succ_iff_of_not_isMax