mathlib3
fe664106 - feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927)

Commit

3 years ago

feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927) This proves the remark made in the definition of `acc`.

Author

vihdzp

Parents

4b788397

mathlib3 fe664106 - feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927)

mathlib3
fe664106 - feat(order/order_iso_nat): value is accessible iff it's not contained in an infinite decreasing sequence (#15927)