Interval inclusions in a linear order #
Over a dense order, a nonempty open interval lies inside a closed interval exactly when its
endpoints do, the missing sibling of Set.Ioo_subset_Ioo_iff and Set.Icc_subset_Ioo_iff. And
in any linear order a ray closed above is never inside a ray open below. Both are [UPSTREAM]
additions to Mathlib.Order.Interval.Set.LinearOrder.
A ray closed above is never inside a ray open below: min a b lies in the first and not in
the second.
theorem
Set.Ioo_subset_Icc_iff
{α : Type u_1}
[LinearOrder α]
[DenselyOrdered α]
{a₁ a₂ b₁ b₂ : α}
(h₁ : a₁ < b₁)
:
Ioo a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