Theorem equivShrink_symm_bot

Modification history

2026-02-06 11:03
Mathlib/Order/Shrink.lean
feat: `equivShrink α x ≤ equivShrink α y ↔ x ≤ y` (#34401) …
Modified equivShrink_symm_botView on Github →
2025-02-07 15:17
Mathlib/Order/Shrink.lean
feat(Order): instances on Shrink (#21429) …
Added equivShrink_symm_botView on Github →