---

Step * 1 5 of Lemma compatible-rat-intervals-iff


1. I1 : ℚ
2. I2 : ℚ
3. J1 : ℚ
4. J2 : ℚ
5. I1 ≤ I2
6. J1 ≤ J2
7. qmax(I1;J1) ≤ qmin(I2;J2)
8. qmax(I1;J1) = I1 ∈ ℚ
9. qmin(I2;J2) = I1 ∈ ℚ
10. qmax(I1;J1) = J1 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)
BY
{ (Unfold `qmin` -3 THEN SplitOnHypITE -3  THEN Auto) }

---

Latex:

---

Latex:

1.  I1  :  \mBbbQ{}
2.  I2  :  \mBbbQ{}
3.  J1  :  \mBbbQ{}
4.  J2  :  \mBbbQ{}
5.  I1  \mleq{}  I2
6.  J1  \mleq{}  J2
7.  qmax(I1;J1)  \mleq{}  qmin(I2;J2)
8.  qmax(I1;J1)  =  I1
9.  qmin(I2;J2)  =  I1
10.  qmax(I1;J1)  =  J1
11.  qmin(I2;J2)  =  J2
\mvdash{}  (<I1,  I2>  =  <J1,  J2>)  \mvee{}  (I2  =  J1)  \mvee{}  (J2  =  I1)


By

---

Latex:
(Unfold  `qmin`  -3  THEN  SplitOnHypITE  -3    THEN  Auto)

---

Home Index