Commit 2024-08-23 10:19 b8518471

View on Github →

chore(Init/Order): Rework files (#15228) Merge Init.Order.Lemmas and the part of Init.Algebra.Classes about relations into Order.Defs.

Estimated changes

deleted theorem antisymm
deleted theorem asymm
deleted theorem asymm_of
deleted theorem irrefl
deleted theorem irrefl_of
deleted theorem not_lt_of_lt
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
deleted theorem eq_max
deleted theorem eq_min
deleted theorem le_max_left
deleted theorem le_max_right
deleted theorem le_min
deleted theorem lt_min
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 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
added theorem antisymm
added theorem asymm
added theorem asymm_of
added theorem eq_max
added theorem eq_min
added theorem irrefl
added theorem irrefl_of
added theorem le_max_left
added theorem le_max_right
added theorem le_min
added theorem lt_min
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 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 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