---

Step * 2 1 of Lemma rat-interval-face-dimension

.....assertion..... 
1. J1 : ℚ
2. J2 : ℚ
3. ¬(J1 = J2 ∈ ℚ)
4. ↑q_le(J1;J2)
5. I : ℚInterval
6. (I = [J1] ∈ ℚInterval) ∨ (I = [J2] ∈ ℚInterval) ∨ (I = <J1, J2> ∈ ℚInterval)
⊢ dim(<J1, J2>) = 1 ∈ ℤ
BY
{ ((RW assert_pushdownC 4 THENA Auto) THEN (RWO "qle-iff" 4 THENM D 4) THEN Auto) }

1
1. J1 : ℚ
2. J2 : ℚ
3. ¬(J1 = J2 ∈ ℚ)
4. J1 < J2
5. I : ℚInterval
6. (I = [J1] ∈ ℚInterval) ∨ (I = [J2] ∈ ℚInterval) ∨ (I = <J1, J2> ∈ ℚInterval)
⊢ dim(<J1, J2>) = 1 ∈ ℤ

---

Latex:

---

Latex:
.....assertion..... 
1.  J1  :  \mBbbQ{}
2.  J2  :  \mBbbQ{}
3.  \mneg{}(J1  =  J2)
4.  \muparrow{}q\_le(J1;J2)
5.  I  :  \mBbbQ{}Interval
6.  (I  =  [J1])  \mvee{}  (I  =  [J2])  \mvee{}  (I  =  <J1,  J2>)
\mvdash{}  dim(<J1,  J2>)  =  1


By

---

Latex:
((RW  assert\_pushdownC  4  THENA  Auto)  THEN  (RWO  "qle-iff"  4  THENM  D  4)  THEN  Auto)

---

Home Index