---

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


1. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. d : ℚCube(k)
6. e : ℚCube(k)
7. b ≤ e
8. d ≤ c
9. ↑is-half-cube(k;d;b)
10. ↑is-half-cube(k;c;a)
11. ↑Inhabited(a)
12. ↑Inhabited(e)
13. a ⋂ e ≤ a ∧ a ⋂ e ≤ e
⊢ b ≤ a
BY
{ (Thin (-2)
   THEN D -1
   THEN (All (RWO "assert-is-half-cube assert-inhabited-rat-cube") THENA Auto)
   THEN All (RepUR ``rat-cube-face rat-cube-intersection``)
   THEN (D 0 THENA Auto)
   THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Auto) THEN Thin h THEN MoveToConcl (-1)) 
   THEN GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜c i⌝;⌜d i⌝;⌜e i⌝]⋅
   THEN All Thin
   THEN ∀h:hyp. D h 
   THEN RepUR ``is-half-interval inhabited-rat-interval rat-interval-face`` 0
   THEN RepUR ``rat-interval-intersection rat-point-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (Assert ∀a,b,c,d:ℚ.  (<a, b> = <c, d> ∈ ℚInterval ⇐⇒ (a = c ∈ ℚ) ∧ (b = d ∈ ℚ)) BY
               (Unfold `rational-interval` 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN Auto) }

1
1. v13 : ℚ
2. v14 : ℚ
3. v11 : ℚ
4. v12 : ℚ
5. v9 : ℚ
6. v10 : ℚ
7. v7 : ℚ
8. v8 : ℚ
9. v5 : ℚ
10. v6 : ℚ
11. ((v11 = v5 ∈ ℚ) ∧ (v12 = v5 ∈ ℚ)) ∨ ((v11 = v6 ∈ ℚ) ∧ (v12 = v6 ∈ ℚ)) ∨ ((v11 = v5 ∈ ℚ) ∧ (v12 = v6 ∈ ℚ))
12. ((v7 = v9 ∈ ℚ) ∧ (v8 = v9 ∈ ℚ)) ∨ ((v7 = v10 ∈ ℚ) ∧ (v8 = v10 ∈ ℚ)) ∨ ((v7 = v9 ∈ ℚ) ∧ (v8 = v10 ∈ ℚ))
13. ((v7 = v11 ∈ ℚ) ∧ (v8 = qavg(v11;v12) ∈ ℚ)) ∨ ((v7 = qavg(v11;v12) ∈ ℚ) ∧ (v8 = v12 ∈ ℚ))
14. ((v9 = v13 ∈ ℚ) ∧ (v10 = qavg(v13;v14) ∈ ℚ)) ∨ ((v9 = qavg(v13;v14) ∈ ℚ) ∧ (v10 = v14 ∈ ℚ))
15. v13 ≤ v14
16. ((qmax(v13;v5) = v13 ∈ ℚ) ∧ (qmin(v14;v6) = v13 ∈ ℚ))
∨ ((qmax(v13;v5) = v14 ∈ ℚ) ∧ (qmin(v14;v6) = v14 ∈ ℚ))
∨ ((qmax(v13;v5) = v13 ∈ ℚ) ∧ (qmin(v14;v6) = v14 ∈ ℚ))
17. ((qmax(v13;v5) = v5 ∈ ℚ) ∧ (qmin(v14;v6) = v5 ∈ ℚ))
∨ ((qmax(v13;v5) = v6 ∈ ℚ) ∧ (qmin(v14;v6) = v6 ∈ ℚ))
∨ ((qmax(v13;v5) = v5 ∈ ℚ) ∧ (qmin(v14;v6) = v6 ∈ ℚ))
⊢ ((v11 = v13 ∈ ℚ) ∧ (v12 = v13 ∈ ℚ)) ∨ ((v11 = v14 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ)) ∨ ((v11 = v13 ∈ ℚ) ∧ (v12 = v14 ∈ ℚ))

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  a  :  \mBbbQ{}Cube(k)
3.  b  :  \mBbbQ{}Cube(k)
4.  c  :  \mBbbQ{}Cube(k)
5.  d  :  \mBbbQ{}Cube(k)
6.  e  :  \mBbbQ{}Cube(k)
7.  b  \mleq{}  e
8.  d  \mleq{}  c
9.  \muparrow{}is-half-cube(k;d;b)
10.  \muparrow{}is-half-cube(k;c;a)
11.  \muparrow{}Inhabited(a)
12.  \muparrow{}Inhabited(e)
13.  a  \mcap{}  e  \mleq{}  a  \mwedge{}  a  \mcap{}  e  \mleq{}  e
\mvdash{}  b  \mleq{}  a


By

---

Latex:
(Thin  (-2)
  THEN  D  -1
  THEN  (All  (RWO  "assert-is-half-cube  assert-inhabited-rat-cube")  THENA  Auto)
  THEN  All  (RepUR  ``rat-cube-face  rat-cube-intersection``)
  THEN  (D  0  THENA  Auto)
  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{};\mkleeneopen{}d  i\mkleeneclose{};\mkleeneopen{}e  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  \mforall{}h:hyp.  D  h 
  THEN  RepUR  ``is-half-interval  inhabited-rat-interval  rat-interval-face``  0
  THEN  RepUR  ``rat-interval-intersection  rat-point-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (Assert  \mforall{}a,b,c,d:\mBbbQ{}.    (<a,  b>  =  <c,  d>  \mLeftarrow{}{}\mRightarrow{}  (a  =  c)  \mwedge{}  (b  =  d))  BY
                          (Unfold  `rational-interval`  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Auto)

---

Home Index