---

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


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)
BY
{ (DVar `v1'
   THEN DVar `v2'
   THEN RepUR ``rat-interval-face rat-point-interval`` -2
   THEN SplitOrHyps
   THEN (EqHD (-2) THENA Auto)
   THEN All Reduce
   THEN RationalElim ⌜v3⌝⋅
   THEN RationalElim ⌜v4⌝⋅
   THEN Try ((Fold `rat-point-interval` (-1) THEN (FLemma `half-point-interval` [-1] THENA Auto)))) }

1
1. v5 : ℚ
2. v : ℚInterval
3. v6 : ℚ
4. ↑is-half-interval(v;[v5])
5. v = [v5] ∈ ℚInterval
⊢ ∃!I:ℚInterval. ((↑is-half-interval(I;<v5, v6>)) ∧ v ≤ I)

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

3
1. v6 : ℚ
2. v5 : ℚ
3. v : ℚInterval
4. ↑is-half-interval(v;<v5, v6>)
⊢ ∃!I:ℚInterval. ((↑is-half-interval(I;<v5, v6>)) ∧ v ≤ I)

---

Latex:

---

Latex:

1.  v  :  \mBbbQ{}Interval
2.  v1  :  \mBbbQ{}Interval
3.  v2  :  \mBbbQ{}Interval
4.  v1  \mleq{}  v2
5.  \muparrow{}is-half-interval(v;v1)
\mvdash{}  \mexists{}!I:\mBbbQ{}Interval.  ((\muparrow{}is-half-interval(I;v2))  \mwedge{}  v  \mleq{}  I)


By

---

Latex:
(DVar  `v1'
  THEN  DVar  `v2'
  THEN  RepUR  ``rat-interval-face  rat-point-interval``  -2
  THEN  SplitOrHyps
  THEN  (EqHD  (-2)  THENA  Auto)
  THEN  All  Reduce
  THEN  RationalElim  \mkleeneopen{}v3\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}v4\mkleeneclose{}\mcdot{}
  THEN  Try  ((Fold  `rat-point-interval`  (-1)  THEN  (FLemma  `half-point-interval`  [-1]  THENA  Auto))))

---

Home Index