---

Step * 3 1 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. I1 = J1 ∈ ℚ
9. I2 = J2 ∈ ℚ
⊢ (<qmax(I1;J1), qmin(I2;J2)> = [J1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [J2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <J1, J2> ∈ ℚInterval)
BY
{ (RepeatFor 2 ((OrRight THENA Auto))
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN (RWO  "qmax-idempotent qmin-idempotent" 0 THENA 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.  I1  =  J1
9.  I2  =  J2
\mvdash{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [J1])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [J2])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  <J1,  J2>)


By

---

Latex:
(RepeatFor  2  ((OrRight  THENA  Auto))
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  (RWO    "qmax-idempotent  qmin-idempotent"  0  THENA  Auto))

---

Home Index