---

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

.....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)
BY
{ (Intro
   THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Auto) THEN Thin h THEN MoveToConcl (-1)) 
   THEN GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜c i⌝]⋅
   THEN All Thin
   THEN Auto) }

1
1. v : ℚInterval
2. v1 : ℚInterval
3. v2 : ℚInterval
4. v1 ≤ v2
5. ↑is-half-interval(v;v1)
⊢ ∃!I:ℚInterval. ((↑is-half-interval(I;v2)) ∧ v ≤ I)

---

Latex:

---

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


By

---

Latex:
(Intro
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  Thin  h  THEN  MoveToConcl  (-1)) 
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}c  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  Auto)

---

Home Index