Commit 2026-02-06 11:03 b1b3d4a0

View on Github →

feat: equivShrink α x ≤ equivShrink α y ↔ x ≤ y (#34401) We also move theorems around for better variable management.

Estimated changes

Modified Mathlib/Order/Shrink.lean

modified theorem equivShrink_bot

added theorem equivShrink_le_equivShrink

added theorem equivShrink_lt_equivShrink

modified theorem equivShrink_symm_bot

modified theorem orderIsoShrink_apply

modified theorem orderIsoShrink_symm_apply