Projection onto a ray and the ray's endpoints

This file describes when Set.projIci a reaches the endpoints of the ray Set.Ici a, whose least element is a and whose greatest element is the ambient ⊤. A point goes to the least element exactly when it lies at or below a, and to the greatest exactly when a or the point is ⊤. The lemmas restate Set.projIci_eq_self, lt_max_iff and max_eq_top through the endpoints of the ray, and are [UPSTREAM] additions to Mathlib.Order.Interval.Set.ProjIcc.

theorem Set.projIci_eq_bot {α : Type u_1} [LinearOrder α] {a x : α} : projIci a x = ⊥ ↔ x ≤ a

theorem Set.bot_lt_projIci {α : Type u_1} [LinearOrder α] {a x : α} : ⊥ < projIci a x ↔ a < x

theorem Set.projIci_eq_top {α : Type u_1} [LinearOrder α] {a x : α} [OrderTop α] : projIci a x = ⊤ ↔ a = ⊤ ∨ x = ⊤