mathlib3

ca795135 - feat(order/bounded): Proved many lemmas about bounded and unbounded sets (#11179)

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.