Commit 2022-12-16 03:25 7fb6b434

View on Github →

feat: port Order.Bounded (#1042) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/Bounded.lean

added theorem Set.Bounded.mono

added theorem Set.Bounded.rel_mono

added theorem Set.Unbounded.mono

added theorem Set.Unbounded.rel_mono

added theorem Set.bounded_ge_Icc

added theorem Set.bounded_ge_Ici

added theorem Set.bounded_ge_Ico

added theorem Set.bounded_ge_Ioc

added theorem Set.bounded_ge_Ioi

added theorem Set.bounded_ge_Ioo

added theorem Set.bounded_ge_iff_bounded_gt

added theorem Set.bounded_ge_inter_ge

added theorem Set.bounded_ge_inter_gt

added theorem Set.bounded_ge_inter_not_ge

added theorem Set.bounded_ge_of_bounded_gt

added theorem Set.bounded_gt_Icc

added theorem Set.bounded_gt_Ici

added theorem Set.bounded_gt_Ico

added theorem Set.bounded_gt_Ioc

added theorem Set.bounded_gt_Ioi

added theorem Set.bounded_gt_Ioo

added theorem Set.bounded_gt_inter_ge

added theorem Set.bounded_gt_inter_gt

added theorem Set.bounded_gt_inter_not_gt

added theorem Set.bounded_inter_not

added theorem Set.bounded_le_Icc

added theorem Set.bounded_le_Ico

added theorem Set.bounded_le_Iic

added theorem Set.bounded_le_Iio

added theorem Set.bounded_le_Ioc

added theorem Set.bounded_le_Ioo

added theorem Set.bounded_le_iff_bounded_lt

added theorem Set.bounded_le_inter_le

added theorem Set.bounded_le_inter_lt

added theorem Set.bounded_le_inter_not_le

added theorem Set.bounded_le_of_bounded_lt

added theorem Set.bounded_lt_Icc

added theorem Set.bounded_lt_Ico

added theorem Set.bounded_lt_Iic

added theorem Set.bounded_lt_Iio

added theorem Set.bounded_lt_Ioc

added theorem Set.bounded_lt_Ioo

added theorem Set.bounded_lt_inter_le

added theorem Set.bounded_lt_inter_lt

added theorem Set.bounded_lt_inter_not_lt

added theorem Set.bounded_self

added theorem Set.unbounded_ge_iff

added theorem Set.unbounded_ge_iff_unbounded_inter_ge

added theorem Set.unbounded_ge_inter_gt

added theorem Set.unbounded_ge_inter_not_ge

added theorem Set.unbounded_ge_of_forall_exists_gt

added theorem Set.unbounded_ge_univ

added theorem Set.unbounded_gt_iff

added theorem Set.unbounded_gt_iff_unbounded_ge

added theorem Set.unbounded_gt_inter_gt

added theorem Set.unbounded_gt_inter_not_gt

added theorem Set.unbounded_gt_of_forall_exists_ge

added theorem Set.unbounded_gt_of_unbounded_ge

added theorem Set.unbounded_gt_univ

added theorem Set.unbounded_inter_ge

added theorem Set.unbounded_inter_not

added theorem Set.unbounded_le_Ici

added theorem Set.unbounded_le_Ioi

added theorem Set.unbounded_le_iff

added theorem Set.unbounded_le_inter_le

added theorem Set.unbounded_le_inter_lt

added theorem Set.unbounded_le_inter_not_le

added theorem Set.unbounded_le_of_forall_exists_lt

added theorem Set.unbounded_le_univ

added theorem Set.unbounded_lt_Ici

added theorem Set.unbounded_lt_Ioi

added theorem Set.unbounded_lt_iff

added theorem Set.unbounded_lt_iff_unbounded_le

added theorem Set.unbounded_lt_inter_le

added theorem Set.unbounded_lt_inter_lt

added theorem Set.unbounded_lt_inter_not_lt

added theorem Set.unbounded_lt_of_forall_exists_le

added theorem Set.unbounded_lt_of_unbounded_le

added theorem Set.unbounded_lt_univ