Lemma: real-vec-be-unique-1
[n:ℕ]. ∀[x,y,u,v:ℝ^n].
  ((||x|| ≤ r1)
   (||y|| ≤ r1)
   x ≠ y
   (||v|| r1)
   (||u|| r1)
   real-vec-be(n;u;x;y)
   real-vec-be(n;v;x;y)
   req-vec(n;u;v))

Definition: real-cube
real-cube(n;a;b) ==  {p:ℝ^n| ∀i:ℕn. (p i ∈ [a i, i])} 

Lemma: real-cube_wf
[n:ℕ]. ∀[a,b:ℕn ⟶ ℝ].  (real-cube(n;a;b) ∈ Type)

Definition: real-cube-interior
real-cube-interior(n;a;b) ==  {p:ℝ^n| ∀i:ℕn. (p i ∈ (a i, i))} 

Lemma: real-cube-interior_wf
[n:ℕ]. ∀[a,b:ℕn ⟶ ℝ].  (real-cube-interior(n;a;b) ∈ Type)

Definition: real-cube-boundary
real-cube-boundary(n;a;b) ==  {p:ℝ^n| (∀i:ℕn. (p i ∈ [a i, i])) ∧ (∀i:ℕn. (p i ∈ (a i, i))))} 

Lemma: real-cube-boundary_wf
[n:ℕ]. ∀[a,b:ℕn ⟶ ℝ].  (real-cube-boundary(n;a;b) ∈ Type)

Definition: in-rat-cube
in-rat-cube(k;p;c) ==  ∀i:ℕk. ((rat2real(fst((c i))) ≤ (p i)) ∧ ((p i) ≤ rat2real(snd((c i)))))

Lemma: in-rat-cube_wf
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].  (in-rat-cube(k;p;c) ∈ ℙ)

Lemma: in-rat-cube_functionality
[k:ℕ]. ∀[p,q:ℝ^k]. ∀[c:ℚCube(k)].  uiff(in-rat-cube(k;p;c);in-rat-cube(k;q;c)) supposing p ≡ q

Lemma: in-rat-half-cube
k:ℕ. ∀c,h:ℚCube(k).  ((↑is-half-cube(k;h;c))  (∀x:ℝ^k. (in-rat-cube(k;x;h)  in-rat-cube(k;x;c))))

Lemma: in-rat-cube-intersection
k:ℕ. ∀c,d:ℚCube(k). ∀x:ℝ^k.  (in-rat-cube(k;x;c ⋂ d) ⇐⇒ in-rat-cube(k;x;c) ∧ in-rat-cube(k;x;d))

Lemma: in-some-half-cube
k:ℕ. ∀x:ℝ^k. ∀c:ℚCube(k).  (in-rat-cube(k;x;c)  (¬¬(∃h:ℚCube(k). ((↑is-half-cube(k;h;c)) ∧ in-rat-cube(k;x;h)))))

Definition: rat-cube-diameter
rat-cube-diameter(k;c) ==  Σ{rmax(r0;rat2real(snd((c i))) rat2real(fst((c i)))) 0≤i≤1}

Lemma: rat-cube-diameter_wf
[k:ℕ]. ∀[c:ℚCube(k)].  (rat-cube-diameter(k;c) ∈ ℝ)

Lemma: rat-cube-diameter-bound
[k:ℕ]. ∀[c:ℚCube(k)]. ∀[x,y:ℝ^k].
  (mdist(rn-prod-metric(k);x;y) ≤ rat-cube-diameter(k;c)) supposing (in-rat-cube(k;y;c) and in-rat-cube(k;x;c))

Definition: rat-complex-diameter
rat-complex-diameter(k;K) ==  rmaximum(0;||K|| 1;i.rat-cube-diameter(k;K[i]))

Lemma: rat-complex-diameter_wf
[k:ℕ]. ∀[K:ℚCube(k) List].  rat-complex-diameter(k;K) ∈ ℝ supposing 0 < ||K||

Lemma: rat-half-cube-diameter
[k:ℕ]. ∀[c,h:ℚCube(k)].  rat-cube-diameter(k;h) ((r1/r(2)) rat-cube-diameter(k;c)) supposing ↑is-half-cube(k;h;c)

Lemma: rat-sub-div-diameter
[k,n:ℕ]. ∀[K:n-dim-complex].
  rat-complex-diameter(k;(K)') ≤ ((r1/r(2)) rat-complex-diameter(k;K)) supposing 0 < ||K||

Lemma: sq_stable__in-rat-cube
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].  SqStable(in-rat-cube(k;p;c))

Lemma: stable__in-rat-cube
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].  Stable{in-rat-cube(k;p;c)}

Lemma: in-rat-cube-face
[k:ℕ]. ∀[p:ℝ^k]. ∀[c,f:ℚCube(k)].  (in-rat-cube(k;p;c)) supposing (in-rat-cube(k;p;f) and (↑Inhabited(c)) and f ≤ c)

Lemma: in-0-dim-cube
[k:ℕ]. ∀[c:ℚCube(k)].  ∀[p:ℝ^k]. uiff(in-rat-cube(k;p;c);req-vec(k;p;λj.rat2real(fst((c j))))) supposing dim(c) 0 ∈ ℤ

Lemma: meq-in-0-dim-cube
[k:ℕ]. ∀[c:ℚCube(k)].  ∀[p,q:ℝ^k].  (p ≡ q) supposing (in-rat-cube(k;q;c) and in-rat-cube(k;p;c)) supposing dim(c) \000C∈ ℤ

Lemma: not-not-in-0-dim-cube
[k:ℕ]. ∀[c:ℚCube(k)].
  ∀[p:ℝ^k]. uiff(¬¬in-rat-cube(k;p;c);req-vec(k;p;λj.rat2real(fst((c j))))) supposing dim(c) 0 ∈ ℤ

