---

Step * of Lemma rat-point-in-cube-interior-not-in-face

No Annotations
∀[k:ℕ]. ∀[x:ℕk ⟶ ℚ]. ∀[a:ℚCube(k)].
  ∀f:ℚCube(k). (f ≤ a ⇒ rat-point-in-cube(k;x;f) ⇒ (f = a ∈ ℚCube(k))) supposing rat-point-in-cube-interior(k;x;a)
BY
{ ((Auto THEN Unfold `rational-cube` 0)
   THEN (FunExt THENA Auto)
   THEN RenameVar `i' (-1)
   THEN ((D 4 With ⌜i⌝  THENA Auto) THEN MoveToConcl (-1))
   THEN RepeatFor 2 (((D 5 With ⌜i⌝  THENA Auto) THEN MoveToConcl (-1)))
   THEN ((GenConcl ⌜(f i) = F ∈ ℚInterval⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1)
   THEN ((GenConcl ⌜(a i) = A ∈ ℚInterval⌝⋅ THENA Auto) THEN Thin (-1) THEN D -1)
   THEN GenConclTerms Auto [⌜x i⌝]⋅
   THEN All Thin
   THEN RepUR ``rat-interval-face rat-point-interval inhabited-rat-interval`` 0
   THEN RW assert_pushdownC 0
   THEN Auto
   THEN SplitOrHyps
   THEN (EqHD (-4) THENA Auto)
   THEN All Reduce
   THEN RationalElim ⌜F1⌝⋅
   THEN RationalElim ⌜F2⌝⋅
   THEN Auto
   THEN Decide ⌜A1 < A2⌝⋅
   THEN Auto
   THEN RWO "qless_complement_qorder" (-1)
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}[x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[a:\mBbbQ{}Cube(k)].
    \mforall{}f:\mBbbQ{}Cube(k).  (f  \mleq{}  a  {}\mRightarrow{}  rat-point-in-cube(k;x;f)  {}\mRightarrow{}  (f  =  a)) 
    supposing  rat-point-in-cube-interior(k;x;a)


By

---

Latex:
((Auto  THEN  Unfold  `rational-cube`  0)
  THEN  (FunExt  THENA  Auto)
  THEN  RenameVar  `i'  (-1)
  THEN  ((D  4  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1))
  THEN  RepeatFor  2  (((D  5  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)  THEN  MoveToConcl  (-1)))
  THEN  ((GenConcl  \mkleeneopen{}(f  i)  =  F\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1)
  THEN  ((GenConcl  \mkleeneopen{}(a  i)  =  A\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Thin  (-1)  THEN  D  -1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}x  i\mkleeneclose{}]\mcdot{}
  THEN  All  Thin
  THEN  RepUR  ``rat-interval-face  rat-point-interval  inhabited-rat-interval``  0
  THEN  RW  assert\_pushdownC  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  (EqHD  (-4)  THENA  Auto)
  THEN  All  Reduce
  THEN  RationalElim  \mkleeneopen{}F1\mkleeneclose{}\mcdot{}
  THEN  RationalElim  \mkleeneopen{}F2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Decide  \mkleeneopen{}A1  <  A2\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  RWO  "qless\_complement\_qorder"  (-1)
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index