Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-03 12:18 e104992d

View on Github →

chore(order/*): Replace total partial orders by linear orders (#13839) partial_order α + is_total α (≤) has no more theorems than linear_order α but is nonetheless used in some places. This replaces those uses by linear_order α or complete_linear_order α. Also make implicit one argument of finset.lt_inf'_iff and friends.

Estimated changes

modified theorem finset.exists_mem_eq_inf'
modified theorem finset.exists_mem_eq_inf
modified theorem finset.exists_mem_eq_sup'
modified theorem finset.exists_mem_eq_sup
modified theorem finset.inf'_le_iff
modified theorem finset.inf'_lt_iff
deleted theorem finset.inf_le_iff
deleted theorem finset.inf_lt_iff
deleted theorem finset.le_inf'_iff
modified theorem finset.le_sup'_iff
deleted theorem finset.le_sup_iff
modified theorem finset.lt_inf'_iff
deleted theorem finset.lt_inf_iff
modified theorem finset.lt_sup'_iff
deleted theorem finset.lt_sup_iff
modified theorem finset.sup'_lt_iff
deleted theorem finset.sup_lt_iff
modified theorem set.Icc_bot_top
modified theorem set.Ici_top
modified theorem set.Iic_bot
modified theorem set.Iio_inter_Iio
modified theorem set.Ioc_inter_Ioi
modified theorem set.Ioi_inter_Ioi
modified theorem antitone.map_inf
modified theorem antitone.map_sup
modified theorem inf_eq_min
modified theorem inf_ind
modified theorem inf_le_iff
added theorem inf_lt_iff
modified theorem le_sup_iff
modified theorem lt_inf_iff
modified theorem lt_sup_iff
modified theorem monotone.map_inf
modified theorem monotone.map_sup
modified theorem sup_eq_max
modified theorem sup_ind
modified theorem sup_lt_iff
modified theorem le_max_iff
modified theorem lt_max_iff
modified theorem lt_min_iff
modified theorem max_lt_iff
added theorem max_lt_max_left_iff
added theorem max_lt_max_right_iff
modified theorem min_le_iff
modified theorem min_lt_iff
added theorem min_lt_min_left_iff
added theorem min_lt_min_right_iff
modified theorem nhds_bot_basis
modified theorem nhds_bot_basis_Iic
modified theorem nhds_top_basis
modified theorem nhds_top_basis_Ici