---

Step * 1 1 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. 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)
BY
{ (Assert ⌜(a1 ≤ e2) ∧ (e1 ≤ a2)⌝⋅ THENM ((RWO "qmax_lb" 0 THENA Auto) THEN RWO "qmin_ub" 0 THEN Auto)) }

1
.....assertion..... 
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
⊢ (a1 ≤ e2) ∧ (e1 ≤ a2)

---

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.  i  :  \mBbbN{}k
8.  a1  :  \mBbbQ{}
9.  a2  :  \mBbbQ{}
10.  b1  :  \mBbbQ{}
11.  b2  :  \mBbbQ{}
12.  c1  :  \mBbbQ{}
13.  c2  :  \mBbbQ{}
14.  d1  :  \mBbbQ{}
15.  d2  :  \mBbbQ{}
16.  e1  :  \mBbbQ{}
17.  e2  :  \mBbbQ{}
18.  ((b1  =  e1)  \mwedge{}  (b2  =  e1))  \mvee{}  ((b1  =  e2)  \mwedge{}  (b2  =  e2))  \mvee{}  ((b1  =  e1)  \mwedge{}  (b2  =  e2))
19.  ((d1  =  c1)  \mwedge{}  (d2  =  c1))  \mvee{}  ((d1  =  c2)  \mwedge{}  (d2  =  c2))  \mvee{}  ((d1  =  c1)  \mwedge{}  (d2  =  c2))
20.  ((d1  =  b1)  \mwedge{}  (d2  =  qavg(b1;b2)))  \mvee{}  ((d1  =  qavg(b1;b2))  \mwedge{}  (d2  =  b2))
21.  ((c1  =  a1)  \mwedge{}  (c2  =  qavg(a1;a2)))  \mvee{}  ((c1  =  qavg(a1;a2))  \mwedge{}  (c2  =  a2))
22.  a1  \mleq{}  a2
23.  e1  \mleq{}  e2
\mvdash{}  qmax(a1;e1)  \mleq{}  qmin(a2;e2)


By

---

Latex:
(Assert  \mkleeneopen{}(a1  \mleq{}  e2)  \mwedge{}  (e1  \mleq{}  a2)\mkleeneclose{}\mcdot{}
THENM  ((RWO  "qmax\_lb"  0  THENA  Auto)  THEN  RWO  "qmin\_ub"  0  THEN  Auto)
)

---

Home Index