---

Step * 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. (<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)
9. (<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)
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)
BY
{ (All (Unfold `rat-point-interval`) THEN SplitOrHyps THEN ∀h:hyp. (EqHD h 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. qmax(I1;J1) = I1 ∈ ℚ
9. qmin(I2;J2) = I1 ∈ ℚ
10. qmax(I1;J1) = J1 ∈ ℚ
11. qmin(I2;J2) = J1 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

2
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) = I2 ∈ ℚ
9. qmin(I2;J2) = I2 ∈ ℚ
10. qmax(I1;J1) = J1 ∈ ℚ
11. qmin(I2;J2) = J1 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

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

4
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) = J2 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

5
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 ∈ ℚ)

6
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) = I2 ∈ ℚ
9. qmin(I2;J2) = I2 ∈ ℚ
10. qmax(I1;J1) = J2 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

7
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) = I2 ∈ ℚ
10. qmax(I1;J1) = J2 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

8
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) = I2 ∈ ℚ
9. qmin(I2;J2) = I2 ∈ ℚ
10. qmax(I1;J1) = J1 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

9
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) = I2 ∈ ℚ
10. qmax(I1;J1) = J1 ∈ ℚ
11. qmin(I2;J2) = J2 ∈ ℚ
⊢ (<I1, I2> = <J1, J2> ∈ ℚInterval) ∨ (I2 = J1 ∈ ℚ) ∨ (J2 = I1 ∈ ℚ)

---

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),  qmin(I2;J2)>  =  [I1])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [I2])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  <I1,  I2>)
9.  (<qmax(I1;J1),  qmin(I2;J2)>  =  [J1])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  [J2])
\mvee{}  (<qmax(I1;J1),  qmin(I2;J2)>  =  <J1,  J2>)
\mvdash{}  (<I1,  I2>  =  <J1,  J2>)  \mvee{}  (I2  =  J1)  \mvee{}  (J2  =  I1)


By

---

Latex:
(All  (Unfold  `rat-point-interval`)
  THEN  SplitOrHyps
  THEN  \mforall{}h:hyp.  (EqHD  h  THENA  Auto) 
  THEN  All  Reduce)

---

Home Index