Commit 2021-01-02 00:36 c32efeae
View on Github →feat(data/fin): there is at most one order_iso from fin n to α (#5499)
- Define a
bounded_latticeinstance onfin (n + 1). - Prove that there is at most one
order_isofromfin ntoα.
feat(data/fin): there is at most one order_iso from fin n to α (#5499)
bounded_lattice instance on fin (n + 1).order_iso from fin n to α.