Lemma: intersecting-0-dim-cubes
k:ℕ. ∀b:ℚCube(k). ∀q:ℝ^k. ∀c:ℚCube(k).
  ((in-rat-cube(k;q;c) ∧ in-rat-cube(k;q;b) ∧ (dim(c) 0 ∈ ℤ) ∧ (dim(b) 0 ∈ ℤ))  (c b ∈ ℚCube(k)))

Lemma: inhabited-iff-in-rat-cube
[k:ℕ]. ∀c:ℚCube(k). (↑Inhabited(c) ⇐⇒ ∃p:ℝ^k. in-rat-cube(k;p;c))

Lemma: in-compatible-cubes
k:ℕ. ∀c,d:ℚCube(k).
  (Compatible(c;d)
   (∀p:ℝ^k. (in-rat-cube(k;p;c)  in-rat-cube(k;p;d)  (∃f:ℚCube(k). (f ≤ c ∧ f ≤ d ∧ in-rat-cube(k;p;f))))))

Lemma: mcompact-rat-cube
k:ℕ. ∀c:ℚCube(k).  ((↑Inhabited(c))  mcompact({x:ℝ^k| in-rat-cube(k;x;c)} ;rn-prod-metric(k)))

Definition: rat-interval-third
rat-interval-third(p;I) ==
  let a,b 
  in (p ((r(2) rat2real(a)) rat2real(b)/r(3))) ∨ (p (rat2real(a) (r(2) rat2real(b))/r(3)))

Lemma: rat-interval-third_wf
[p:ℝ]. ∀[I:ℚInterval].  (rat-interval-third(p;I) ∈ ℙ)

Definition: rat-cube-third
rat-cube-third(k;p;c) ==  in-rat-cube(k;p;c)  (∀i:ℕk. rat-interval-third(p i;c i))

Lemma: rat-cube-third_wf
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].  (rat-cube-third(k;p;c) ∈ ℙ)

Lemma: rat-cube-third-exists
k:ℕ. ∀c:ℚCube(k).  ((↑Inhabited(c))  (∃p:ℝ^k. (in-rat-cube(k;p;c) ∧ rat-cube-third(k;p;c))))

Lemma: rat-cube-third-half
k:ℕ. ∀p:ℝ^k. ∀c:ℚCube(k).  (rat-cube-third(k;p;c)  (∀h:ℚCube(k). ((↑is-half-cube(k;h;c))  rat-cube-third(k;p;h))))

Lemma: not-rat-cube-third
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].
  rat-cube-third(k;p;c) ⇐⇒ in-rat-cube(k;p;c) ∧ (¬¬(∃i:ℕk. rat-interval-third(p i;c i)))))

Lemma: rat-cube-third-not-in-face
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:ℚCube(k)].
  ∀f:ℚCube(k). in-rat-cube(k;p;f)) supposing ((¬(f c ∈ ℚCube(k))) and f ≤ c) supposing rat-cube-third(k;p;c) ∧ (↑Inh\000Cabited(c))

