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, b 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, b 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, b i])) ∧ (¬(∀i:ℕn. (p i ∈ (a i, b 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≤k - 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) = 0 \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 = I 
  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 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| ⊆r |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)| ⊆r |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)| ⊆r |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 ≤ c 
⇒ (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. f 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| x 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 <z i then p j if i <z j then p (j - 1) else t 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) ⊆r 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 ≤ n supposing (s m) = 1 ∈ ℤ
Definition: mkibs
mkibs(n.p[n]) ==  λn.if p[n] then 1 else 0 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 <z y (m + 1))_b then 1 else 0 fi 
Lemma: rless_ibs_wf
∀[x,y:ℝ].  (rless_ibs(x;y) ∈ IBS)
Lemma: rless_ibs_property
∀x,y:ℝ.
  ((x < y 
⇐⇒ ∃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) n =z 1) then f p else z 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) n =z 1) then f p else z 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) 
⇒ g p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f 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) 
⇒ g p ≡ z))
         ∧ (∀p:{p:ℝ^k| r0 < ||p||} . g p ≡ f 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) 
⇒ g p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f 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) 
⇒ g p ≡ z)) ∧ (∀p:{p:ℝ^k| r0 < mdist(max-metric(k);p;λi.r0)} . g p ≡ f 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 < y 
⇐⇒ ∃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) 
⇒ g p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < ||p||} . g 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) 
⇒ g p ≡ λi.r0))
   ∧ (∀p:{p:ℝ^n| r0 < mdist(max-metric(n);λi.r0;p)} . g 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) ⊆r unit-ball-approx(n;k) supposing n ≤ m
Definition: extend-approx-ball
extend-approx-ball(n;p;z) ==  λi.if i <z n then p i else z 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 < n - 1) + (z * z)) ≤ (k * k))
                             ∧ (∀i:ℕn - 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 x 
                        (λp.eval i' = -k in
                            eval j' = k + 1 in
                              letrec G(x)=if (x) < (j')
                                             then if (k * k) < (Σ((p i) * (p i) | i < (i + 1) - 1) + (x * x))
                                                     then G (x + 1)
                                                     else case %2 (λi@0.if (i@0) < ((i + 1) - 1)  then p i@0  else x)
                                                           of inl(x1) =>
                                                           inl <x, <λ%.Ax, Ax, Ax>, x1>
                                                           | inr(x1) =>
                                                           G (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 p 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 * 8 * n). (d(p;approx-ball-to-ball(k * 8 * 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). f 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). f 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). f 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). f 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 k = 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 k = m in
                                            λn.if (k) < (0)
                                                  then -((r(q i) (2 * n)) ÷ (-2) * k)
                                                  else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = m 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 k = k in
                                   λn.if (k) < (0)
                                         then -((r(q i) (2 * n)) ÷ (-2) * k)
                                         else ((r(q i) (2 * n)) ÷ 2 * k));λi.eval k = k 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) )
            of inl(x) =>
            let q,%8 = x 
            in <λi.eval k = k in
                   λn.if (k) < (0)  then -((r(q i) (2 * n)) ÷ (-2) * k)  else ((r(q i) (2 * n)) ÷ 2 * k)
               , Ax
               >
            | inr(x) =>
            let q,%8 = fix((λx.x)) 
            in <λi.eval k = k in
                   λn.if (k) < (0)  then -((r(q i) (2 * n)) ÷ (-2) * k)  else ((r(q i) (2 * n)) ÷ 2 * 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). f 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). f 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). f 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:ℕn + 1. (r0 ≤ (v i))) ∧ (Σ{v i | 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:ℕn + 1. (r0 ≤ (v i))) ∧ (Σ{v i | 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 <z i then v j if i <z j then v (j - 1) else r0 fi 
Lemma: simplex-face_wf
∀[n:ℤ]. ∀[v:Δ(n)]. ∀[i:ℕn + 2].  (simplex-face(v;i) ∈ Δ(n + 1))
Lemma: simplex-face-face
∀[n:ℤ]. ∀[v:Δ(n)]. ∀[i,j:ℕn + 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 ∈ c ==  ∀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) ∨ f t1 # f 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 ∈ f 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 = c 
  in if up then <λj.if (j =z i) then u j else l j fi , u> else <l, λj.if (j =z i) then l j else u j 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 = c 
  in <λi.if up i then ravg(l i;u i) else l i fi , λi.if up i then u i 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