Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-31 13:24 6b51787e

View on Github →

feat(order/conditionally_complete_lattice): add complete_linear_order instance for enat (#1633)

Estimated changes

Modified src/data/nat/enat.lean

added theorem enat.with_top_equiv_coe

added theorem enat.with_top_equiv_le

added theorem enat.with_top_equiv_lt

added theorem enat.with_top_equiv_symm_coe

added theorem enat.with_top_equiv_symm_le

added theorem enat.with_top_equiv_symm_lt

added theorem enat.with_top_equiv_symm_top

added theorem enat.with_top_equiv_symm_zero

added theorem enat.with_top_equiv_top

added theorem enat.with_top_equiv_zero

Modified src/order/conditionally_complete_lattice.lean