Lemma: rat-cube-third-complex
k,n:ℕ. ∀K:n-dim-complex. ∀c:ℚCube(k).
  ((c ∈ K)  (∀p:ℝ^k. (in-rat-cube(k;p;c)  rat-cube-third(k;p;c)  (∀j:ℕ(¬¬(∀d∈K'^(j).rat-cube-third(k;p;d)))))))

Definition: rat-cube-complex-polyhedron
|K| ==  {p:ℝ^k| ¬¬(∃c∈K. in-rat-cube(k;p;c))} 

Lemma: rat-cube-complex-polyhedron_wf
[k:ℕ]. ∀[K:ℚCube(k) List].  (|K| ∈ Type)

Lemma: rat-cube-complex-polyhedron_functionality
[k:ℕ]. ∀[K,L:ℚCube(k) List].  |K| ≡ |L| supposing permutation(ℚCube(k);K;L)

Lemma: rat-cube-complex-polyhedron-compact1
k:ℕ. ∀K:ℚCube(k) List.  (0 < ||K||  (∀c∈K.↑Inhabited(c))  mcompact(|K|;rn-prod-metric(k)))

Lemma: rat-cube-complex-polyhedron-compact
k:ℕ. ∀[n:ℕ]. ∀K:{K:n-dim-complex| 0 < ||K||} mcompact(|K|;rn-prod-metric(k))

Lemma: rat-cube-complex-polyhedron-metric-subspace
[k:ℕ]. ∀[K:ℚCube(k) List].  metric-subspace(ℝ^k;rn-prod-metric(k);|K|)

Lemma: rat-complex-subdiv-polyhedron
[k,n:ℕ]. ∀[K:n-dim-complex].  |(K)'| ≡ |K|

Lemma: rat-complex-iter-subdiv-polyhedron
[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[j:ℕ].  |K'^(j)| ≡ |K|

Lemma: rat-complex-boundary-iter-subdiv-polyhedron
[k,n:ℕ]. ∀[K:n-dim-complex]. ∀[j:ℕ].  |∂(K'^(j))| ≡ |∂(K)|

Lemma: rat-complex-diameter-bound
[k:ℕ]. ∀[K:ℚCube(k) List].
  ∀[x,y:ℝ^k].
    mdist(rn-prod-metric(k);x;y) ≤ rat-complex-diameter(k;K) 
    supposing ¬¬(∃c:ℚCube(k). ((c ∈ K) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c))) 
  supposing 0 < ||K||

Lemma: rat-complex-iter-subdiv-pos-length
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[j:ℕ].  0 < ||K'^(j)||

Lemma: rat-complex-iter-subdiv-diameter
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[j:ℕ].
  (rat-complex-diameter(k;K'^(j)) ≤ ((r1/r(2^j)) rat-complex-diameter(k;K)))

Lemma: fine-iter-subdiv
k:ℕ
  ∀[n:ℕ]
    ∀K:{K:n-dim-complex| 0 < ||K||} . ∀M:ℕ+.
      ∃j:ℕ
       ∀[x,y:ℝ^k].
         mdist(rn-prod-metric(k);x;y) ≤ (r1/r(M)) 
         supposing ¬¬(∃c:ℚCube(k). ((c ∈ K'^(j)) ∧ in-rat-cube(k;y;c) ∧ in-rat-cube(k;x;c)))

Definition: rccp-compact
rccp-compact(k;K) ==  TERMOF{rat-cube-complex-polyhedron-compact:o, 1:l} K

Lemma: rccp-compact_wf
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ].  (rccp-compact(k;K) ∈ mcompact(|K|;rn-prod-metric(k)))

Definition: rccp-dist
dist(x, |K|) ==  dist(x;|K|)

Lemma: rccp-dist_wf
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[x:ℝ^k].  (dist(x, |K|) ∈ ℝ)

Lemma: rccp-dist-nonneg
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[x:ℝ^k].  (r0 ≤ dist(x, |K|))

Lemma: rccp-dist-0
[k,n:ℕ]. ∀[K:{K:n-dim-complex| 0 < ||K||} ]. ∀[x:ℝ^k].  uiff(dist(x, |K|) r0;x ∈ |K|)

Lemma: rccp-dist-positive
k:ℕ
  ∀[n:ℕ]
    ∀K:{K:n-dim-complex| 0 < ||K||} . ∀x:ℝ^k.
      (r0 < dist(x, |K|) ⇐⇒ ∃n:ℕ+. ∀p:|K|. ((r1/r(n)) ≤ mdist(rn-prod-metric(k);x;p)))

Lemma: rat-cube-complex-polyhedron-closed
[k:ℕ]. ∀[K:ℚCube(k) List]. ∀[v:|K|]. ∀[x:ℝ^k].  x ∈ |K| supposing v ≡ x

Lemma: rat-cube-complex-polyhedron-subtype
[k:ℕ]. ∀[K,L:ℚCube(k) List].  |L| ⊆|K| supposing L ⊆ K

Lemma: rat-cube-sub-complex-polyhedron-subtype
[k:ℕ]. ∀[K:ℚCube(k) List]. ∀[P:{c:ℚCube(k)| (c ∈ K)}  ⟶ 𝔹].  (|rat-cube-sub-complex(P;K)| ⊆|K|)

Lemma: rat-cube-complex-polyhedron-inhabited
k:ℕ. ∀[n:ℕ]. ∀K:n-dim-complex. (0 < ||K||  |K|)

Lemma: 0-dim-complex-polyhedron
k:ℕ. ∀K:0-dim-complex. ∀x:|K|.  ∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))

Lemma: 0-dim-complex-polyhedron-decidable
k:ℕ. ∀K:0-dim-complex. ∀x,y:|K|.  Dec(x ≡ y)

Lemma: boundary-polyhedron-subtype
[k:ℕ]. ∀[n:ℕ+]. ∀[K:n-dim-complex].  (|∂(K)| ⊆|K|)

Lemma: no-retraction-case-0
[k:ℕ]. ∀[K:0-dim-complex].  (0 < ||K||  retraction(|K|;rn-prod-metric(k);|∂(K)|)))

Lemma: 1-dim-cube-endpoints
k:ℕ. ∀c:ℚCube(k).
  ((dim(c) 1 ∈ ℤ)
   (∃a,b:ℚCube(k)
       (a ≤ c
       ∧ b ≤ c
       ∧ (dim(a) 0 ∈ ℤ)
       ∧ (dim(b) 0 ∈ ℤ)
       ∧ (∀p,q:ℝ^k.  ((¬¬in-rat-cube(k;p;a))  (¬¬in-rat-cube(k;q;b))  p ≠ q))
       ∧ (∀f:ℚCube(k). (f ≤  (dim(f) 0 ∈ ℤ ((f a ∈ ℚCube(k)) ∨ (f b ∈ ℚCube(k))))))))

Lemma: no-retraction-case-1
[k:ℕ]. ∀[K:1-dim-complex].  (0 < ||K||  retraction(|K|;rn-prod-metric(k);|∂(K)|)))

Lemma: real-cube-uniform-continuity
k,n:ℕ. ∀a,b:ℕn ⟶ ℝ.
  ((∀i:ℕn. ((a i) < (b i)))
   (∀f:{f:real-cube(n;a;b) ⟶ ℝ^k| ∀x,y:real-cube(n;a;b).  (req-vec(n;x;y)  req-vec(k;f x;f y))} . ∀e:{e:ℝr0 < e} \000C.
        ∃d:ℕ+. ∀x,y:real-cube(n;a;b).  ((d(x;y) ≤ (r1/r(d)))  (d(f x;f y) ≤ e))))

Lemma: interval-cube-uniform-continuity
I:{I:Interval| icompact(I)} 
  (iproper(I)
   (∀n,k:ℕ. ∀f:{f:I^n ⟶ ℝ^k| ∀x,y:I^n.  (req-vec(n;x;y)  req-vec(k;f x;f y))} . ∀e:{e:ℝr0 < e} .
        ∃d:ℕ+. ∀x,y:I^n.  ((d(x;y) ≤ (r1/r(d)))  (d(f x;f y) ≤ e))))

Lemma: approx-fixpoint
I:{I:Interval| icompact(I)} . ∀n:ℕ. ∀f:{f:I^n ⟶ I^n| ∀a,b:I^n.  (req-vec(n;a;b)  req-vec(n;f a;f b))} .
  ((¬(∀x:I^n. x ≠ x))  (∀e:{e:ℝr0 < e} . ∃x:I^n. (d(f x;x) < e)))

Definition: rational-vec
rational-vec(n;x) ==  ∀i:ℕn. ∃d:ℕ+. ∃n:ℤ((x i) (r(n)/r(d)))

Lemma: rational-vec_wf
[n:ℕ]. ∀[x:ℝ^n].  (rational-vec(n;x) ∈ ℙ)

Definition: real-ball
B(n;r) ==  {v:ℝ^n| ||v|| ≤ r} 

Lemma: real-ball_wf
[n:ℕ]. ∀[r:ℝ].  (B(n;r) ∈ Type)

Lemma: real-ball-0
[r:{r:ℝr0 ≤ r} ]. B(0;r) ≡ Top

Lemma: real-ball-1
[r:{r:ℝr0 ≤ r} ]. B(1;r) ≡ {x:ℝ^1| 0 ∈ [-(r), r]} 

Lemma: real-ball-coordinate-range
[r:{r:ℝr0 ≤ r} ]. ∀[n:ℕ]. ∀[i:ℕn]. ∀[x:B(n;r)].  (x i ∈ [-(r), r])

Definition: ball-slice-radius
ball-slice-radius(r;t) ==  rsqrt(r^2 t^2)

Lemma: ball-slice-radius_wf
[r:{r:ℝr0 ≤ r} ]. ∀[t:{t:ℝt ∈ [-(r), r]} ].  (ball-slice-radius(r;t) ∈ {r':ℝ(r0 ≤ r') ∧ ((r'^2 t^2) r^2)} )

Definition: real-ball-slice
real-ball-slice(p;i;t) ==  λj.if j <then if i <then (j 1) else fi 

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))

Definition: real-unit-ball
B(n) ==  {v:ℝ^n| ||v|| ≤ r1} 

Lemma: real-unit-ball_wf
[n:ℕ]. (B(n) ∈ Type)

Lemma: real-unit-ball-0
B(0) ≡ Top

Definition: real-unit-sphere
S(n) ==  {v:ℝ^n 1| ||v|| r1} 

Lemma: real-unit-sphere_wf
[n:ℕ]. (S(n) ∈ Type)

Lemma: real-unit-sphere-subtype-ball
[n:ℕ]. (S(n) ⊆B(n 1))

Definition: sphere-map
sphere-map(n) ==  {f:S(n) ⟶ S(n)| ∀k:ℕ+. ∃d:ℕ+. ∀p,q:S(n).  ((d(p;q) ≤ (r1/r(d)))  (d(f p;f q) ≤ (r1/r(k))))} 

Lemma: sphere-map_wf
[n:ℕ]. (sphere-map(n) ∈ Type)

Definition: sphere-map-eq
sphere-map-eq(n;f;g) ==  ∀p:S(n). req-vec(n 1;f p;g p)

Lemma: sphere-map-eq_wf
[n:ℕ]. ∀[f,g:S(n) ⟶ S(n)].  (sphere-map-eq(n;f;g) ∈ ℙ)

Definition: const-sphere-map
const-sphere-map(p) ==  λx.p

Lemma: const-sphere-map_wf
[n:ℕ]. ∀[p:S(n)].  (const-sphere-map(p) ∈ sphere-map(n))

Definition: id-sphere-map
id-sphere-map() ==  λx.x

Lemma: id-sphere-map_wf
[n:ℕ]. (id-sphere-map() ∈ sphere-map(n))

Definition: incr-binary-seq
IBS ==  {s:ℕ ⟶ ℕ2| ∀i:ℕ((s i) ≤ (s (1 i)))} 

Lemma: incr-binary-seq_wf
IBS ∈ Type

Lemma: ibs-property
[s:IBS]. ∀[m:ℕ].  ∀[n:ℕ]. (s n) 1 ∈ ℤ supposing m ≤ supposing (s m) 1 ∈ ℤ

Definition: mkibs
mkibs(n.p[n]) ==  λn.if p[n] then else fi 

Lemma: mkibs_wf
[p:ℕ ⟶ 𝔹]. mkibs(n.p[n]) ∈ IBS supposing ∀n:ℕ((↑p[n])  (↑p[n 1]))

Definition: rless_ibs
rless_ibs(x;y) ==  λn.if (∃m∈upto(n 1).(x (m 1)) 4 <(m 1))_b then else fi 

Lemma: rless_ibs_wf
[x,y:ℝ].  (rless_ibs(x;y) ∈ IBS)

Lemma: rless_ibs_property
x,y:ℝ.
  ((x < ⇐⇒ ∃n:ℕ((rless_ibs(x;y) n) 1 ∈ ℤ))
  ∧ (∀n:ℕ
       (((rless_ibs(x;y) n) 0 ∈ ℤ)
        (((y < x) ∧ (∀m:ℕ((rless_ibs(x;y) m) 0 ∈ ℤ))) ∨ (|x y| ≤ (r(4)/r(n 1)))))))

Definition: realvec-ibs
realvec-ibs(n;p) ==  rless_ibs(r0;||p||)

Lemma: realvec-ibs_wf
[n:ℕ]. ∀[p:ℝ^n].  (realvec-ibs(n;p) ∈ IBS)

Lemma: realvec-ibs-property
k:ℕ. ∀p:ℝ^k.
  ((r0 < ||p|| ⇐⇒ ∃n:ℕ((realvec-ibs(k;p) n) 1 ∈ ℤ))
  ∧ (∀n:ℕ(((realvec-ibs(k;p) n) 0 ∈ ℤ (||p|| ≤ (r(4)/r(n 1))))))

Definition: realvec-max-ibs
realvec-max-ibs(n;p) ==  rless_ibs(r0;mdist(max-metric(n);p;λi.r0))

Lemma: realvec-max-ibs_wf
[n:ℕ]. ∀[p:ℝ^n].  (realvec-max-ibs(n;p) ∈ IBS)

Lemma: realvec-max-ibs-property
k:ℕ. ∀p:ℝ^k.
  ((r0 < mdist(max-metric(k);p;λi.r0) ⇐⇒ ∃n:ℕ((realvec-max-ibs(k;p) n) 1 ∈ ℤ))
  ∧ (∀n:ℕ(((realvec-max-ibs(k;p) n) 0 ∈ ℤ (mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(n 1))))))

Definition: remove-singularity-seq
remove-singularity-seq(k;p;f;z) ==  λn.if (realvec-ibs(k;p) =z 1) then else fi 

Lemma: remove-singularity-seq_wf
[X:Type]. ∀[k:ℕ]. ∀[p:ℝ^k]. ∀[f:{p:ℝ^k| r0 < ||p||}  ⟶ X]. ∀[z:X].  (remove-singularity-seq(k;p;f;z) ∈ ℕ ⟶ X)

Lemma: remove-singularity-seq-mcauchy
[X:Type]. ∀[d:metric(X)]. ∀[k:ℕ]. ∀[f:{p:ℝ^k| r0 < ||p||}  ⟶ X]. ∀[z:X].
  ((∃c:{c:ℝr0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
   (∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-seq(k;p;f;z) n)))

Definition: remove-singularity-max-seq
remove-singularity-max-seq(k;p;f;z) ==  λn.if (realvec-max-ibs(k;p) =z 1) then else fi 

Lemma: remove-singularity-max-seq_wf
[X:Type]. ∀[k:ℕ]. ∀[p:ℝ^k]. ∀[f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X]. ∀[z:X].
  (remove-singularity-max-seq(k;p;f;z) ∈ ℕ ⟶ X)

Lemma: remove-singularity-max-seq-mcauchy
[X:Type]. ∀[d:metric(X)]. ∀[k:ℕ]. ∀[f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X]. ∀[z:X].
  ((∃c:{c:ℝr0 ≤ c} 
     ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
       ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
   (∀[p:ℝ^k]. mcauchy(d;n.remove-singularity-max-seq(k;p;f;z) n)))

Lemma: remove-singularity
[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < ||p||}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝr0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
     mcomplete(X with d)
     (∃g:ℝ^k ⟶ X. ((∀p:ℝ^k. (req-vec(k;p;λi.r0)  p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < ||p||} p ≡ p))))

Lemma: remove-singularity-mfun
[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < ||p||}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝr0 ≤ c} . ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < ||p||} .  ((||p|| ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
     mcomplete(X with d)
     (∃g:ℝ^k ⟶ X
         ((∀p:ℝ^k. (req-vec(k;p;λi.r0)  p ≡ z))
         ∧ (∀p:{p:ℝ^k| r0 < ||p||} p ≡ p)
         ∧ (f:FUN({p:ℝ^k| r0 < ||p||} ;X)  g:FUN(ℝ^k;X)))))

Lemma: remove-singularity-max
[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝr0 ≤ c} 
       ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
         ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
     mcomplete(X with d)
     (∃g:ℝ^k ⟶ X
         ((∀p:ℝ^k. (req-vec(k;p;λi.r0)  p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} p ≡ p))))

Lemma: remove-singularity-max-mfun
[X:Type]. ∀[d:metric(X)].
  ∀k:ℕ. ∀f:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)}  ⟶ X. ∀z:X.
    ((∃c:{c:ℝr0 ≤ c} 
       ∀m:ℕ+. ∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} .
         ((mdist(max-metric(k);p;λi.r0) ≤ (r(4)/r(m)))  (mdist(d;f p;z) ≤ (c/r(m)))))
     mcomplete(X with d)
     (∃g:ℝ^k ⟶ X
         (((∀p:ℝ^k. (req-vec(k;p;λi.r0)  p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} p ≡ p))
         ∧ (f:FUN({p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} ;X)  g:FUN(ℝ^k;X)))))

Lemma: rless-ibs
x,y:ℝ.
  ∃s:IBS
   ((x < ⇐⇒ ∃n:ℕ((s n) 1 ∈ ℤ))
   ∧ (∀n:ℕ(((s n) 0 ∈ ℤ (((y < x) ∧ (∀m:ℕ((s m) 0 ∈ ℤ))) ∨ (|x y| ≤ (r(4)/r(n 1)))))))

Lemma: unit-cube-to-unit-ball
n:ℕ+
  ∃g:ℝ^n ⟶ ℝ^n
   ((∀p:ℝ^n. (req-vec(n;p;λi.r0)  p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < ||p||} p ≡ p.(mdist(max-metric(n);λi.r0;p)/||p||)*p) p)
   ∧ (g ∈ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1}  ⟶ {q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} )
   ∧ g:FUN(ℝ^n;ℝ^n))

Lemma: unit-ball-to-unit-cube
n:ℕ+
  ∃g:ℝ^n ⟶ ℝ^n
   ((∀p:ℝ^n. (req-vec(n;p;λi.r0)  p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} p ≡ p.(||p||/mdist(max-metric(n);p;λi.r0))*p) p)
   ∧ (g ∈ {p:ℝ^n| ||p|| ≤ r1}  ⟶ {q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} )
   ∧ g:FUN(ℝ^n;ℝ^n)
   ∧ (∀x,y:{p:ℝ^n| ||p|| ≤ r1} .  (mdist(max-metric(n);g x;g y) ≤ (r((2 n) 1) mdist(rn-metric(n);x;y)))))

Lemma: unit-balls-homeomorphic+
n:ℕ+homeomorphic+({q:ℝ^n| mdist(rn-metric(n);λi.r0;q) ≤ r1} ;rn-metric(n);{q:ℝ^n| mdist(max-metric(n);λi.r0;q) ≤ r1} \000C;max-metric(n))

Lemma: unit-balls-homeomorphic+-2
n:ℕ+homeomorphic+(B(n;r1);rn-metric(n);[r(-1), r1]^n;max-metric(n))

Lemma: real-ball-uniform-continuity
k:ℕ. ∀n:ℕ+. ∀f:{f:B(n;r1) ⟶ ℝ^k| ∀x,y:B(n;r1).  (req-vec(n;x;y)  req-vec(k;f x;f y))} . ∀e:{e:ℝr0 < e} .
  ∃d:ℕ+. ∀x,y:B(n;r1).  ((d(x;y) ≤ (r1/r(d)))  (d(f x;f y) ≤ e))

Lemma: sphere-map-from-ball-map
[n:ℕ]. ∀[g:{g:B(n 1) ⟶ B(n 1)| 
             (∀x,y:B(n 1).  (req-vec(n 1;x;y)  req-vec(n 1;g x;g y))) ∧ (∀x:B(n 1). (||g x|| r1))} ].
  (g ∈ sphere-map(n))

Definition: unit-ball-approx
unit-ball-approx(n;k) ==  {x:ℕn ⟶ {-k..k 1-}| Σ((x i) (x i) i < n) ≤ (k k)} 

Lemma: unit-ball-approx_wf
[n,k:ℕ].  (unit-ball-approx(n;k) ∈ Type)

Lemma: unit-ball-approx0
[k:ℕ]. unit-ball-approx(0;k) ≡ Top

Lemma: unit-ball-approx-subtype
[k,n,m:ℕ].  unit-ball-approx(m;k) ⊆unit-ball-approx(n;k) supposing n ≤ m

Definition: extend-approx-ball
extend-approx-ball(n;p;z) ==  λi.if i <then else fi 

Lemma: extend-approx-ball_wf
[k,n:ℕ]. ∀[p:unit-ball-approx(n;k)]. ∀[z:{-k..k 1-}].
  extend-approx-ball(n;p;z) ∈ unit-ball-approx(n 1;k) supposing ((p i) (p i) i < n) (z z)) ≤ (k k)

Lemma: unit-ball-approxn
[k:ℕ]. ∀[n:ℕ+].
  unit-ball-approx(n;k) ≡ {f:ℕn ⟶ {-k..k 1-}| 
                           ∃q:unit-ball-approx(n 1;k)
                            ∃z:{-k..k 1-}
                             (((Σ((q i) (q i) i < 1) (z z)) ≤ (k k))
                             ∧ (∀i:ℕ1. ((f i) (q i) ∈ ℤ))
                             ∧ ((f (n 1)) z ∈ ℤ))} 

Lemma: decidable__exists-unit-ball-approx-1
k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∃p:unit-ball-approx(n;k). P[p]))

Lemma: decidable__exists-unit-ball-approx-1-ext
k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∃p:unit-ball-approx(n;k). P[p]))

