Commit 2025-02-03 07:17 600654aa
View on Github →feat(Order): Fin.succAboveOrderIso (#21303)
This PR introduces the order isomorphism Fin.succAboveOrderIso i : Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2)))
for i : Fin (n + 2)
.
feat(Order): Fin.succAboveOrderIso (#21303)
This PR introduces the order isomorphism Fin.succAboveOrderIso i : Fin (n + 1) ≃o ({i}ᶜ : Finset (Fin (n + 2)))
for i : Fin (n + 2)
.