Commit 2021-07-02 18:11 25e4f065

View on Github →

feat (Algebra): port init.algebra.order (#18)

  • feat (Algebra): port init.algebra.order
  • capitalise sections and classes
  • capitalise sections and classes pt 2 I don't think I commited everything properly first time round.
  • add missing import
  • change class fields capitalisation

Estimated changes

added theorem eq_or_lt_of_not_lt
added theorem ge_trans
added theorem gt_irrefl
added theorem gt_of_ge_of_gt
added theorem gt_of_gt_of_ge
added theorem gt_trans
added theorem le_antisymm
added theorem le_antisymm_iff
added theorem le_iff_lt_or_eq
added theorem le_imp_le_of_lt_imp_lt
added theorem le_not_le_of_lt
added theorem le_of_eq
added theorem le_of_eq_or_lt
added theorem le_of_lt
added theorem le_of_lt_or_eq
added theorem le_of_not_ge
added theorem le_of_not_gt
added theorem le_of_not_le
added theorem le_of_not_lt
added theorem le_or_gt
added theorem le_or_lt
added theorem le_refl
added theorem le_total
added theorem le_trans
added theorem lt_asymm
added def lt_by_cases
added theorem lt_iff_le_not_le
added theorem lt_iff_not_ge
added theorem lt_irrefl
added theorem lt_of_le_not_le
added theorem lt_of_le_of_lt
added theorem lt_of_le_of_ne
added theorem lt_of_lt_of_le
added theorem lt_of_not_ge
added theorem lt_or_eq_of_le
added theorem lt_or_ge
added theorem lt_or_gt_of_ne
added theorem lt_or_le
added theorem lt_trans
added theorem lt_trichotomy
added theorem ne_iff_lt_or_gt
added theorem ne_of_gt
added theorem ne_of_lt
added theorem not_le
added theorem not_le_of_gt
added theorem not_lt
added theorem not_lt_of_ge
added theorem not_lt_of_gt