Definition: unit-ball-ex-decider
unit-ball-ex-decider(k;n) ==
  primrec(n;λ%.case Ax of inl(%) => inl <Ax, %> inr(%6) => inr %.Ax) ;
          λi,x,%2. case 
                        p.eval i' -k in
                            eval j' in
                              letrec G(x)=if (x) < (j')
                                             then if (k k) < ((p i) (p i) i < (i 1) 1) (x x))
                                                     then (x 1)
                                                     else case %2 i@0.if (i@0) < ((i 1) 1)  then i@0  else x)
                                                           of inl(x1) =>
                                                           inl <x, <λ%.Ax, Ax, Ax>x1>
                                                           inr(x1) =>
                                                           (x 1)
                                             else (inr x.Ax) in
                               G(i'))
                   of inl(%3) =>
                   inl let p,z,%6,%7 %3 
                       in <λi@0.if (i@0) < ((i 1) 1)  then i@0  else z, %7>  
                   inr(%4) =>
                   inr %.Ax) )

Lemma: unit-ball-ex-decider_wf
k,n:ℕ.
  (unit-ball-ex-decider(k;n) ∈ ∀[P:unit-ball-approx(n;k) ⟶ ℙ]
                                 ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∃p:unit-ball-approx(n;k). P[p])))

Lemma: decidable__exists-unit-ball-approx
k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∃p:unit-ball-approx(n;k). P[p]))

