Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-25 03:33 8cc2ff4c

View on Github →

refactor(order/{bounded, rel_classes}): Moved bounded into the set namespace (#11594) As per the Zulip discussion. Closes #11589.

Estimated changes

deleted theorem bounded.mono
deleted theorem bounded.rel_mono
deleted theorem bounded_ge_Icc
deleted theorem bounded_ge_Ici
deleted theorem bounded_ge_Ico
deleted theorem bounded_ge_Ioc
deleted theorem bounded_ge_Ioi
deleted theorem bounded_ge_Ioo
deleted theorem bounded_ge_iff_bounded_gt
deleted theorem bounded_ge_inter_ge
deleted theorem bounded_ge_inter_gt
deleted theorem bounded_ge_inter_not_ge
deleted theorem bounded_ge_of_bounded_gt
deleted theorem bounded_gt_Icc
deleted theorem bounded_gt_Ici
deleted theorem bounded_gt_Ico
deleted theorem bounded_gt_Ioc
deleted theorem bounded_gt_Ioi
deleted theorem bounded_gt_Ioo
deleted theorem bounded_gt_inter_ge
deleted theorem bounded_gt_inter_gt
deleted theorem bounded_gt_inter_not_gt
deleted theorem bounded_inter_not
deleted theorem bounded_le_Icc
deleted theorem bounded_le_Ico
deleted theorem bounded_le_Iic
deleted theorem bounded_le_Iio
deleted theorem bounded_le_Ioc
deleted theorem bounded_le_Ioo
deleted theorem bounded_le_iff_bounded_lt
deleted theorem bounded_le_inter_le
deleted theorem bounded_le_inter_lt
deleted theorem bounded_le_inter_not_le
deleted theorem bounded_le_of_bounded_lt
deleted theorem bounded_lt_Icc
deleted theorem bounded_lt_Ico
deleted theorem bounded_lt_Iic
deleted theorem bounded_lt_Iio
deleted theorem bounded_lt_Ioc
deleted theorem bounded_lt_Ioo
deleted theorem bounded_lt_inter_le
deleted theorem bounded_lt_inter_lt
deleted theorem bounded_lt_inter_not_lt
deleted theorem bounded_self
added theorem set.bounded.mono
added theorem set.bounded.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_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_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_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_self
added theorem set.unbounded.mono
added theorem set.unbounded.rel_mono
added theorem set.unbounded_ge_iff
added theorem set.unbounded_gt_iff
added theorem set.unbounded_inter_ge
added theorem set.unbounded_le_Ici
added theorem set.unbounded_le_Ioi
added theorem set.unbounded_le_iff
added theorem set.unbounded_lt_Ici
added theorem set.unbounded_lt_Ioi
added theorem set.unbounded_lt_iff
deleted theorem unbounded.mono
deleted theorem unbounded.rel_mono
deleted theorem unbounded_ge_iff
deleted theorem unbounded_ge_inter_gt
deleted theorem unbounded_ge_inter_not_ge
deleted theorem unbounded_gt_iff
deleted theorem unbounded_gt_inter_gt
deleted theorem unbounded_gt_inter_not_gt
deleted theorem unbounded_inter_ge
deleted theorem unbounded_inter_not
deleted theorem unbounded_le_Ici
deleted theorem unbounded_le_Ioi
deleted theorem unbounded_le_iff
deleted theorem unbounded_le_inter_le
deleted theorem unbounded_le_inter_lt
deleted theorem unbounded_le_inter_not_le
deleted theorem unbounded_lt_Ici
deleted theorem unbounded_lt_Ioi
deleted theorem unbounded_lt_iff
deleted theorem unbounded_lt_inter_le
deleted theorem unbounded_lt_inter_lt
deleted theorem unbounded_lt_inter_not_lt
deleted def bounded
deleted theorem not_bounded_iff
deleted theorem not_unbounded_iff
added def set.bounded
added theorem set.not_bounded_iff
added theorem set.not_unbounded_iff
added def set.unbounded
deleted def unbounded