---

Step * 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. (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)
⊢ (<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
{ (SplitOrHyps THEN Try (((EqHD (-1) THENA Auto) THEN All Reduce))) }

1
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)

2
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)

3
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)> = [J1] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = [J2] ∈ ℚInterval)
∨ (<qmax(I1;J1), qmin(I2;J2)> = <J1, J2> ∈ ℚInterval)

---

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,  I2>  =  <J1,  J2>)  \mvee{}  (I2  =  J1)  \mvee{}  (J2  =  I1)
\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:
(SplitOrHyps  THEN  Try  (((EqHD  (-1)  THENA  Auto)  THEN  All  Reduce)))

---

Home Index