Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-21 10:54 ca795135

View on Github →

feat(order/bounded): Proved many lemmas about bounded and unbounded sets (#11179) These include more convenient characterizations of unboundedness in preorders and linear orders, and many results about bounded intervals and initial segments.

Estimated changes

added theorem bounded.mono
added theorem bounded.rel_mono
added theorem bounded_ge_Icc
added theorem bounded_ge_Ici
added theorem bounded_ge_Ico
added theorem bounded_ge_Ioc
added theorem bounded_ge_Ioi
added theorem bounded_ge_Ioo
added theorem bounded_ge_inter_ge
added theorem bounded_ge_inter_gt
added theorem bounded_gt_Icc
added theorem bounded_gt_Ici
added theorem bounded_gt_Ico
added theorem bounded_gt_Ioc
added theorem bounded_gt_Ioi
added theorem bounded_gt_Ioo
added theorem bounded_gt_inter_ge
added theorem bounded_gt_inter_gt
added theorem bounded_inter_not
added theorem bounded_le_Icc
added theorem bounded_le_Ico
added theorem bounded_le_Iic
added theorem bounded_le_Iio
added theorem bounded_le_Ioc
added theorem bounded_le_Ioo
added theorem bounded_le_inter_le
added theorem bounded_le_inter_lt
added theorem bounded_lt_Icc
added theorem bounded_lt_Ico
added theorem bounded_lt_Iic
added theorem bounded_lt_Iio
added theorem bounded_lt_Ioc
added theorem bounded_lt_Ioo
added theorem bounded_lt_inter_le
added theorem bounded_lt_inter_lt
added theorem bounded_self
added theorem unbounded.mono
added theorem unbounded.rel_mono
added theorem unbounded_ge_iff
added theorem unbounded_ge_inter_gt
added theorem unbounded_gt_iff
added theorem unbounded_gt_inter_gt
added theorem unbounded_inter_ge
added theorem unbounded_inter_not
added theorem unbounded_le_Ici
added theorem unbounded_le_Ioi
added theorem unbounded_le_iff
added theorem unbounded_le_inter_le
added theorem unbounded_le_inter_lt
added theorem unbounded_lt_Ici
added theorem unbounded_lt_Ioi
added theorem unbounded_lt_iff
added theorem unbounded_lt_inter_le
added theorem unbounded_lt_inter_lt
added theorem inf_lt_of_left_lt
added theorem inf_lt_of_right_lt
added theorem lt_sup_of_lt_left
added theorem lt_sup_of_lt_right
modified def bounded