Extra lemmas about intervals #
This file contains lemmas about intervals that cannot be included into data.set.intervals.basic
because this would create an import
cycle. Namely, lemmas in this file can use definitions
from data.set.lattice
, including disjoint
.
@[simp]
@[simp]
theorem
set.eq_of_Ico_disjoint
{α : Type u}
[linear_order α]
{x₁ x₂ y₁ y₂ : α}
(h : disjoint (set.Ico x₁ x₂) (set.Ico y₁ y₂))
(hx : x₁ < x₂)
(h2 : x₂ ∈ set.Ico y₁ y₂) :
y₁ = x₂
If two half-open intervals are disjoint and the endpoint of one lies in the other, then it must be equal to the endpoint of the other.