Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-26 10:41
6c84e8f7
View on Github →
chore: split Order.Defs (
#19498
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Group/Commute/Defs.lean
Modified
Mathlib/Algebra/Group/Semiconj/Defs.lean
Modified
Mathlib/Algebra/NeZero.lean
Modified
Mathlib/Data/Bool/Basic.lean
Modified
Mathlib/Data/Char.lean
Modified
Mathlib/Data/Int/Order/Basic.lean
Modified
Mathlib/Data/Ordering/Lemmas.lean
Modified
Mathlib/Deprecated/AlgebraClasses.lean
Modified
Mathlib/Deprecated/Order.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/Logic/Function/Basic.lean
Modified
Mathlib/Logic/Nontrivial/Basic.lean
Modified
Mathlib/Order/Basic.lean
Deleted
Mathlib/Order/Defs.lean
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
def
decidableEqOfDecidableLE
deleted
def
decidableLTOfDecidableLE
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
Created
Mathlib/Order/Defs/LinearOrder.lean
added
theorem
cmp_eq_compare
added
theorem
cmp_eq_compareOfLessAndEq
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
Created
Mathlib/Order/Defs/PartialOrder.lean
added
theorem
Decidable.eq_or_lt_of_le
added
theorem
Decidable.le_iff_lt_or_eq
added
theorem
Decidable.lt_or_eq_of_le
added
def
decidableEqOfDecidableLE
added
def
decidableLTOfDecidableLE
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
Created
Mathlib/Order/Defs/Unbundled.lean
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
Modified
Mathlib/Order/Interval/Set/Defs.lean
Modified
Mathlib/Tactic/GCongr/Core.lean
Modified
Mathlib/Tactic/PushNeg.lean
Modified
MathlibTest/push_neg.lean
Modified
scripts/noshake.json