---

Step * of Lemma inhabited-half-cube

No Annotations
∀k:ℕ. ∀a,b:ℚCube(k).  ((↑is-half-cube(k;a;b)) ⇒ (↑Inhabited(a) ⇐⇒ ↑Inhabited(b)))
BY
{ (RepeatFor 3 (Intro)
   THEN (RWO "assert-is-half-cube" 0 THENA Auto)
   THEN Auto
   THEN (RWO "assert-inhabited-rat-cube" (-1) THENA Auto)
   THEN (RWO "assert-inhabited-rat-cube" 0 THENA Auto)
   THEN ParallelLast
   THEN (Assert ↑is-half-interval(a i;b i) BY
               Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclTerms Auto [⌜a i⌝; ⌜b i⌝]⋅
   THEN All Thin) }

1
1. v : ℚInterval
2. v1 : ℚInterval
⊢ (↑Inhabited(v)) ⇒ (↑is-half-interval(v;v1)) ⇒ (↑Inhabited(v1))

2
1. v : ℚInterval
2. v1 : ℚInterval
⊢ (↑Inhabited(v1)) ⇒ (↑is-half-interval(v;v1)) ⇒ (↑Inhabited(v))

---

Latex:

---

Latex:
No  Annotations
\mforall{}k:\mBbbN{}.  \mforall{}a,b:\mBbbQ{}Cube(k).    ((\muparrow{}is-half-cube(k;a;b))  {}\mRightarrow{}  (\muparrow{}Inhabited(a)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}Inhabited(b)))


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (RWO  "assert-is-half-cube"  0  THENA  Auto)
  THEN  Auto
  THEN  (RWO  "assert-inhabited-rat-cube"  (-1)  THENA  Auto)
  THEN  (RWO  "assert-inhabited-rat-cube"  0  THENA  Auto)
  THEN  ParallelLast
  THEN  (Assert  \muparrow{}is-half-interval(a  i;b  i)  BY
                          Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  i\mkleeneclose{};  \mkleeneopen{}b  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index