---

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

.....antecedent..... 
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)
⊢ ↑Inhabited(a ⋂ e)
BY
{ ((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 ((GenConclTerm ⌜a i⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN RenameVar `a1' (-2) THEN RenameVar `a2' (-1))
   THEN ((GenConclTerm ⌜b i⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN RenameVar `b1' (-2) THEN RenameVar `b2' (-1))
   THEN ((GenConclTerm ⌜c i⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN RenameVar `c1' (-2) THEN RenameVar `c2' (-1))
   THEN ((GenConclTerm ⌜d i⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1 THEN RenameVar `d1' (-2) THEN RenameVar `d2' (-1))
   THEN (GenConclTerm ⌜e i⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN RenameVar `e1' (-2)
   THEN RenameVar `e2' (-1)
   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. k : ℕ
2. a : ℚCube(k)
3. b : ℚCube(k)
4. c : ℚCube(k)
5. d : ℚCube(k)
6. e : ℚCube(k)
7. i : ℕk
8. a1 : ℚ
9. a2 : ℚ
10. b1 : ℚ
11. b2 : ℚ
12. c1 : ℚ
13. c2 : ℚ
14. d1 : ℚ
15. d2 : ℚ
16. e1 : ℚ
17. e2 : ℚ
18. ((b1 = e1 ∈ ℚ) ∧ (b2 = e1 ∈ ℚ)) ∨ ((b1 = e2 ∈ ℚ) ∧ (b2 = e2 ∈ ℚ)) ∨ ((b1 = e1 ∈ ℚ) ∧ (b2 = e2 ∈ ℚ))
19. ((d1 = c1 ∈ ℚ) ∧ (d2 = c1 ∈ ℚ)) ∨ ((d1 = c2 ∈ ℚ) ∧ (d2 = c2 ∈ ℚ)) ∨ ((d1 = c1 ∈ ℚ) ∧ (d2 = c2 ∈ ℚ))
20. ((d1 = b1 ∈ ℚ) ∧ (d2 = qavg(b1;b2) ∈ ℚ)) ∨ ((d1 = qavg(b1;b2) ∈ ℚ) ∧ (d2 = b2 ∈ ℚ))
21. ((c1 = a1 ∈ ℚ) ∧ (c2 = qavg(a1;a2) ∈ ℚ)) ∨ ((c1 = qavg(a1;a2) ∈ ℚ) ∧ (c2 = a2 ∈ ℚ))
22. a1 ≤ a2
23. e1 ≤ e2
⊢ qmax(a1;e1) ≤ qmin(a2;e2)

---

Latex:

---

Latex:
.....antecedent..... 
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)
\mvdash{}  \muparrow{}Inhabited(a  \mcap{}  e)


By

---

Latex:
((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  ((GenConclTerm  \mkleeneopen{}a  i\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RenameVar  `a1'  (-2)
              THEN  RenameVar  `a2'  (-1))
  THEN  ((GenConclTerm  \mkleeneopen{}b  i\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RenameVar  `b1'  (-2)
              THEN  RenameVar  `b2'  (-1))
  THEN  ((GenConclTerm  \mkleeneopen{}c  i\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RenameVar  `c1'  (-2)
              THEN  RenameVar  `c2'  (-1))
  THEN  ((GenConclTerm  \mkleeneopen{}d  i\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RenameVar  `d1'  (-2)
              THEN  RenameVar  `d2'  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}e  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  RenameVar  `e1'  (-2)
  THEN  RenameVar  `e2'  (-1)
  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