Commit 2025-02-07 15:17 bd47360e

View on Github →

feat(Order): instances on Shrink (#21429) If α : Type v is u-small, we transport various order related instances on α to Shrink.{u} α.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Shrink.lean

added theorem equivShrink_bot

added theorem equivShrink_symm_bot

added theorem equivShrink_symm_top

added theorem equivShrink_top

added theorem orderIsoShrink_apply

added theorem orderIsoShrink_symm_apply