Lemma: decidable__all-unit-ball-approx
k,n:ℕ.  ∀[P:unit-ball-approx(n;k) ⟶ ℙ]. ((∀p:unit-ball-approx(n;k). Dec(P[p]))  Dec(∀p:unit-ball-approx(n;k). P[p]))

Definition: approx-ball-to-ball
approx-ball-to-ball(k;p) ==  λi.(r(p i))/k

Lemma: approx-ball-to-ball_wf
[n:ℕ]. ∀[k:ℕ+]. ∀[p:unit-ball-approx(n;k)].  (approx-ball-to-ball(k;p) ∈ B(n))

Lemma: real-unit-ball-totally-bounded1
n:ℕ. ∀k:ℕ+. ∀p:B(n).  ∃q:unit-ball-approx(n;k n). (d(p;approx-ball-to-ball(k n;q)) ≤ (r1/r(k)))

Lemma: real-unit-ball-totally-bounded
n:ℕ. ∀k:ℕ+.  (∃L:{p:B(n)| rational-vec(n;p)}  List [(∀p:B(n). ∃i:ℕ||L||. (d(p;L[i]) ≤ (r1/r(k))))])

Lemma: approx-fixpoint-unit-ball-0
n:ℕ+. ∀f:{f:B(n) ⟶ B(n)| 
           (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
           ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃t:B(n) ⟶ 𝔹
   ((∀p:B(n). ((↑(t p))  (↓d(f p;p) < e))) ∧ (↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q)))))

