Commit 2024-11-26 10:41 6c84e8f7

View on Github →

chore: split Order.Defs (#19498)

Estimated changes

deleted def AntiSymmetric
deleted theorem Decidable.eq_or_lt_of_le
deleted theorem Decidable.le_iff_lt_or_eq
deleted theorem Decidable.lt_or_eq_of_le
deleted def EmptyRelation
deleted theorem Equivalence.reflexive
deleted theorem Equivalence.symmetric
deleted theorem Equivalence.transitive
deleted theorem InvImage.irreflexive
deleted theorem InvImage.trans
deleted def Irreflexive
deleted def IsLowerSet
deleted def IsUpperSet
deleted structure LowerSet
deleted theorem Maximal.le_of_ge
deleted theorem Maximal.prop
deleted def Maximal
deleted theorem Minimal.le_of_le
deleted theorem Minimal.prop
deleted def Minimal
deleted def Reflexive
deleted def Symmetric
deleted def Total
deleted def Transitive
deleted structure UpperSet
deleted theorem antisymm
deleted theorem asymm
deleted theorem asymm_of
deleted theorem cmp_eq_compare
deleted theorem cmp_eq_compareOfLessAndEq
deleted theorem compare_eq_iff_eq
deleted theorem compare_ge_iff_ge
deleted theorem compare_gt_iff_gt
deleted theorem compare_iff
deleted theorem compare_le_iff_le
deleted theorem compare_lt_iff_lt
deleted theorem eq_max
deleted theorem eq_min
deleted theorem eq_or_lt_of_not_lt
deleted theorem ge_trans
deleted theorem gt_irrefl
deleted theorem gt_of_ge_of_gt
deleted theorem gt_of_gt_of_ge
deleted theorem gt_trans
deleted theorem irrefl
deleted theorem irrefl_of
deleted theorem le_antisymm
deleted theorem le_antisymm_iff
deleted theorem le_iff_lt_or_eq
deleted theorem le_imp_le_of_lt_imp_lt
deleted theorem le_max_left
deleted theorem le_max_right
deleted theorem le_min
deleted theorem le_not_le_of_lt
deleted theorem le_of_eq
deleted theorem le_of_eq_or_lt
deleted theorem le_of_lt
deleted theorem le_of_lt_or_eq
deleted theorem le_of_not_ge
deleted theorem le_of_not_gt
deleted theorem le_of_not_le
deleted theorem le_of_not_lt
deleted theorem le_or_gt
deleted theorem le_or_lt
deleted theorem le_refl
deleted theorem le_rfl
deleted theorem le_total
deleted theorem le_trans
deleted def ltByCases
deleted theorem lt_asymm
deleted theorem lt_iff_le_not_le
deleted theorem lt_iff_not_ge
deleted theorem lt_irrefl
deleted theorem lt_min
deleted theorem lt_of_le_not_le
deleted theorem lt_of_le_of_lt
deleted theorem lt_of_le_of_ne
deleted theorem lt_of_lt_of_le
deleted theorem lt_of_not_ge
deleted theorem lt_or_eq_of_le
deleted theorem lt_or_ge
deleted theorem lt_or_gt_of_ne
deleted theorem lt_or_le
deleted theorem lt_trans
deleted theorem lt_trichotomy
deleted def maxDefault
deleted theorem max_assoc
deleted theorem max_comm
deleted theorem max_def
deleted theorem max_eq_left
deleted theorem max_eq_left_of_lt
deleted theorem max_eq_right
deleted theorem max_eq_right_of_lt
deleted theorem max_le
deleted theorem max_left_comm
deleted theorem max_lt
deleted theorem max_self
deleted def minDefault
deleted theorem min_assoc
deleted theorem min_comm
deleted theorem min_def
deleted theorem min_eq_left
deleted theorem min_eq_left_of_lt
deleted theorem min_eq_right
deleted theorem min_eq_right_of_lt
deleted theorem min_le_left
deleted theorem min_le_right
deleted theorem min_left_comm
deleted theorem min_self
deleted theorem ne_iff_lt_or_gt
deleted theorem ne_of_gt
deleted theorem ne_of_lt
deleted theorem not_le
deleted theorem not_le_of_gt
deleted theorem not_le_of_lt
deleted theorem not_lt
deleted theorem not_lt_of_ge
deleted theorem not_lt_of_le
deleted theorem refl
deleted theorem refl_of
deleted theorem symm
deleted theorem symm_of
deleted theorem total_of
deleted theorem trans
deleted theorem trans_of
deleted theorem trichotomous
deleted theorem trichotomous_of
added theorem cmp_eq_compare
added theorem compare_eq_iff_eq
added theorem compare_ge_iff_ge
added theorem compare_gt_iff_gt
added theorem compare_iff
added theorem compare_le_iff_le
added theorem compare_lt_iff_lt
added theorem eq_max
added theorem eq_min
added theorem eq_or_lt_of_not_lt
added theorem le_imp_le_of_lt_imp_lt
added theorem le_max_left
added theorem le_max_right
added theorem le_min
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_total
added def ltByCases
added theorem lt_iff_not_ge
added theorem lt_min
added theorem lt_of_not_ge
added theorem lt_or_ge
added theorem lt_or_gt_of_ne
added theorem lt_or_le
added theorem lt_trichotomy
added def maxDefault
added theorem max_assoc
added theorem max_comm
added theorem max_def
added theorem max_eq_left
added theorem max_eq_left_of_lt
added theorem max_eq_right
added theorem max_eq_right_of_lt
added theorem max_le
added theorem max_left_comm
added theorem max_lt
added theorem max_self
added def minDefault
added theorem min_assoc
added theorem min_comm
added theorem min_def
added theorem min_eq_left
added theorem min_eq_left_of_lt
added theorem min_eq_right
added theorem min_eq_right_of_lt
added theorem min_le_left
added theorem min_le_right
added theorem min_left_comm
added theorem min_self
added theorem ne_iff_lt_or_gt
added theorem not_le
added theorem 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_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_refl
added theorem le_rfl
added theorem le_trans
added theorem lt_asymm
added theorem lt_iff_le_not_le
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_or_eq_of_le
added theorem lt_trans
added theorem ne_of_gt
added theorem ne_of_lt
added theorem not_le_of_gt
added theorem not_le_of_lt
added theorem not_lt_of_ge
added theorem not_lt_of_le
added def AntiSymmetric
added def EmptyRelation
added theorem Equivalence.reflexive
added theorem Equivalence.symmetric
added theorem Equivalence.transitive
added theorem InvImage.irreflexive
added theorem InvImage.trans
added def Irreflexive
added def IsLowerSet
added def IsUpperSet
added structure LowerSet
added theorem Maximal.le_of_ge
added theorem Maximal.prop
added def Maximal
added theorem Minimal.le_of_le
added theorem Minimal.prop
added def Minimal
added def Reflexive
added def Symmetric
added def Total
added def Transitive
added structure UpperSet
added theorem antisymm
added theorem asymm
added theorem asymm_of
added theorem irrefl
added theorem irrefl_of
added theorem refl
added theorem refl_of
added theorem symm
added theorem symm_of
added theorem total_of
added theorem trans
added theorem trans_of
added theorem trichotomous
added theorem trichotomous_of