---

Step * of Lemma face-of-intersection

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

1
1. v : ℚInterval
2. v1 : ℚInterval
3. v2 : ℚInterval
⊢ ((↑Inhabited(v2)) ∧ (↑Inhabited(v1))) ⇒ v ≤ v2 ⇒ v ≤ v1 ⇒ v ≤ v1 ⋂ v2

---

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{}  a  \mleq{}  b  \mcap{}  b')


By

---

Latex:
((Auto  THEN  (All  (RWO  "assert-inhabited-rat-cube")  THENA  Auto))
  THEN  All  (RepUR  ``rat-cube-face``)
  THEN  ParallelLast
  THEN  (D  -4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepUR  ``rat-cube-intersection``  0
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (Assert  (\muparrow{}Inhabited(b'  i))  \mwedge{}  (\muparrow{}Inhabited(b  i))  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};\mkleeneopen{}b  i\mkleeneclose{};\mkleeneopen{}b'  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index