Lemma: approx-fixpoint-unit-ball-0-ext
n:ℕ+. ∀f:{f:B(n) ⟶ B(n)| 
           (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
           ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃t:B(n) ⟶ 𝔹
   ((∀p:B(n). ((↑(t p))  (↓d(f p;p) < e))) ∧ (↓∃k:ℕ+. ∃q:unit-ball-approx(n;k). (↑(t approx-ball-to-ball(k;q)))))

Lemma: approx-fixpoint-unit-ball-1
n:ℕ. ∀f:{f:B(n) ⟶ B(n)| 
          (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
          ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃p:B(n). (↓d(f p;p) < e)

Lemma: approx-fixpoint-unit-ball-1-ext
n:ℕ. ∀f:{f:B(n) ⟶ B(n)| 
          (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
          ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃p:B(n). (↓d(f p;p) < e)

Definition: find-approx-fp
find-approx-fp(n;f;e) ==
  if n=0
  then <Ax, Ax>
  else let mu-ge(λm.(unit-ball-ex-decider(m;n) 
                         q.case isr(rless-case((r(2) e/r(3));e;(((rlessw(((r(2) e/r(3)) r(3)) rinv(r(3));(e
                                  r(3))
                                  rinv(r(3)))
                                  20)
                                  1)
                                  20)
                                  1;d(f 
                                        i.eval in
                                            λn.if (k) < (0)
                                                  then -((r(q i) (2 n)) ÷ (-2) k)
                                                  else ((r(q i) (2 n)) ÷ k));λi.eval in
                                                                                      λn.if (k) < (0)
                                                                                            then -((r(q i) 
                                                                                                    (2 n)) ÷ (-2) k)
                                                                                            else ((r(q i) (2 n)) ÷ 2
                                                                                                 k))))
                              of inl(x) =>
                              inl x
                              inr(x) =>
                              inr x.Ax) ));1) in
           case unit-ball-ex-decider(k;n) 
                q.case isr(rless-case((r(2) e/r(3));e;(((rlessw(((r(2) e/r(3)) r(3)) rinv(r(3));(e r(3))
                         rinv(r(3)))
                         20)
                         1)
                         20)
                         1;d(f 
                               i.eval in
                                   λn.if (k) < (0)
                                         then -((r(q i) (2 n)) ÷ (-2) k)
                                         else ((r(q i) (2 n)) ÷ k));λi.eval in
                                                                             λn.if (k) < (0)
                                                                                   then -((r(q i) (2 n)) ÷ (-2) k)
                                                                                   else ((r(q i) (2 n)) ÷ k))))
                     of inl(x) =>
                     inl x
                     inr(x) =>
                     inr x.Ax) )
            of inl(x) =>
            let q,%8 
            in <λi.eval in
                   λn.if (k) < (0)  then -((r(q i) (2 n)) ÷ (-2) k)  else ((r(q i) (2 n)) ÷ k)
               Ax
               >
            inr(x) =>
            let q,%8 fix((λx.x)) 
            in <λi.eval in
                   λn.if (k) < (0)  then -((r(q i) (2 n)) ÷ (-2) k)  else ((r(q i) (2 n)) ÷ k)
               Ax
               >

