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

modified theorem set.nonempty_Iio
modified theorem set.nonempty_Ioi
deleted theorem sum.no_bot_order_iff
added theorem sum.no_max_order_iff
added theorem sum.no_min_order_iff
deleted theorem sum.no_top_order_iff
modified theorem measure_theory.ae_cover_Ico
modified theorem measure_theory.ae_cover_Iio
modified theorem measure_theory.ae_cover_Ioc
modified theorem measure_theory.ae_cover_Ioi
modified theorem measure_theory.ae_cover_Ioo
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 is_glb.nonempty
modified theorem is_lub.nonempty
modified theorem not_bdd_above_univ
modified theorem not_bdd_below_univ
modified theorem cInf_Ioi
modified theorem cSup_Iio
modified theorem filter.Iio_mem_at_bot
modified theorem filter.Ioi_mem_at_top
modified theorem filter.at_top_basis_Ioi
modified theorem filter.eventually_gt_at_top
modified theorem filter.eventually_lt_at_bot
modified theorem filter.frequently_at_bot'
modified theorem filter.frequently_at_top'
modified theorem filter.high_scores
modified theorem filter.low_scores
modified theorem filter.map_coe_Iio_at_bot
modified theorem filter.map_coe_Ioi_at_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
modified theorem metric.tendsto_at_top'