Commit 2022-04-21 23:36 e728cfd4

View on Github →

feat(order/grade): Graded orders (#11308) Define graded orders. To be the most general, we use is_min/is_max rather than order_bot/order_top. A grade is a function that respects the covering relation and eventually minimality/maximality.

Estimated changes

Modified docs/references.bib

Modified src/data/fin/basic.lean

added theorem fin.coe_strict_mono

Modified src/data/int/basic.lean

added theorem int.coe_nat_strict_mono

Modified src/data/int/succ_pred.lean

added theorem nat.cast_int_covby_iff

Modified src/data/nat/succ_pred.lean

added theorem fin.coe_covby_iff

Created src/order/grade.lean

added theorem covby_iff_lt_covby_grade

added def grade

added theorem grade_bot

added def grade_bounded_order.lift_left

added def grade_bounded_order.lift_right

added theorem grade_covby_grade_iff

added theorem grade_eq_grade_iff

added theorem grade_injective

added theorem grade_le_grade_iff

added theorem grade_lt_grade_iff

added def grade_max_order.lift_left

added def grade_max_order.lift_right

added def grade_min_order.fin_to_nat

added def grade_min_order.lift_left

added def grade_min_order.lift_right

added theorem grade_mono

added theorem grade_ne_grade_iff

added theorem grade_of_dual

added def grade_order.fin_to_nat

added def grade_order.lift_left

added def grade_order.lift_right

added theorem grade_self

added theorem grade_strict_mono

added theorem grade_to_dual

added theorem grade_top

added theorem is_max_grade_iff

added theorem is_min_grade_iff