---

Step * of Lemma rat-point-in-face

No Annotations
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[c,d:ℚCube(k)].
  (rat-point-in-cube(k;x;c)) supposing (rat-point-in-cube(k;x;d) and d ≤ c and (↑Inhabited(c)))
BY
{ (Auto
   THEN RepeatFor 2 (ParallelLast)
   THEN (RWO "assert-inhabited-rat-cube" 5 THENA Auto)
   THEN (D 5 With ⌜i⌝  THENA Auto)
   THEN (D 5 With ⌜i⌝  THENA Auto)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN (GenConcl ⌜(c i) = C ∈ ℚInterval⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (GenConcl ⌜(d i) = D ∈ ℚInterval⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN D -1
   THEN (GenConcl ⌜(x i) = a ∈ ℚ⌝⋅ THENA Auto)
   THEN All Thin) }

1
1. C1 : ℚ
2. C2 : ℚ
3. D1 : ℚ
4. D2 : ℚ
5. a : ℚ
⊢ (((fst(<D1, D2>)) ≤ a) ∧ (a ≤ (snd(<D1, D2>)))) ⇒ (↑Inhabited(<C1, C2>)) ⇒ <D1, D2> ≤ <C1, C2> ⇒ (((fst(<C1, C2>)) \000C≤ a) ∧ (a ≤ (snd(<C1, C2>))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[c,d:\mBbbQ{}Cube(k)].
    (rat-point-in-cube(k;x;c))  supposing  (rat-point-in-cube(k;x;d)  and  d  \mleq{}  c  and  (\muparrow{}Inhabited(c)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (RWO  "assert-inhabited-rat-cube"  5  THENA  Auto)
  THEN  (D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  (D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}(c  i)  =  C\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (GenConcl  \mkleeneopen{}(d  i)  =  D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  (GenConcl  \mkleeneopen{}(x  i)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin)

---

Home Index