---

Step * 1 1 1 2 of Lemma face-of-half-cube


1. v6 : ℚ
2. v : ℚInterval
3. v5 : ℚ
4. ↑is-half-interval(v;[v6])
5. v = [v6] ∈ ℚInterval
⊢ ∃!I:ℚInterval. ((↑is-half-interval(I;<v5, v6>)) ∧ v ≤ I)
BY
{ ((D 0 With ⌜<qavg(v5;v6), v6>⌝  THEN Auto)
   THENL [(RepUR ``is-half-interval`` 0 THEN RW assert_pushdownC 0 THEN Auto)
         ; ((RWO "-2" 0 THENA Auto) THEN RepUR ``rat-interval-face`` 0 THEN Auto)
         ; ((RWO "5" (-1) THENA Auto) THEN DVar `y' THEN RepUR ``rat-interval-face`` -1)]
) }

1
1. v6 : ℚ
2. v : ℚInterval
3. v5 : ℚ
4. ↑is-half-interval(v;[v6])
5. v = [v6] ∈ ℚInterval
6. ↑is-half-interval(<qavg(v5;v6), v6>;<v5, v6>)
7. v ≤ <qavg(v5;v6), v6>
8. y1 : ℚ
9. y2 : ℚ
10. ↑is-half-interval(<y1, y2>;<v5, v6>)
11. ([v6] = [y1] ∈ ℚInterval) ∨ ([v6] = [y2] ∈ ℚInterval) ∨ ([v6] = <y1, y2> ∈ ℚInterval)
⊢ <y1, y2> = <qavg(v5;v6), v6> ∈ ℚInterval

---

Latex:

---

Latex:

1.  v6  :  \mBbbQ{}
2.  v  :  \mBbbQ{}Interval
3.  v5  :  \mBbbQ{}
4.  \muparrow{}is-half-interval(v;[v6])
5.  v  =  [v6]
\mvdash{}  \mexists{}!I:\mBbbQ{}Interval.  ((\muparrow{}is-half-interval(I;<v5,  v6>))  \mwedge{}  v  \mleq{}  I)


By

---

Latex:
((D  0  With  \mkleeneopen{}<qavg(v5;v6),  v6>\mkleeneclose{}    THEN  Auto)
  THENL  [(RepUR  ``is-half-interval``  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)
              ;  ((RWO  "-2"  0  THENA  Auto)  THEN  RepUR  ``rat-interval-face``  0  THEN  Auto)
              ;  ((RWO  "5"  (-1)  THENA  Auto)  THEN  DVar  `y'  THEN  RepUR  ``rat-interval-face``  -1)]
)

---

Home Index