Lemma: find-approx-fp_wf
n:ℕ. ∀f:{f:B(n) ⟶ B(n)| 
          (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
          ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  (find-approx-fp(n;f;e) ∈ ∃p:B(n). (↓d(f p;p) < e))

Lemma: find-approx-fixpoint-unit-ball
n:ℕ. ∀f:{f:B(n) ⟶ B(n)| 
          (∀e:{e:ℝr0 < e} . ∃del:{del:ℝr0 < del} . ∀x,y:B(n).  ((d(x;y) < del)  (d(f x;f y) < e)))
          ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝr0 < e} .
  ∃p:B(n). (↓d(f p;p) < e)

Lemma: approx-fixpoint-unit-ball-2
n:ℕ. ∀f:{f:B(n) ⟶ B(n)| (∀x,y:B(n).  (req-vec(n;x;y)  req-vec(n;f x;f y))) ∧ (∀x:B(n). x ≠ x))} . ∀e:{e:ℝ
                                                                                                             r0 < e} .
  ∃p:B(n). (↓d(f p;p) < e)

Definition: BrouwerFPT
BrouwerFPT(n) ==
  ∀f:{f:B(n) ⟶ B(n)| ∀x,y:B(n).  (req-vec(n;x;y)  req-vec(n;f x;f y))} . ∀e:{e:ℝr0 < e} .  ∃p:B(n). (↓d(f p;p) < e)

Lemma: BrouwerFPT_wf
[n:ℕ]. (BrouwerFPT(n) ∈ ℙ)

Definition: NoBallRetraction
NoBallRetraction(n) ==
  ¬(∃g:B(n) ⟶ B(n)
     ((∀x,y:B(n).  (req-vec(n;x;y)  req-vec(n;g x;g y)))
     ∧ (∀x:B(n). (||g x|| r1))
     ∧ (∀x:B(n). ((||x|| r1)  req-vec(n;g x;x)))))

Lemma: NoBallRetraction_wf
[n:ℕ]. (NoBallRetraction(n) ∈ ℙ)

Lemma: NoBallRetraction-implies-BrouwerFPT
n:ℕBrouwerFPT(n) supposing NoBallRetraction(n)

Definition: IdNotHomotopicConst
IdNotHomotopicConst(n) ==
  ¬(∃h:{t:ℝt ∈ [r0, r1]}  ⟶ S(n) ⟶ S(n)
     ((∀p:S(n). req-vec(n 1;h r1 p;p))
     ∧ (∃q:S(n). ∀p:S(n). req-vec(n 1;h r0 p;q))
     ∧ (∀t1,t2:{t:ℝt ∈ [r0, r1]} . ∀p1,p2:S(n).
          ((t1 t2)  req-vec(n 1;p1;p2)  req-vec(n 1;h t1 p1;h t2 p2)))))

Lemma: IdNotHomotopicConst_wf
[n:ℕ]. (IdNotHomotopicConst(n) ∈ ℙ)

Lemma: IdNotHomotopicConst-implies-BrowerFPT
n:ℕBrouwerFPT(n 1) supposing IdNotHomotopicConst(n)

Definition: DegreeExists
DegreeExists(n) ==
  ∃ind:sphere-map(n) ⟶ ℤ
   ((∀f,g:sphere-map(n).  (sphere-map-eq(n;f;g)  ((ind f) (ind g) ∈ ℤ)))
   ∧ (∀p:S(n). ((ind const-sphere-map(p)) 0 ∈ ℤ))
   ∧ ((ind id-sphere-map()) 1 ∈ ℤ))

Lemma: DegreeExists_wf
[n:ℕ]. (DegreeExists(n) ∈ ℙ)

Lemma: Degree-implies-BrowerFPT
n:ℕBrouwerFPT(n 1) supposing ¬¬DegreeExists(n)

Lemma: Degree-implies-BrowerFPT-ext
n:ℕBrouwerFPT(n 1) supposing ¬¬DegreeExists(n)

Definition: std-simplex
Δ(n) ==  {v:ℝ^n 1| (∀i:ℕ1. (r0 ≤ (v i))) ∧ {v 0≤i≤n} r1)} 

