English
If two half-open intervals Ico(x1,x2) and Ico(y1,y2) are disjoint and x1 < x2, and x2 ∈ Ico(y1,y2), then y1 = x2.
Русский
Если два полупервообразующих интервала Ico(x1,x2) и Ico(y1,y2) непересекаются и x1 < x2, и x2 ∈ Ico(y1,y2), то y1 = x2.
LaTeX
$$$$ y_1 = x_2 $$ given the hypotheses$$
Lean4
/-- 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. -/
theorem eq_of_Ico_disjoint {x₁ x₂ y₁ y₂ : α} (h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)) (hx : x₁ < x₂)
(h2 : x₂ ∈ Ico y₁ y₂) : y₁ = x₂ :=
by
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h
apply le_antisymm h2.1
exact h.elim (fun h => absurd hx (not_lt_of_ge h)) id
