---

Step * of Lemma half-cube-of-face

∀k:ℕ. ∀a,b,c,d,e:ℚCube(k).
  (Compatible(a;e)
  ⇒ b ≤ e
  ⇒ d ≤ c
  ⇒ (b ≤ a) supposing ((↑Inhabited(e)) and (↑Inhabited(a)) and (↑is-half-cube(k;c;a)) and (↑is-half-cube(k;d;b))))
BY
{ (Auto THEN D 7) }

1
.....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)

2
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

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}.  \mforall{}a,b,c,d,e:\mBbbQ{}Cube(k).
    (Compatible(a;e)
    {}\mRightarrow{}  b  \mleq{}  e
    {}\mRightarrow{}  d  \mleq{}  c
    {}\mRightarrow{}  (b  \mleq{}  a)  supposing 
                ((\muparrow{}Inhabited(e))  and 
                (\muparrow{}Inhabited(a))  and 
                (\muparrow{}is-half-cube(k;c;a))  and 
                (\muparrow{}is-half-cube(k;d;b))))


By

---

Latex:
(Auto  THEN  D  7)

---

Home Index