---

Step * 2 3 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. J2 = I1 ∈ ℚ
⊢ (<qmax(I1;J1), qmin(I2;J2)> = [I1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [I2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <I1, I2> ∈ ℚInterval)
BY
{ ((Eliminate ⌜J2⌝⋅ THENA Auto)
   THEN (Assert qmin(I2;I1) = I1 ∈ ℚ BY
               (Unfold `qmin` 0 THEN Auto))
   THEN (Eliminate ⌜qmin(I2;I1)⌝⋅ THENA Auto)
   THEN (Assert qmax(I1;J1) = I1 ∈ ℚ BY
               (Unfold `qmax` 0 THEN Auto))
   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.  J2  =  I1
\mvdash{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [I1])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [I2])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  <I1,  I2>)


By

---

Latex:
((Eliminate  \mkleeneopen{}J2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  qmin(I2;I1)  =  I1  BY
                          (Unfold  `qmin`  0  THEN  Auto))
  THEN  (Eliminate  \mkleeneopen{}qmin(I2;I1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  qmax(I1;J1)  =  I1  BY
                          (Unfold  `qmax`  0  THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index