---

Step * of Lemma rat-interval-face-dimension

∀J:ℚInterval. ((↑Inhabited(J)) ⇒ (∀I:ℚInterval. (I ≤ J ⇒ ((I = J ∈ ℚInterval) ∨ (dim(I) = (dim(J) - 1) ∈ ℤ)))))
BY
{ ((D 0 THENA Auto)
   THEN D -1
   THEN RepUR ``rat-interval-face inhabited-rat-interval`` 0
   THEN Decide ⌜J1 = J2 ∈ ℚ⌝⋅
   THEN Auto) }

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

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

---

Latex:

---

Latex:
\mforall{}J:\mBbbQ{}Interval.  ((\muparrow{}Inhabited(J))  {}\mRightarrow{}  (\mforall{}I:\mBbbQ{}Interval.  (I  \mleq{}  J  {}\mRightarrow{}  ((I  =  J)  \mvee{}  (dim(I)  =  (dim(J)  -  1))))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  -1
  THEN  RepUR  ``rat-interval-face  inhabited-rat-interval``  0
  THEN  Decide  \mkleeneopen{}J1  =  J2\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index