Order Isomorphisms between Finsets

This module provides some utilities for working with order isomorphisms between finite sets.

instance unique_finite_orderiso {α β : Type} [LinearOrder α] [LinearOrder β] [WellFoundedLT α] {a : Finset α} {b : Finset β} (equal_size : a.card = b.card) : Unique (↥a ≃o ↥b)

There is a unique order isomorphism between finsets of equal cardinality when the source type has a well-founded linear order.

Equations

• unique_finite_orderiso equal_size = { default := (a.orderIsoOfFin ⋯).symm.trans (b.orderIsoOfFin ⋯), uniq := ⋯ }

theorem equal_size_of_orderiso {α β : Type} [LinearOrder α] [LinearOrder β] {a : Finset α} {b : Finset β} (f : ↥a ≃o ↥b) : a.card = b.card

If there exists an order isomorphism between two finsets, they must have equal cardinality.