---

Step * 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))
⊢ ∃!d:ℚCube(k). ((↑is-half-cube(k;d;c)) ∧ (∀i:ℕk. a i ≤ d i))
BY
{ Assert ⌜∀i:ℕk. ∃!I:ℚInterval. ((↑is-half-interval(I;c i)) ∧ a i ≤ I)⌝⋅ }

1
.....assertion..... 
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))
⊢ ∀i:ℕk. ∃!I:ℚInterval. ((↑is-half-interval(I;c i)) ∧ a i ≤ I)

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

---

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))
\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:
Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}k.  \mexists{}!I:\mBbbQ{}Interval.  ((\muparrow{}is-half-interval(I;c  i))  \mwedge{}  a  i  \mleq{}  I)\mkleeneclose{}\mcdot{}

---

Home Index