---

Step * 3 2 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. I2 = J1 ∈ ℚ
⊢ (<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
{ ((Eliminate ⌜I2⌝⋅ THENA Auto)
   THEN (Assert qmin(J1;J2) = J1 ∈ ℚ BY
               (Unfold `qmin` 0 THEN Auto))
   THEN (Eliminate ⌜qmin(J1;J2)⌝⋅ THENA Auto)
   THEN (Assert qmax(I1;J1) = J1 ∈ ℚ BY
               (Unfold `qmax` 0 THEN AutoSplit))
   THEN RWO "-1" 0
   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.  I2  =  J1
\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:
((Eliminate  \mkleeneopen{}I2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  qmin(J1;J2)  =  J1  BY
                          (Unfold  `qmin`  0  THEN  Auto))
  THEN  (Eliminate  \mkleeneopen{}qmin(J1;J2)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  qmax(I1;J1)  =  J1  BY
                          (Unfold  `qmax`  0  THEN  AutoSplit))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index