---

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


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)
⊢ (I = <J1, J2> ∈ ℚInterval) ∨ (dim(I) = (dim(<J1, J2>) - 1) ∈ ℤ)
BY
{ ((OrLeft THEN Auto)
   THEN SplitOrHyps
   THEN (RWO "-1" 0 THENA Auto)
   THEN RepUR ``rat-point-interval`` 0
   THEN EqCDA
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((OrLeft  THEN  Auto)
  THEN  SplitOrHyps
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  RepUR  ``rat-point-interval``  0
  THEN  EqCDA
  THEN  Auto)

---

Home Index