Commit 2025-11-08 03:04 fcc21383

View on Github →

chore(Order): deprecate Codisjoint.ne_bot_of_ne_top', OrderEmbedding.{w,}covBy_of_apply and OrderIso.map_{w,}covBy (#28486)

Estimated changes

Modified Mathlib/Order/Cover.lean

deleted theorem OrderEmbedding.covBy_of_apply

deleted theorem OrderEmbedding.wcovBy_of_apply

deleted theorem OrderIso.map_covBy

deleted theorem OrderIso.map_wcovBy

Modified Mathlib/Order/Disjoint.lean

modified theorem Codisjoint.ne_bot_of_ne_top'

Modified Mathlib/Order/SuccPred/Basic.lean