Theorem orderIsoShrink_apply

Modification history

2026-02-06 11:03

Mathlib/Order/Shrink.lean

feat: `equivShrink α x ≤ equivShrink α y ↔ x ≤ y` (#34401) …

Modified orderIsoShrink_apply View on Github →

2025-02-07 15:17

Mathlib/Order/Shrink.lean

feat(Order): instances on Shrink (#21429) …

Added orderIsoShrink_apply View on Github →