---

Step * 1 2 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)
⊢ ∃!d:ℚCube(k). ((↑is-half-cube(k;d;c)) ∧ (∀i:ℕk. a i ≤ d i))
BY
{ (Unfold `exists!` -1
   THEN (Skolemize (-1) `d' THENA Auto)
   THEN Fold `rational-cube` (-2)
   THEN D 0 With ⌜d⌝ 
   THEN Auto
   THEN Try ((RWO "assert-is-half-cube" 0 THEN Auto))
   THEN Unfold `rational-cube` 0
   THEN FunExt
   THEN Auto) }

1
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

---

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)
\mvdash{}  \mexists{}!d:\mBbbQ{}Cube(k).  ((\muparrow{}is-half-cube(k;d;c))  \mwedge{}  (\mforall{}i:\mBbbN{}k.  a  i  \mleq{}  d  i))


By

---

Latex:
(Unfold  `exists!`  -1
  THEN  (Skolemize  (-1)  `d'  THENA  Auto)
  THEN  Fold  `rational-cube`  (-2)
  THEN  D  0  With  \mkleeneopen{}d\mkleeneclose{} 
  THEN  Auto
  THEN  Try  ((RWO  "assert-is-half-cube"  0  THEN  Auto))
  THEN  Unfold  `rational-cube`  0
  THEN  FunExt
  THEN  Auto)

---

Home Index