Lemma: std-simplex_wf
[n:ℤ]. (n) ∈ Type)

Lemma: std-simplex-void
[n:ℤ]. ¬Δ(n) supposing n < 0

Lemma: std-simplex-properties
[n:ℕ]. ∀[v:Δ(n)].  ((∀i:ℕ1. (r0 ≤ (v i))) ∧ {v 0≤i≤n} r1))

Definition: simplex-metric
simplex-metric(n) ==  rn-metric(n 1)

Lemma: simplex-metric_wf
[n:ℤ]. (simplex-metric(n) ∈ metric(Δ(n)))

Definition: simplex-face
simplex-face(v;i) ==  λj.if j <then if i <then (j 1) else r0 fi 

Lemma: simplex-face_wf
[n:ℤ]. ∀[v:Δ(n)]. ∀[i:ℕ2].  (simplex-face(v;i) ∈ Δ(n 1))

Lemma: simplex-face-face
[n:ℤ]. ∀[v:Δ(n)]. ∀[i,j:ℕ2].
  simplex-face(simplex-face(v;i);j) simplex-face(simplex-face(v;j);i 1) ∈ Δ(n 2) supposing j ≤ i

Definition: real-cube
real-cube(k) ==  ℝ^k × ℝ^k

Lemma: real-cube_wf
[k:ℕ]. (real-cube(k) ∈ Type)

Definition: req-cube
req-cube(k;c1;c2) ==  req-vec(k;fst(c1);fst(c2)) ∧ req-vec(k;snd(c1);snd(c2))

Lemma: req-cube_wf
[k,k:ℕ]. ∀[c1,c2:real-cube(k)].  (req-cube(k;c1;c2) ∈ ℙ)

Definition: cube-upper
c+ ==  snd(c)

Lemma: cube-upper_wf
[k:ℕ]. ∀[c:real-cube(k)].  (c+ ∈ ℝ^k)

Definition: cube-lower
c- ==  fst(c)

Lemma: cube-lower_wf
[k:ℕ]. ∀[c:real-cube(k)].  (c- ∈ ℝ^k)

Definition: in-real-cube
p ∈ ==  ∀i:ℕk. (((c- i) ≤ (p i)) ∧ ((p i) ≤ (c+ i)))

Lemma: in-real-cube_wf
[k:ℕ]. ∀[p:ℝ^k]. ∀[c:real-cube(k)].  (p ∈ c ∈ ℙ)

Definition: real-cube-sep
c1 c2 ==  ∃i:ℕk. (((c1+ i) < (c2- i)) ∨ ((c2+ i) < (c1- i)))

Lemma: real-cube-sep_wf
[k:ℕ]. ∀[c1,c2:real-cube(k)].  (c1 c2 ∈ ℙ)

Lemma: real-cube-sep-disjoint
[k:ℕ]. ∀[c1,c2:real-cube(k)].  (c1 c2  (∀p:ℝ^k. (p ∈ c1 ∧ p ∈ c2))))

Definition: adjacent-cubes
adjacent-cubes(k;c1;c2) ==
  ∃i:ℕk
   ((∀j:ℕk. ((¬(j i ∈ ℤ))  (((c1- j) (c2- j)) ∧ ((c1+ j) (c2+ j)))))
   ∧ (((c1- i) (c2+ i)) ∨ ((c2- i) (c1+ i))))

Lemma: adjacent-cubes_wf
[k:ℕ]. ∀[c1,c2:real-cube(k)].  (adjacent-cubes(k;c1;c2) ∈ ℙ)

Definition: real-cube-complex
RealCubeComplex(k) ==
  T:Type
  × finite(T)
  × f:T ⟶ real-cube(k)
  × (∀t1,t2:T.  ((¬(t1 t2 ∈ T))  (adjacent-cubes(k;f t1;f t2) ∨ t1 t2)))

Lemma: real-cube-complex_wf
[k:ℕ]. (RealCubeComplex(k) ∈ 𝕌')

Definition: in-cube-complex
in-cube-complex(k;p;cc) ==  let T,_,f,_ cc in ∃t:T. p ∈ t  

Lemma: in-cube-complex_wf
[k:ℕ]. ∀[p:ℝ^k]. ∀[cc:RealCubeComplex(k)].  (in-cube-complex(k;p;cc) ∈ ℙ)

Definition: cube-complex-space
|cc| ==  {p:ℝ^k| in-cube-complex(k;p;cc)} 

Lemma: cube-complex-space_wf
[k:ℕ]. ∀[cc:RealCubeComplex(k)].  (|cc| ∈ Type)

Definition: cube-face
cube-face(i;up;c) ==
  let l,u 
  in if up then <λj.if (j =z i) then else fi u> else <l, λj.if (j =z i) then else fi > fi 

Lemma: cube-face_wf
[k:ℕ]. ∀[i:ℕk]. ∀[up:𝔹]. ∀[c:real-cube(k)].  (cube-face(i;up;c) ∈ real-cube(k))

Definition: sub-cube
sub-cube(up;c) ==
  let l,u 
  in <λi.if up then ravg(l i;u i) else fi , λi.if up then else ravg(l i;u i) fi >

Lemma: sub-cube_wf
[k:ℕ]. ∀[up:ℕk ⟶ 𝔹]. ∀[c:real-cube(k)].  (sub-cube(up;c) ∈ real-cube(k))

Definition: sub-cube-complex
sub-cube-complex(k;L) ==  concat(map(λc.sub-cubes(k; c);L))



Home Index