Commit 2023-01-17 08:59 474c7b85

View on Github →

feat: port Order.Grade (#1594) Some of the docs seem dodgy, even Lean3 wise. I left them as-is for now awaiting further input. I got some weird breakage with OrderDual that I don't know how to fix; judicious @ didn't seem to help. Also, some nice variable features seem to not be working in Lean4; they were very useful for organisation.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Grade.lean

added def GradeBoundedOrder.liftLeft

added def GradeBoundedOrder.liftRight

added def GradeMaxOrder.liftLeft

added def GradeMaxOrder.liftRight

added def GradeMinOrder.finToNat

added def GradeMinOrder.liftLeft

added def GradeMinOrder.liftRight

added def GradeOrder.finToNat

added def GradeOrder.liftLeft

added def GradeOrder.liftRight

added theorem covby_iff_lt_covby_grade

added def grade

added theorem grade_bot

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 theorem grade_mono

added theorem grade_ne_grade_iff

added theorem grade_ofDual

added theorem grade_self

added theorem grade_strict_mono

added theorem grade_toDual

added theorem grade_top

added theorem isMax_grade_iff

added theorem isMin_grade_iff