---

Step * of Lemma real-ball-slice_wf

∀[r:{r:ℝ| r0 ≤ r} ]
  ∀n:ℕ+. ∀t:{t:ℝ| t ∈ [-(r), r]} . ∀i:ℕn. ∀p:B(n - 1;ball-slice-radius(r;t)).  (real-ball-slice(p;i;t) ∈ B(n;r))
BY
{ (Auto
   THEN (Assert λj.if j <z i then p j
                   if i <z j then p (j - 1)
                   else t
                   fi  ∈ ℝ^n BY
               (Unfold `real-vec` 0 THEN FunExt THEN Reduce 0 THEN Auto))
   THEN Unfold `real-ball-slice` 0
   THEN MemTypeCD
   THEN Auto
   THEN (BLemma `square-rleq-implies` THENA Auto)
   THEN ((RWO "real-vec-norm-squared" 0 THENA Auto) ORELSE Auto)
   THEN D -2
   THEN (Unhide THENA Auto)
   THEN (Assert (p⋅p + t^2) ≤ r^2 BY
               ((Assert ||p||^2 ≤ ball-slice-radius(r;t)^2 BY
                       (RWO  "-2" 0 THEN Auto))
                THEN (RWO  "real-vec-norm-squared" (-1) THENA Auto)
                THEN (RWO  "-1" 0 THENA Auto)
                THEN (GenConclTerm ⌜ball-slice-radius(r;t)⌝⋅ THENA Auto)
                THEN D -2
                THEN Unhide
                THEN Auto
                THEN RWO "-2<" 0
                THEN Auto))) }

1
1. r : {r:ℝ| r0 ≤ r} 
2. n : ℕ+
3. t : {t:ℝ| t ∈ [-(r), r]} 
4. i : ℕn
5. p : ℝ^n - 1
6. ||p|| ≤ ball-slice-radius(r;t)
7. λj.if j <z i then p j
      if i <z j then p (j - 1)
      else t
      fi  ∈ ℝ^n
8. (p⋅p + t^2) ≤ r^2
⊢ λj.if j <z i then p j
     if i <z j then p (j - 1)
     else t
     fi ⋅λj.if j <z i then p j
            if i <z j then p (j - 1)
            else t
            fi  ≤ r^2

---

Latex:

---

Latex:
\mforall{}[r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  ]
    \mforall{}n:\mBbbN{}\msupplus{}.  \mforall{}t:\{t:\mBbbR{}|  t  \mmember{}  [-(r),  r]\}  .  \mforall{}i:\mBbbN{}n.  \mforall{}p:B(n  -  1;ball-slice-radius(r;t)).
        (real-ball-slice(p;i;t)  \mmember{}  B(n;r))


By

---

Latex:
(Auto
  THEN  (Assert  \mlambda{}j.if  j  <z  i  then  p  j
                                  if  i  <z  j  then  p  (j  -  1)
                                  else  t
                                  fi    \mmember{}  \mBbbR{}\^{}n  BY
                          (Unfold  `real-vec`  0  THEN  FunExt  THEN  Reduce  0  THEN  Auto))
  THEN  Unfold  `real-ball-slice`  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  (BLemma  `square-rleq-implies`  THENA  Auto)
  THEN  ((RWO  "real-vec-norm-squared"  0  THENA  Auto)  ORELSE  Auto)
  THEN  D  -2
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  (p\mcdot{}p  +  t\^{}2)  \mleq{}  r\^{}2  BY
                          ((Assert  ||p||\^{}2  \mleq{}  ball-slice-radius(r;t)\^{}2  BY
                                          (RWO    "-2"  0  THEN  Auto))
                            THEN  (RWO    "real-vec-norm-squared"  (-1)  THENA  Auto)
                            THEN  (RWO    "-1"  0  THENA  Auto)
                            THEN  (GenConclTerm  \mkleeneopen{}ball-slice-radius(r;t)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  D  -2
                            THEN  Unhide
                            THEN  Auto
                            THEN  RWO  "-2<"  0
                            THEN  Auto)))

---

Home Index