---

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


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. ∀i:ℕk. b i ≤ c i
6. ∀i:ℕk. (↑is-half-interval(a i;b i))
7. ∀i:ℕk
     ∃I:ℚInterval
      (((↑is-half-interval(I;c i)) ∧ a i ≤ I)
      ∧ (∀y:ℚInterval. (((↑is-half-interval(y;c i)) ∧ a i ≤ y) ⇒ (y = I ∈ ℚInterval))))
8. d : ℚCube(k)
9. ∀i:ℕk
     (((↑is-half-interval(d i;c i)) ∧ a i ≤ d i)
     ∧ (∀y:ℚInterval. (((↑is-half-interval(y;c i)) ∧ a i ≤ y) ⇒ (y = (d i) ∈ ℚInterval))))
10. ↑is-half-cube(k;d;c)
11. ∀i:ℕk. a i ≤ d i
12. y : ℚCube(k)
13. ↑is-half-cube(k;y;c)
14. ∀i:ℕk. a i ≤ y i
15. x : ℕk
⊢ (y x) = (d x) ∈ ℚInterval
BY
{ ((D -7 With ⌜x⌝  THENA Auto) THEN (D -1 THEN BHyp -1) THEN Auto THEN All (RWO "assert-is-half-cube") THEN Auto) }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  \mforall{}i:\mBbbN{}k.  b  i  \mleq{}  c  i
6.  \mforall{}i:\mBbbN{}k.  (\muparrow{}is-half-interval(a  i;b  i))
7.  \mforall{}i:\mBbbN{}k
          \mexists{}I:\mBbbQ{}Interval
            (((\muparrow{}is-half-interval(I;c  i))  \mwedge{}  a  i  \mleq{}  I)
            \mwedge{}  (\mforall{}y:\mBbbQ{}Interval.  (((\muparrow{}is-half-interval(y;c  i))  \mwedge{}  a  i  \mleq{}  y)  {}\mRightarrow{}  (y  =  I))))
8.  d  :  \mBbbQ{}Cube(k)
9.  \mforall{}i:\mBbbN{}k
          (((\muparrow{}is-half-interval(d  i;c  i))  \mwedge{}  a  i  \mleq{}  d  i)
          \mwedge{}  (\mforall{}y:\mBbbQ{}Interval.  (((\muparrow{}is-half-interval(y;c  i))  \mwedge{}  a  i  \mleq{}  y)  {}\mRightarrow{}  (y  =  (d  i)))))
10.  \muparrow{}is-half-cube(k;d;c)
11.  \mforall{}i:\mBbbN{}k.  a  i  \mleq{}  d  i
12.  y  :  \mBbbQ{}Cube(k)
13.  \muparrow{}is-half-cube(k;y;c)
14.  \mforall{}i:\mBbbN{}k.  a  i  \mleq{}  y  i
15.  x  :  \mBbbN{}k
\mvdash{}  (y  x)  =  (d  x)


By

---

Latex:
((D  -7  With  \mkleeneopen{}x\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THEN  BHyp  -1)
  THEN  Auto
  THEN  All  (RWO  "assert-is-half-cube")
  THEN  Auto)

---

Home Index