Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 56d6a915

View on Github →

chore(order/basic): Rename no_bot_order/no_top_order to no_min_order/no_max_order (#11357) because that's really what they are. ∀ a, ∃ b, b < a precisely means that every a is not a minimal element. The correct statement for an order without bottom elements is ∀ a, ∃ b, ¬ a ≤ b, which is a weaker condition in general. Both conditions are equivalent over a linear order. Renames

  • no_bot_order -> no_min_order
  • no_top_order -> no_max_order
  • no_bot -> exists_lt
  • no_top -> exists_gt

Estimated changes

added theorem exists_gt
added theorem exists_lt
deleted theorem no_bot
deleted theorem no_top
modified theorem not_is_bot
modified theorem not_is_top
modified theorem pred_succ
modified theorem succ_pred
modified theorem closure_Iio
modified theorem closure_Ioi
modified theorem dense.exists_ge
modified theorem dense.exists_gt
modified theorem dense.exists_le
modified theorem dense.exists_lt
modified theorem disjoint_nhds_at_bot
modified theorem disjoint_nhds_at_top
modified theorem filter.eventually.exists_gt
modified theorem filter.eventually.exists_lt
modified theorem frontier_Icc
modified theorem frontier_Ici
modified theorem frontier_Ico
modified theorem frontier_Iic
modified theorem frontier_Iio
modified theorem frontier_Ioc
modified theorem frontier_Ioi
modified theorem inf_nhds_at_bot
modified theorem inf_nhds_at_top
modified theorem interior_Icc
modified theorem interior_Ici
modified theorem interior_Ico
modified theorem interior_Iic
modified theorem interior_Ioc
modified theorem nhds_basis_Ioo
modified theorem nhds_basis_Ioo_pos
modified theorem nhds_basis_Ioo_pos_of_pos
modified theorem nhds_basis_abs_sub_lt
modified theorem nhds_basis_zero_abs_sub_lt
modified theorem nhds_within_Iio_ne_bot
modified theorem nhds_within_Iio_self_ne_bot
modified theorem nhds_within_Ioi_ne_bot
modified theorem nhds_within_Ioi_self_ne_bot