Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-28 18:57 18dce134

View on Github →

feat(data/finset/interval): Bounded intervals in locally finite orders are finite (#9960) A set which is bounded above and below is finite. A set which is bounded below in an order_top is finite. A set which is bounded above in an order_bot is finite. Also provide the order_dual constructions for bdd_stuff and locally_finite_order.

Estimated changes

added theorem bdd_above.finite
added theorem bdd_below.finite
added theorem bdd_above.dual
added theorem bdd_below.dual
added theorem is_glb.dual
modified theorem is_glb.lower_bounds_eq
modified theorem is_glb.nonempty
modified theorem is_glb_lt_iff
added theorem is_greatest.dual
added theorem is_least.dual
added theorem is_lub.dual
modified theorem lt_is_glb_iff
added theorem Icc_to_dual
added theorem Ico_to_dual
added theorem Ioc_to_dual
added theorem Ioo_to_dual