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