---

Step * of Lemma common-face-inhabited-intersection

No Annotations
∀k:ℕ. ∀a,b,b':ℚCube(k).  ((↑Inhabited(b')) ⇒ (↑Inhabited(b)) ⇒ (a ≤ b ∧ a ≤ b') ⇒ (↑Inhabited(b ⋂ b')))
BY
{ ((RWO "assert-inhabited-rat-cube" 0 THENA Auto)
   THEN RepUR ``rat-cube-face rat-cube-intersection`` 0
   THEN Auto
   THEN ∀h:hyp. ((InstHyp [⌜i⌝] h⋅ THENA Auto) THEN MoveToConcl (-1)) 
   THEN GenConclTerms Auto [⌜a i⌝;⌜b i⌝;⌜b' i⌝]⋅
   THEN All Thin
   THEN ∀h:hyp. D h 
   THEN RepUR ``inhabited-rat-interval rat-interval-intersection`` 0
   THEN RepUR ``rat-interval-face rat-point-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN Auto) }

1
1. v7 : ℚ
2. v8 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. v3 : ℚ
6. v4 : ℚ
7. v3 ≤ v4
8. v5 ≤ v6
9. (<v7, v8> = <v5, v5> ∈ ℚInterval) ∨ (<v7, v8> = <v6, v6> ∈ ℚInterval) ∨ (<v7, v8> = <v5, v6> ∈ ℚInterval)
10. (<v7, v8> = <v3, v3> ∈ ℚInterval) ∨ (<v7, v8> = <v4, v4> ∈ ℚInterval) ∨ (<v7, v8> = <v3, v4> ∈ ℚInterval)
⊢ qmax(v5;v3) ≤ qmin(v6;v4)

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}a,b,b':\mBbbQ{}Cube(k).
    ((\muparrow{}Inhabited(b'))  {}\mRightarrow{}  (\muparrow{}Inhabited(b))  {}\mRightarrow{}  (a  \mleq{}  b  \mwedge{}  a  \mleq{}  b')  {}\mRightarrow{}  (\muparrow{}Inhabited(b  \mcap{}  b')))


By

---

Latex:
((RWO  "assert-inhabited-rat-cube"  0  THENA  Auto)
  THEN  RepUR  ``rat-cube-face  rat-cube-intersection``  0
  THEN  Auto
  THEN  \mforall{}h:hyp.  ((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h\mcdot{}  THENA  Auto)  THEN  MoveToConcl  (-1)) 
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}b'  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  \mforall{}h:hyp.  D  h 
  THEN  RepUR  ``inhabited-rat-interval  rat-interval-intersection``  0
  THEN  RepUR  ``rat-interval-face  rat-point-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  Auto)

---

Home Index