The book "Classical Geometries in Modern Contexts", by Walter Benz,
subtitled "Geometry of Real Inner Product Spaces", seems to use mainly
constructive methods.
To make it fully constructive, we introduce the needed separation
primitives into the definition of a real inner product space.
So far, we have proved such theorems as
implies-isometry which is Schroeder and Benz's
version of the Benedick & Quarles theorem. It is fully constructive.
.⋅
Definition: real-vector-space
RealVectorSpace ==
SeparationSpace
"0":Point(self)
"+":{f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). f x (f y z) ≡ f (f x y) z) ∧ (∀x,y:Point(self). f x y ≡ f y x)}
"+sep":∀x,x',y,y':Point(self). (self."+" x y # self."+" x' y' ⇒ (x # x' ∨ y # y'))
"*":{m:ℝ ⟶ Point(self) ⟶ Point(self)|
(∀a:ℝ. ∀x,y:Point(self). m a (self."+" x y) ≡ self."+" (m a x) (m a y))
∧ (∀x:Point(self)
(m r1 x ≡ x
∧ m r0 x ≡ self."0"
∧ (∀a,b:ℝ. m a (m b x) ≡ m (a * b) x)
∧ (∀a,b:ℝ. m (a + b) x ≡ self."+" (m a x) (m b x))))}
"*sep":∀a,b:ℝ. ∀x,y:Point(self). (self."*" a x # self."*" b y ⇒ (a ≠ b ∨ x # y))
Lemma: real-vector-space_wf
RealVectorSpace ∈ 𝕌'
Lemma: real-vector-space_subtype1
RealVectorSpace ⊆r SeparationSpace
Definition: mk-real-vector-space
ss=ss;0=z;+=p;*=m;+sep=psep;*sep=msep == ss["0" := z]["+" := p]["*" := m]["+sep" := psep]["*sep" := msep]
Lemma: mk-real-vector-space_wf
∀[self:SeparationSpace]. ∀[z:Point(self)]. ∀[p:{f:Point(self) ⟶ Point(self) ⟶ Point(self)|
(∀x,y,z:Point(self). f x (f y z) ≡ f (f x y) z)
∧ (∀x,y:Point(self). f x y ≡ f y x)} ].
∀[m:{m:ℝ ⟶ Point(self) ⟶ Point(self)|
(∀a:ℝ. ∀x,y:Point(self). m a (p x y) ≡ p (m a x) (m a y))
∧ (∀x:Point(self)
(m r1 x ≡ x
∧ m r0 x ≡ z
∧ (∀a,b:ℝ. m a (m b x) ≡ m (a * b) x)
∧ (∀a,b:ℝ. m (a + b) x ≡ p (m a x) (m b x))))} ]. ∀[psep:∀x,x',y,y':Point(self).
(p x y # p x' y' ⇒ (x # x' ∨ y # y'))].
∀[msep:∀a,b:ℝ. ∀x,y:Point(self). (m a x # m b y ⇒ (a ≠ b ∨ x # y))].
(ss=self;
0=z;
+=p;
*=m;
+sep=psep;
*sep=msep ∈ RealVectorSpace)
Definition: rv-0
0 == rv."0"
Lemma: rv-0_wf
∀[rv:RealVectorSpace]. (0 ∈ Point(rv))
Definition: rv-add
x + y == rv."+" x y
Lemma: rv-add_wf
∀[rv:RealVectorSpace]. ∀[x,y:Point(rv)]. (x + y ∈ Point(rv))
Lemma: rv-add-sep
∀rv:RealVectorSpace. ∀x,x',y,y':Point(rv). (x + y # x' + y' ⇒ (x # x' ∨ y # y'))
Lemma: rv-add-sep1
∀rv:RealVectorSpace. ∀x,x',y:Point(rv). (x + y # x' + y ⇒ x # x')
Lemma: rv-add-sep2
∀rv:RealVectorSpace. ∀x,x',y:Point(rv). (y + x # y + x' ⇒ x # x')
Lemma: rv-add_functionality
∀[rv:RealVectorSpace]. ∀[x,y,x',y':Point(rv)]. (x + y ≡ x' + y') supposing (y ≡ y' and x ≡ x')
Lemma: rv-add-assoc
∀[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)]. x + y + z ≡ x + y + z
Lemma: rv-add-comm
∀[rv:RealVectorSpace]. ∀[x,y:Point(rv)]. x + y ≡ y + x
Lemma: rv-add-swap
∀[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)]. x + y + z ≡ x + z + y
Definition: rv-mul
a*x == rv."*" a x
Lemma: rv-mul_wf
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x:Point(rv)]. (a*x ∈ Point(rv))
Lemma: rv-mul-sep
∀rv:RealVectorSpace. ∀a,b:ℝ. ∀x,y:Point(rv). (a*x # b*y ⇒ (a ≠ b ∨ x # y))
Lemma: rv-mul-sep1
∀rv:RealVectorSpace. ∀a,b:ℝ. ∀y:Point(rv). (a*y # b*y ⇒ a ≠ b)
Lemma: rv-mul-sep2
∀rv:RealVectorSpace. ∀a:ℝ. ∀x,y:Point(rv). (a*x # a*y ⇒ x # y)
Lemma: rv-mul1
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. r1*x ≡ x
Lemma: rv-mul0
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. r0*x ≡ 0
Lemma: rv-mul_functionality
∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x,x':Point(rv)]. (a*x ≡ b*x') supposing (x ≡ x' and (a = b))
Lemma: rv-mul-linear
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)]. a*x + y ≡ a*x + a*y
Lemma: rv-mul-mul
∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)]. a*b*x ≡ a * b*x
Lemma: rv-mul-add
∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)]. a*x + b*x ≡ a + b*x
Lemma: rv-mul-add-alt
∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x,u:Point(rv)]. u + a*x + b*x ≡ u + a + b*x
Lemma: rv-mul-add-1
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x:Point(rv)]. a*x + x ≡ a + r1*x
Lemma: rv-mul-add-1-alt
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,u:Point(rv)]. u + a*x + x ≡ u + a + r1*x
Lemma: rv-mul-1-add
∀[rv:RealVectorSpace]. ∀[b:ℝ]. ∀[x:Point(rv)]. x + b*x ≡ r1 + b*x
Lemma: rv-mul-1-add-alt
∀[rv:RealVectorSpace]. ∀[b:ℝ]. ∀[x,u:Point(rv)]. u + x + b*x ≡ u + r1 + b*x
Lemma: rv-mul-0
∀[rv:RealVectorSpace]. ∀[a:ℝ]. a*0 ≡ 0
Definition: rv-minus
-x == r(-1)*x
Lemma: rv-minus_wf
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. (-x ∈ Point(rv))
Lemma: rv-minus_functionality
∀[rv:RealVectorSpace]. ∀[x,x':Point(rv)]. -x ≡ -x' supposing x ≡ x'
Lemma: rv-add-minus
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. -x + x ≡ 0
Lemma: rv-add-minus2
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. x + -x ≡ 0
Lemma: rv-add-0
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. 0 + x ≡ x
Lemma: rv-0-add
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. x + 0 ≡ x
Lemma: rv-add-cancel-left
∀[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)]. uiff(x + y ≡ x + z;y ≡ z)
Lemma: rv-add-cancel-right
∀[rv:RealVectorSpace]. ∀[x,y,z:Point(rv)]. uiff(y + x ≡ z + x;y ≡ z)
Lemma: rv-mul-cancel
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)]. uiff(a*x ≡ a*y;x ≡ y) supposing a ≠ r0
Definition: inner-product-space
InnerProductSpace ==
RealVectorSpace
"ip":{ip:Point(self) ⟶ Point(self) ⟶ ℝ|
(∀x1,x2,y1,y2:Point(self). (x1 ≡ x2 ⇒ y1 ≡ y2 ⇒ ((ip x1 y1) = (ip x2 y2))))
∧ (∀x,y:Point(self). ((ip x y) = (ip y x)))
∧ (∀x,y,z:Point(self). ((ip x + y z) = ((ip x z) + (ip y z))))
∧ (∀a:ℝ. ∀x,y:Point(self). ((ip a*x y) = (a * (ip x y))))}
"positive":∀x:Point(self). (x # 0 ⇐⇒ r0 < (self."ip" x x))
"perp":∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((self."ip" x y) = r0))))
Lemma: inner-product-space_wf
InnerProductSpace ∈ 𝕌'
Lemma: inner-product-space_subtype
InnerProductSpace ⊆r RealVectorSpace
Definition: mk-inner-product-space
vs=vs;ip=ip;positive=pos;perp=perp == vs["ip" := ip]["positive" := pos]["perp" := perp]
Lemma: mk-inner-product-space_wf
∀[self:RealVectorSpace]. ∀[ip:{ip:Point(self) ⟶ Point(self) ⟶ ℝ|
(∀x1,x2,y1,y2:Point(self). (x1 ≡ x2 ⇒ y1 ≡ y2 ⇒ ((ip x1 y1) = (ip x2 y2))))
∧ (∀x,y:Point(self). ((ip x y) = (ip y x)))
∧ (∀x,y,z:Point(self). ((ip x + y z) = ((ip x z) + (ip y z))))
∧ (∀a:ℝ. ∀x,y:Point(self). ((ip a*x y) = (a * (ip x y))))} ]. ∀[pos:∀x:Point(self)
(x # 0
⇐⇒ r0 < (ip x
x))].
∀[perp:∀x:Point(self). (x # 0 ⇒ (∃y:Point(self). (y # 0 ∧ ((ip x y) = r0))))].
(vs=self;
ip=ip;
positive=pos;
perp=perp ∈ InnerProductSpace)
Definition: rn-ss
sepℝ^n == Point=ℝ^n #=λx,y. x ≠ y cotrans=TERMOF{real-vec-sep-cases-alt:o, 1:l} n
Lemma: rn-ss_wf
∀[n:ℕ]. (sepℝ^n ∈ SeparationSpace)
Definition: rv-n
vecℝ^n ==
ss=sepℝ^n;
0=λi.r0;
+=λx,y. x + y;
*=λa,y. a*y;
+sep=TERMOF{real-vec-sep-add:o, 1:l} n;
*sep=TERMOF{real-vec-sep-mul:o, 1:l} n
Lemma: rv-n_wf
∀[n:ℕ]. (vecℝ^n ∈ RealVectorSpace)
Definition: rn-ip
ipℝ^n == vs=vecℝ^n;ip=λx,y. x⋅y;positive=TERMOF{real-vec-sep-0-iff:o, 1:l} n;perp=TERMOF{real-vec-perp-exists:o, 1:l} n
Lemma: rn-ip_wf
∀[n:{2...}]. (ipℝ^n ∈ InnerProductSpace)
Definition: rv-ip
x ⋅ y == rv."ip" x y
Lemma: rv-ip_wf
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (x ⋅ y ∈ ℝ)
Lemma: rv-ip_functionality
∀[rv:InnerProductSpace]. ∀[x1,x2,y1,y2:Point(rv)]. (x1 ⋅ y1 = x2 ⋅ y2) supposing (y1 ≡ y2 and x1 ≡ x2)
Lemma: rv-ip-symmetry
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (x ⋅ y = y ⋅ x)
Lemma: rv-ip-add
∀[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)]. (x + y ⋅ z = (x ⋅ z + y ⋅ z))
Lemma: rv-ip-add2
∀[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)]. (z ⋅ x + y = (z ⋅ x + z ⋅ y))
Lemma: rv-ip-mul
∀[rv:InnerProductSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)]. (a*x ⋅ y = (a * x ⋅ y))
Lemma: rv-ip-mul2
∀[rv:InnerProductSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)]. (y ⋅ a*x = (a * y ⋅ x))
Lemma: rv-ip-positive
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇐⇒ r0 < x^2)
Lemma: rv-ip0
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (x ⋅ 0 = r0)
Lemma: rv-0ip
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (0 ⋅ x = r0)
Lemma: rv-ip-nonneg
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (r0 ≤ x^2)
Lemma: rsqrt-1-plus-ip-positive
∀rv:InnerProductSpace. ∀h:Point(rv). (r0 < rsqrt(r1 + h^2))
Lemma: rv-ip-minus
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (-x ⋅ y = -(x ⋅ y))
Lemma: rv-ip-minus2
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (x ⋅ -y = -(x ⋅ y))
Definition: rv-sub
x - y == x + -y
Lemma: rv-sub_wf
∀[rv:RealVectorSpace]. ∀[x,y:Point(rv)]. (x - y ∈ Point(rv))
Lemma: rv-sub_functionality
∀[rv:RealVectorSpace]. ∀[x,y,x',y':Point(rv)]. (x - y ≡ x' - y') supposing (y ≡ y' and x ≡ x')
Lemma: rv-sub-is-zero
∀[rv:RealVectorSpace]. ∀[x,y:Point(rv)]. uiff(x - y ≡ 0;x ≡ y)
Lemma: rv-sub0
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. x - 0 ≡ x
Lemma: rv-sub-same
∀[rv:RealVectorSpace]. ∀[x:Point(rv)]. x - x ≡ 0
Lemma: rv-sub-sep
∀rv:RealVectorSpace. ∀x,x',y,y':Point(rv). (x - y # x' - y' ⇒ (x # x' ∨ y # y'))
Lemma: rv-mul-sub
∀[rv:RealVectorSpace]. ∀[a,b:ℝ]. ∀[x:Point(rv)]. a - b*x ≡ a*x - b*x
Lemma: rv-mul-rv-sub
∀[rv:RealVectorSpace]. ∀[a:ℝ]. ∀[x,y:Point(rv)]. a*x - y ≡ a*x - a*y
Lemma: rv-ip-sub
∀[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)]. (x - y ⋅ z = (x ⋅ z - y ⋅ z))
Lemma: rv-ip-sub2
∀[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)]. (z ⋅ x - y = (z ⋅ x - z ⋅ y))
Lemma: rv-sub-add
∀[rv:InnerProductSpace]. ∀[x,v:Point(rv)]. x - v + v ≡ x
Lemma: rv-ip-sub-squared
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (x - y^2 = ((x^2 - r(2) * x ⋅ y) + y^2))
Lemma: rv-ip-add-squared
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (x + y^2 = ((x^2 + (r(2) * x ⋅ y)) + y^2))
Lemma: rv-ip-zero-iff
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. uiff(x^2 = r0;x ≡ 0)
Lemma: rv-sep-iff
∀rv:InnerProductSpace. ∀x,y:Point(rv). (x # y ⇐⇒ x - y # 0)
Lemma: rv-sep-iff-ext
∀rv:InnerProductSpace. ∀x,y:Point(rv). (x # y ⇐⇒ x - y # 0)
Definition: rv-norm
||x|| == rsqrt(x^2)
Lemma: rv-norm_wf
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (||x|| ∈ {r:ℝ| (r0 ≤ r) ∧ ((r * r) = x^2)} )
Lemma: rv-norm_functionality
∀[rv:InnerProductSpace]. ∀[x1,x2:Point(rv)]. ||x1|| = ||x2|| supposing x1 ≡ x2
Lemma: rv-norm0
∀[rv:InnerProductSpace]. (||0|| = r0)
Lemma: rv-norm-nonneg
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (r0 ≤ ||x||)
Lemma: rv-norm-positive
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇒ (r0 < ||x||))
Lemma: rv-norm-squared
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. (||x||^2 = x^2)
Lemma: rv-norm-eq-iff
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. ∀[r:ℝ]. uiff(||x|| = r;x^2 = r^2) supposing r0 ≤ r
Lemma: rv-norm-equal-iff
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. uiff(||x|| = ||y||;x^2 = y^2)
Lemma: rv-norm-difference-symmetry
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. (||a - b|| = ||b - a||)
Lemma: rv-norm-is-zero
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. uiff(||x|| = r0;x ≡ 0)
Lemma: rv-norm-positive-iff
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇐⇒ r0 < ||x||)
Lemma: rv-norm-positive-iff-ext
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇐⇒ r0 < ||x||)
Lemma: rv-sep-iff-norm
∀rv:InnerProductSpace. ∀x,y:Point(rv). (x # y ⇐⇒ r0 < ||x - y||)
Lemma: rv-sep-shift
∀rv:InnerProductSpace. ∀a,p,q:Point(rv). (p # q ⇒ p - a # q - a)
Lemma: rv-sep-shift2
∀rv:InnerProductSpace. ∀a,p,q:Point(rv). (p # q ⇒ p + a # q + a)
Lemma: sq_stable__rv-sep
∀rv:InnerProductSpace. ∀x,y:Point(rv). SqStable(x # y)
Lemma: sq_stable__rv-sep-ext
∀rv:InnerProductSpace. ∀x,y:Point(rv). SqStable(x # y)
Lemma: rv-sep-or
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀c:Point(rv). (a # c ∨ b # c)
Definition: rv-sep-witness
rv-sep-witness(rv;x;y) ==
case rv."+sep" -y -y x y
case rv."#or" -y + x 0 -y + x
case rv."#or" x + -y 0 -y + x
let _,p = rv."positive" x - y
in p ((((rlessw(r0^2;||x - y||^2) * 20) + 1) * 20) + 1)
of inl(_) =>
Ax
| inr(b) =>
case rv."#or" 0 -y + x 0 b of inl(_) => Ax | inr(a) => a
of inl(_) =>
Ax
| inr(b) =>
case rv."#or" 0 -y + x -y + y b of inl(_) => Ax | inr(a) => a
of inl(_) =>
Ax
| inr(a) =>
a
Lemma: rv-sep-witness_wf
∀rv:InnerProductSpace. ∀x:Point(rv). ∀y:{y:Point(rv)| x # y} . (rv-sep-witness(rv;x;y) ∈ x # y)
Lemma: rv-norm-mul
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. ∀[a:ℝ]. (||a*x|| = (|a| * ||x||))
Lemma: rv-norm-sub
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (||x - y|| = ||y - x||)
Lemma: rv-mul-sep-zero
∀rv:InnerProductSpace. ∀t:ℝ. ∀x:Point(rv). (t*x # 0 ⇐⇒ x # 0 ∧ (r0 < |t|))
Lemma: rv-mul-sep-iff
∀rv:InnerProductSpace. ∀a,b:ℝ. ∀y:Point(rv). (a*y # b*y ⇐⇒ a ≠ b ∧ y # 0)
Lemma: rv-add-sep-iff
∀rv:InnerProductSpace. ∀a,b,h:Point(rv). (h + a # h + b ⇐⇒ a # b)
Definition: rv-unit
rv-unit(rv;x) == (r1/||x||)*x
Lemma: rv-unit_wf
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. rv-unit(rv;x) ∈ {z:Point(rv)| z^2 = r1} supposing x # 0
Lemma: rv-unit-squared
∀[rv:InnerProductSpace]. ∀[x:Point(rv)]. rv-unit(rv;x)^2 = r1 supposing x # 0
Lemma: rv-unit-property
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇒ (∃t:ℝ. (t ≠ r0 ∧ rv-unit(rv;x) ≡ t*x)))
Lemma: rv-perp-1
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇒ (∃y:Point(rv). ((y^2 = r1) ∧ (x ⋅ y = r0))))
Lemma: rv-perp-same-norm
∀rv:InnerProductSpace. ∀x:Point(rv). (x # 0 ⇒ (∃y:Point(rv). ((||y|| = ||x||) ∧ (x ⋅ y = r0))))
Lemma: rv-Cauchy-Schwarz
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. (a ⋅ b^2 ≤ (a^2 * b^2))
Lemma: rv-Cauchy-Schwarz'
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. (|a ⋅ b| ≤ (||a|| * ||b||))
Lemma: rv-ip-rleq
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. (a ⋅ b ≤ (||a|| * ||b||))
Lemma: rv-ip-rneq-0
∀rv:InnerProductSpace. ∀a,b:Point(rv). (a ⋅ b ≠ r0 ⇒ (a # 0 ∧ b # 0))
Lemma: rv-ip-rneq
∀rv:InnerProductSpace. ∀a1,b1,a2,b2:Point(rv). (a1 ⋅ b1 ≠ a2 ⋅ b2 ⇒ (a1 # a2 ∨ b1 # b2))
Lemma: rv-norm-triangle-inequality
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (||x + y|| ≤ (||x|| + ||y||))
Lemma: rv-norm-triangle-inequality2
∀[rv:InnerProductSpace]. ∀[x,y,z:Point(rv)]. (||x - z|| ≤ (||x - y|| + ||y - z||))
Lemma: rv-Cauchy-Schwarz-equality
∀rv:InnerProductSpace. ∀a,b:Point(rv). ((a ⋅ b^2 = (a^2 * b^2)) ⇒ b # 0 ⇒ (∃t:ℝ. a ≡ t*b))
Lemma: rv-Cauchy-Schwarz-equality'
∀rv:InnerProductSpace. ∀a,b:Point(rv). ((|a ⋅ b| = (||a|| * ||b||)) ⇒ b # 0 ⇒ (∃t:ℝ. a ≡ t*b))
Definition: rv-orthogonal
Orthogonal(f) == (∀x,y:Point(rv). (f x + y ≡ f x + f y ∧ (x ⋅ y = f x ⋅ f y))) ∧ (∀x:Point(rv). ∀a:ℝ. f a*x ≡ a*f x)
Lemma: rv-orthogonal_wf
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ∈ ℙ)
Lemma: sq_stable__rv-orthogonal
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). SqStable(Orthogonal(f))
Lemma: rv-orthogonal-injective
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇒ (∀x,y:Point(rv). (f x ≡ f y ⇒ x ≡ y)))
Lemma: rv-orthogonal-iff-norm-preserving
∀[rv:InnerProductSpace]
∀f:Point(rv) ⟶ Point(rv)
(Orthogonal(f)
⇐⇒ (∀x,y:Point(rv). f x + y ≡ f x + f y) ∧ (∀x:Point(rv). ((∀a:ℝ. f a*x ≡ a*f x) ∧ (||f x|| = ||x||))))
Definition: rv-isometry
Isometry(f) == ∀[x,y:Point(rv)]. (||f x - f y|| = ||x - y||)
Lemma: rv-isometry_wf
∀[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)]. (Isometry(f) ∈ ℙ)
Lemma: sq_stble__rv-isometry
∀[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)]. SqStable(Isometry(f))
Lemma: rv-orthogonal-isometry
∀[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)]. Isometry(f) supposing Orthogonal(f)
Lemma: rv-isometry-implies-extensional
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀x,y:Point(rv). (f x # f y ⇒ x # y) supposing Isometry(f)
Lemma: rv-isometry-injective
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Isometry(f) ⇒ (∀x,y:Point(rv). (f x ≡ f y ⇒ x ≡ y)))
Lemma: rv-orthogonal-implies-extensional
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀x,y:Point(rv). (f x # f y ⇒ x # y) supposing Orthogonal(f)
Lemma: rv-orthogonal-implies-extensional-ext
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀x,y:Point(rv). (f x # f y ⇒ x # y) supposing Orthogonal(f)
Definition: rv-orthog-ext
rv-orthog-ext(rv;f) ==
λx,y,_. case rv."+sep" -y -y x y
case rv."#or" -y + x 0 -y + x
case rv."#or" x + -y 0 -y + x
let _,h = rv."positive" x - y
in h ((((rlessw(r0^2;||x - y||^2) * 20) + 1) * 20) + 1)
of inl(_) =>
Ax
| inr(a) =>
case rv."#or" 0 -y + x 0 a of inl(_) => Ax | inr(x) => x
of inl(_) =>
Ax
| inr(a) =>
case rv."#or" 0 -y + x -y + y a of inl(_) => Ax | inr(x) => x
of inl(_) =>
Ax
| inr(x) =>
x
Lemma: rv-orthog-ext_wf
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv).
rv-orthog-ext(rv;f) ∈ ∀x,y:Point(rv). (f x # f y ⇒ x # y) supposing Orthogonal(f)
Lemma: rv-isometry-implies-functional
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Isometry(f) ⇒ (∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y)))
Lemma: rv-orthogonal-implies-functional
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇒ (∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y)))
Lemma: rv-midpoint-unique
∀rv:InnerProductSpace. ∀a,b,m:Point(rv).
((||m - a|| = (||b - a||/r(2))) ∧ (||m - b|| = (||b - a||/r(2))) ⇐⇒ m ≡ (r1/r(2))*a + b)
Lemma: rv-orthogonal-iff
∀[rv:InnerProductSpace]. ∀f:Point(rv) ⟶ Point(rv). (Orthogonal(f) ⇐⇒ f 0 ≡ 0 ∧ Isometry(f))
Lemma: rv-isometry-compose
∀[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)]. (Isometry(f o g)) supposing (Isometry(g) and Isometry(f))
Lemma: rv-orthogonal-compose
∀[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)]. (Orthogonal(f o g)) supposing (Orthogonal(g) and Orthogonal(f))
Lemma: rv-isometry-inverse
∀[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].
(Isometry(f)) supposing (Isometry(g) and (∀x:Point(rv). g (f x) ≡ x))
Lemma: rv-orthogonal-inverse
∀[rv:InnerProductSpace]. ∀[f,g:Point(rv) ⟶ Point(rv)].
(Orthogonal(f)) supposing (Orthogonal(g) and (∀x:Point(rv). g (f x) ≡ x))
Lemma: rv-isometry-id
∀[rv:InnerProductSpace]. Isometry(λx.x)
Lemma: rv-orthogonal-id
∀[rv:InnerProductSpace]. Orthogonal(λx.x)
Definition: rv-permutation-group
Perm(rv) == Perm(rv)
Lemma: rv-permutation-group_wf
∀[rv:InnerProductSpace]. (Perm(rv) ∈ s-Group)
Lemma: rv-perm-point
∀[rv:Top]
(Point(Perm(rv)) ~ {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))|
let f,g = fg
in (∀x:Point(rv). f (g x) ≡ x)
∧ (∀x:Point(rv). g (f x) ≡ x)
∧ (∀x,y:Point(rv). (f x # f y ⇒ x # y))
∧ (∀x,y:Point(rv). (g x # g y ⇒ x # y))} )
Lemma: rv-perm-id
∀[rv:Top]. (1 ~ <λx.x, λx.x>)
Lemma: rv-perm-inv
∀[rv,x:Top]. (x^-1 ~ let f,g = x in <g, f>)
Lemma: rv-perm-op
∀[rv,x,y:Top]. ((x y) ~ let f,g = x in let f',g' = y in <f o f', g' o g>)
Definition: rv-isometry-group
Isom(rv) == mk-s-subgroup(Perm(rv);fg.Isometry(fst(fg)))
Lemma: rv-isometry-group_wf
∀[rv:InnerProductSpace]. (Isom(rv) ∈ s-Group)
Lemma: subtype-rv-isometry-group
∀[rv:InnerProductSpace]
({fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| let f,g = fg in (∀x:Point(rv). f (g x) ≡ x) ∧ Isometry(f)}
⊆r Point(Isom(rv)))
Definition: orthogonal-group
O(rv) == mk-s-subgroup(Perm(rv);fg.Orthogonal(fst(fg)))
Lemma: orthogonal-group_wf
∀[rv:InnerProductSpace]. (O(rv) ∈ s-Group)
Lemma: subtype-orthogonal-group
∀[rv:InnerProductSpace]
({fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))| let f,g = fg in (∀x:Point(rv). f (g x) ≡ x) ∧ Orthogonal(f)}
⊆r Point(O(rv)))
Definition: is-isometry
is-isometry(rv;f) == ∃g:Point(rv) ⟶ Point(rv). ∃t:Point(rv). (Orthogonal(g) ∧ (∀x:Point(rv). f x ≡ g x + t))
Lemma: is-isometry_wf
∀[rv:InnerProductSpace]. ∀[f:Point(rv) ⟶ Point(rv)]. (is-isometry(rv;f) ∈ ℙ)
Lemma: implies-isometry-lemma1
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} . ∀N:{2...}.
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r)))
⇒ (∀x,y:Point(rv). ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||)))
⇒ {∀x,y:Point(rv). (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||))})
Lemma: implies-isometry-lemma2
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} .
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||)))
⇒ (∀x,y:Point(rv). ((||x - y|| = r) ⇒ (∀j:ℕ. f x + r(j)*y - x ≡ f x + r(j)*f y - f x))))
Comment: geometry primitives in inner product spaces
The primitives of constructive geometry are
1) separation (of two points)
2) betweeness (a ternary relation)
3) congruence (a quaternary relation)
4) triangle (a ternary relation that says
a triangle has strictly positive angles)
If rv is an ⌜InnerProductSpace⌝ then it is a ⌜SeparationSpace⌝ so it has
a primitive ⌜x # y⌝ for separation.
For congrence ab=cd we use ⌜||a - b|| = ||c - d||⌝.
The proper triangle relation on a, b, c is
⌜|a - b ⋅ c - b| < (||a - b|| * ||c - b||)⌝
it is saying that the Cauchy-Schwarz inequality is strict.
This turns out to be a symmetric relation.
For the betweeness relation B(a,b,c) we say that
Cauchy-Schwarz gives equality so that (a-b) and (c-b) are linearly dependent
and in addition the inner product is non-positive ⌜a - b ⋅ c - b ≤ r0⌝.
That puts 0 between ⌜a - b⌝ and ⌜c - b⌝, so b is between a and c.
We can say both parts of the B(a,b,c) relation in one equality realtion:
⌜((||a - b|| * ||c - b||) + a - b ⋅ c - b) = r0⌝.
This makes B(a,b,c) and ab=cd stable relations
(equivalent to their double negation), while ⌜x # y⌝ and triangle(a,b,c)
have constructive content and are not stable, in general.
.⋅
Definition: ip-congruent
ab=cd == ||a - b|| = ||c - d||
Lemma: ip-congruent_wf
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. (ab=cd ∈ ℙ)
Lemma: stable__ip-congruent
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. Stable{ab=cd}
Lemma: sq_stable__ip-congruent
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. SqStable(ab=cd)
Lemma: ip-congruent-sym
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. ab=ba
Lemma: ip-congruent-trans
∀[rv:InnerProductSpace]. ∀[a,b,p,q,r,s:Point(rv)]. (pq=rs) supposing (ab=rs and ab=pq)
Lemma: ip-congruent_functionality
∀[rv:InnerProductSpace]. ∀[a,b,c,d,a2,b2,c2,d2:Point(rv)].
({ab=cd ⇐⇒ a2b2=c2d2}) supposing (d ≡ d2 and c ≡ c2 and b ≡ b2 and a ≡ a2)
Lemma: ip-congruent-same
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (aa=bc ⇒ b ≡ c)
Lemma: ip-congruent-same2
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (ab=cc ⇒ a ≡ b)
Lemma: ip-congruent-sep
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). ∀d:{d:Point(rv)| ab=cd} . (a # b ⇒ c # d)
Definition: ip-between
a_b_c == ((||a - b|| * ||c - b||) + a - b ⋅ c - b) = r0
Lemma: ip-between_wf
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (a_b_c ∈ ℙ)
Lemma: ip-between_functionality
∀[rv:InnerProductSpace]. ∀[a,b,c,a2,b2,c2:Point(rv)]. (a ≡ a2 ⇒ b ≡ b2 ⇒ c ≡ c2 ⇒ {a_b_c ⇐⇒ a2_b2_c2})
Lemma: ip-between-iff
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (a # b ⇒ c # b ⇒ (a_b_c ⇐⇒ ∃t:ℝ. ((t ∈ (r0, r1)) ∧ b ≡ t*a + r1 - t*c)))
Lemma: ip-between-same
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. (a_b_a ⇒ b ≡ a)
Definition: ip-triangle
Δ(a;b;c) == |a - b ⋅ c - b| < (||a - b|| * ||c - b||)
Lemma: ip-triangle_wf
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (Δ(a;b;c) ∈ ℙ)
Lemma: sq_stable__ip-triangle
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). SqStable(Δ(a;b;c))
Lemma: ip-triangle_functionality
∀rv:InnerProductSpace. ∀a,b,c,a2,b2,c2:Point(rv). (a ≡ a2 ⇒ b ≡ b2 ⇒ c ≡ c2 ⇒ {Δ(a;b;c) ⇐⇒ Δ(a2;b2;c2)})
Lemma: ip-triangle-symmetry
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ Δ(c;b;a))
Lemma: ip-triangle-permute-lemma
∀rv:InnerProductSpace. ∀x,y:Point(rv). ((|x ⋅ y| < (||x|| * ||y||)) ⇒ (|x ⋅ y - x| < (||x|| * ||y - x||)))
Lemma: ip-triangle-permute
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ Δ(c;a;b))
Lemma: ip-triangle-linearity
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ (∀t:ℝ. ((r0 < |t|) ⇒ Δ(b + t*a - b;b;c))))
Lemma: ip-triangle-implies-separated
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ a # c)
Lemma: ip-triangle-implies-separated2
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ a # b)
Lemma: not-ip-triangle
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (a # b ⇒ c # b ⇒ (¬Δ(a;b;c)) ⇒ (∃t:ℝ. ((r0 < |t|) ∧ c ≡ b + t*a - b)))
Lemma: ip-triangle-shift
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (Δ(a;b;c) ⇒ (∀z:Point(rv). (z # b ⇒ (¬Δ(a;b;z)) ⇒ Δ(z;b;c))))
Lemma: ip-triangle-not-between
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. ¬a_b_c supposing Δ(a;b;c)
Lemma: ip-triangle-implies
∀rv:InnerProductSpace. ∀a,b,c:Point(rv).
(Δ(a;b;c) ⇒ (Δ(c;b;a) ∧ Δ(c;a;b) ∧ a # c ∧ (¬a_b_c) ∧ (∀z:Point(rv). (z # b ⇒ (¬Δ(a;b;z)) ⇒ Δ(z;b;c)))))
Lemma: ip-triangle-lemma
∀rv:InnerProductSpace. ∀x,y:Point(rv).
((||x|| = ||y||) ⇒ (r0 < ||x - y||) ⇒ (r0 < ||r(-1)*x - y||) ⇒ (|x ⋅ y| < (||x|| * ||y||)))
Lemma: implies-ip-triangle
∀rv:InnerProductSpace. ∀a,b,c,a':Point(rv). (a_b_a' ⇒ ab=a'b ⇒ ab=cb ⇒ c # a ⇒ c # a' ⇒ Δ(a;b;c))
Lemma: ip-between-symmetry
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (a_b_c ⇒ c_b_a)
Lemma: ip-between-trivial
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. b_b_a
Lemma: ip-between-trivial2
∀[rv:InnerProductSpace]. ∀[a,b:Point(rv)]. a_b_b
Lemma: stable__ip-between
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. Stable{a_b_c}
Lemma: sq_stable__ip-between
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. SqStable(a_b_c)
Lemma: not-ip-triangle-implies
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). ((¬Δ(a;b;c)) ⇒ (¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b))))
Lemma: not-ip-triangle-iff
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (¬Δ(a;b;c) ⇐⇒ ¬((¬a_b_c) ∧ (¬b_c_a) ∧ (¬c_a_b)))
Lemma: ip-between-inner-trans
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. (a_b_d ⇒ b_c_d ⇒ a_b_c)
Lemma: ip-dist-between-1
∀[rv:InnerProductSpace]. ∀[t:ℝ]. ∀[a,c:Point(rv)]. (||a - t*a + r1 - t*c|| = (|r1 - t| * ||a - c||))
Lemma: ip-dist-between-2
∀[rv:InnerProductSpace]. ∀[t:ℝ]. ∀[a,c:Point(rv)]. (||t*a + r1 - t*c - c|| = (|t| * ||a - c||))
Lemma: ip-dist-between
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. ||a - c|| = (||a - b|| + ||b - c||) supposing a_b_c
Lemma: ip-between-rleq
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. {(||a - b|| ≤ ||a - c||) ∧ (||b - c|| ≤ ||a - c||)} supposing a_b_c
Lemma: ip-between-rless
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (a_b_c ⇒ b # c ⇒ (||a - b|| < ||a - c||))
Lemma: ip-between-sep
∀rv:InnerProductSpace. ∀a,c:Point(rv). ∀[b:Point(rv)]. (a # c) supposing (a # b and a_b_c)
Lemma: ip-between-iff2
∀rv:InnerProductSpace. ∀a,b,c:Point(rv).
(a_b_c ⇐⇒ (a ≡ c ⇒ b ≡ c) ∧ (a # c ⇒ (∃t:ℝ. ((t ∈ [r0, r1]) ∧ b ≡ t*a + r1 - t*c))))
Lemma: rn-ip-between
∀n:{2...}. ∀a,b,c:ℝ^n. (a_b_c ⇐⇒ rv-T(n;a;b;c))
Definition: ip-ge
cd ≥ ab == ¬¬(∃w:Point(rv). (c_w_d ∧ cw=ab))
Lemma: ip-ge_wf
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. (cd ≥ ab ∈ ℙ)
Definition: ip-gt
cd > ab == ↓∃w:Point(rv). (c_w_d ∧ cw=ab ∧ w # d)
Lemma: ip-gt_wf
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. (cd > ab ∈ ℙ)
Lemma: ip-five-segment-lemma
∀[rv:InnerProductSpace]. ∀[A,B,C,D:Point(rv)]. ∀[t:ℝ].
((t ∈ (r0, r1))
⇒ B ≡ t*A + r1 - t*C
⇒ let a = ||D - B|| in
let b = ||A - D|| in
let c = ||B - C|| in
let d = ||A - B|| in
let x = ||D - C|| in
let s = (t/t - r1) in
x^2 = (c^2 + a^2 + (s * (b^2 - d^2 + a^2))))
Lemma: ip-five-segment
∀[rv:InnerProductSpace]. ∀[a,b,c,d,A,B,C,D:Point(rv)].
(cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and a # b)
Definition: ip-strict-between
a-b-c == a_b_c ∧ a # b ∧ b # c
Lemma: ip-strict-between_wf
∀[rv:InnerProductSpace]. ∀[a,b,c:Point(rv)]. (a-b-c ∈ ℙ)
Lemma: ip-strict-between-iff
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). (a-b-c ⇐⇒ (∃t:ℝ. ((t ∈ (r0, r1)) ∧ b ≡ t*a + r1 - t*c)) ∧ a # c)
Lemma: ip-inner-Pasch1
∀rv:InnerProductSpace. ∀a,b,c,p,q:Point(rv).
(a # p
⇒ b # c
⇒ a_p_c
⇒ b_q_c
⇒ (∃x:Point(rv)
(a_x_q
∧ b_x_p
∧ (a # q ⇒ x # a)
∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
∧ ((b # p ∧ b # q) ⇒ x # b)
∧ ((b # p ∧ q # c) ⇒ x # p))))
Lemma: ip-inner-Pasch
∀rv:InnerProductSpace. ∀a,b,c:Point(rv). ∀p:{p:Point(rv)| a_p_c} . ∀q:{q:Point(rv)| b_q_c} .
(a # p
⇒ b # c
⇒ (∃x:{x:Point(rv)| a_x_q ∧ b_x_p}
((a # q ⇒ x # a)
∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
∧ ((b # p ∧ b # q) ⇒ x # b)
∧ ((b # p ∧ q # c) ⇒ x # p))))
Lemma: ip-inner-Pasch'
∀rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| b # c} . ∀p:{p:Point(rv)| a_p_c ∧ a # p} .
∀q:{q:Point(rv)| b_q_c} .
(∃x:Point(rv) [(a_x_q
∧ b_x_p
∧ (a # q ⇒ x # a)
∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
∧ ((b # p ∧ b # q) ⇒ x # b)
∧ ((b # p ∧ q # c) ⇒ x # p))])
Lemma: ip-line-circle-lemma
∀rv:InnerProductSpace. ∀r:ℝ. ∀p,q:Point(rv).
(p # q
⇒ (||p|| ≤ r)
⇒ let v = q - p in
(r0 ≤ (((r(2) * p ⋅ v) * r(2) * p ⋅ v) - r(4) * ||v||^2 * (||p||^2 - r^2)))
∧ (||p + quadratic1(||v||^2;r(2) * p ⋅ v;||p||^2 - r^2)*v|| = r)
∧ (||p + quadratic2(||v||^2;r(2) * p ⋅ v;||p||^2 - r^2)*v|| = r))
Lemma: ip-line-circle-1
∀rv:InnerProductSpace. ∀a,b,p,q:Point(rv).
(a # b
⇒ p # q
⇒ (||p - a|| ≤ ||a - b||)
⇒ (||a - b|| ≤ ||q - a||)
⇒ (∃u:{u:Point(rv)| ab=au ∧ q_u_p}
∃v:{v:Point(rv)| ab=av ∧ q_p_v} . ((||a - p|| < ||a - b||) ⇒ (p # v ∧ ((||a - b|| < ||a - q||) ⇒ q # u)))))
Lemma: ip-circle-circle-lemma1
∀rv:InnerProductSpace. ∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:Point(rv).
((r0 < ||b||)
⇒ (∀b':Point(rv)
((b ⋅ b' = r0)
⇒ (||b'|| = ||b||)
⇒ ((r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2))
⇒ let c = ((r1^2 - r2^2) + ||b||^2/r(2)) in
let d = (||b||^2 * r1^2) - c^2 in
∀x:Point(rv)
((x ≡ (r1/||b||^2)*c*b + rsqrt(d)*b' ∨ x ≡ (r1/||b||^2)*c*b - rsqrt(d)*b')
⇒ ((||x|| = r1) ∧ (||x - b|| = r2))))))
Lemma: ip-circle-circle-lemma2
∀rv:InnerProductSpace. ∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:Point(rv).
((r0 < ||b||)
⇒ ((r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2))
⇒ (∃u,v:Point(rv)
(((||u|| = r1) ∧ (||u - b|| = r2))
∧ ((||v|| = r1) ∧ (||v - b|| = r2))
∧ (((r1^2 - r2^2) + ||b||^2^2 < (r(4) * ||b||^2 * r1^2)) ⇒ u # v))))
Lemma: ip-circle-circle-lemma3
∀rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| a # c} . ∀d:Point(rv).
∀[p:{p:Point(rv)| ab=ap ∧ (||c - p|| ≤ ||c - d||)} ]. ∀[q:{q:Point(rv)| cd=cq ∧ (||a - q|| ≤ ||a - b||)} ].
∃u,v:{p:Point(rv)| ab=ap ∧ cd=cp} . (((||a - q|| < ||a - b||) ∧ (||c - p|| < ||c - d||)) ⇒ u # v)
Lemma: ip-extend-lemma
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀dcd:{d:ℝ| r0 ≤ d} .
(∃x:Point(rv) [(a_b_x ∧ (||b - x|| = dcd))])
Lemma: ip-ge-dist
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. ((||a - b|| ≤ ||c - d||) ⇒ (¬¬(∃w:Point(rv). (a_b_w ∧ cd=aw))))
Lemma: ip-gt-iff
∀rv:InnerProductSpace. ∀a,b,c,d:Point(rv). uiff(cd > ab;||a - b|| < ||c - d||)
Lemma: ip-ge-iff
∀[rv:InnerProductSpace]. ∀[a,b,c,d:Point(rv)]. uiff(cd ≥ ab;||a - b|| ≤ ||c - d||)
Lemma: ip-line-circle
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀p:{p:Point(rv)| ab ≥ ap} . ∀q:{q:Point(rv)|
p # q ∧ aq ≥ ab} .
∃u:{u:Point(rv)| ab=au ∧ q_u_p} . (∃v:Point(rv) [(ab=av ∧ q_p_v)])
Lemma: ip-ge-sep
∀rv:InnerProductSpace. ∀a,c:Point(rv). ∀[b:Point(rv)]. (a # c) supposing (a # b and ac ≥ ab)
Lemma: ip-circle-circle
∀rv:InnerProductSpace. ∀a,b:Point(rv). ∀c:{c:Point(rv)| a # c} . ∀d:Point(rv).
∀[p:{p:Point(rv)| ab=ap ∧ cd ≥ cp} ]. ∀[q:{q:Point(rv)| cd=cq ∧ ab ≥ aq} ].
∃u:{u:Point(rv)| ab=au ∧ cd=cu} . (∃v:Point(rv) [((ab=av ∧ cd=cv) ∧ ((ab > aq ∧ cd > cp) ⇒ u # v))])
Lemma: ip-weak-triangle-inequality
∀rv:InnerProductSpace. ∀a,b,x,p:Point(rv). (ax=ab ⇒ a_x_p ⇒ bp ≥ xp)
Lemma: ip-non-trivial
∀rv:InnerProductSpace. ∀x:{x:Point(rv)| r0 < ||x||} . ∃a:Point(rv). (∃b:Point(rv) [a # b])
Lemma: ip-extend
∀rv:InnerProductSpace. ∀a:Point(rv). ∀b:{b:Point(rv)| a # b} . ∀c,d:Point(rv). (∃x:Point(rv) [(a_b_x ∧ bx=cd)])
Definition: mkr2
mkr2(a;b) == λi.[a; b][i]
Lemma: mkr2_wf
∀[a,b:ℝ]. (mkr2(a;b) ∈ ℝ^2)
Lemma: implies-isometry-lemma3
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} .
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||)))
⇒ (∀n,m:ℕ+. ∀x,y:Point(rv). ((||x - y|| = (r(n) * r/r(m))) ⇒ (||f x - f y|| = ||x - y||))))
Lemma: implies-isometry-lemma4
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} .
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). (((||x - y|| = r) ∨ (||x - y|| = (r(2) * r))) ⇒ (||f x - f y|| = ||x - y||)))
⇒ (∀n,m:ℕ+. ∀x,y:Point(rv). ((||x - y|| < (r(n) * r/r(m))) ⇒ (||f x - f y|| ≤ (r(n) * r/r(m))))))
Lemma: implies-isometry-lemma5
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀d:{r:ℝ| r0 < r} .
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). (((||x - y|| = d) ∨ (||x - y|| = (r(2) * d))) ⇒ (||f x - f y|| = ||x - y||)))
⇒ (∀s,r:ℝ.
((∃n,m:ℕ+. (s = (r(n)/r(m))))
⇒ (∃n,m:ℕ+. (r = (r(n)/r(m))))
⇒ (∀x,y:Point(rv). ((||x - y|| ∈ (r * d, s * d)) ⇒ (||f x - f y|| ∈ [r * d, s * d]))))))
Lemma: implies-isometry
∀rv:InnerProductSpace. ∀f:Point(rv) ⟶ Point(rv). ∀r:{r:ℝ| r0 < r} . ∀N:{2...}.
((∀x,y:Point(rv). (x ≡ y ⇒ f x ≡ f y))
⇒ (∀x,y:Point(rv). ((||x - y|| = r) ⇒ (||f x - f y|| ≤ r)))
⇒ (∀x,y:Point(rv). ((||x - y|| = (r(N) * r)) ⇒ ((r(N) * r) ≤ ||f x - f y||)))
⇒ is-isometry(rv;f))
Lemma: uhg-identity1
∀[t1,t2,t3,t4:ℝ].
((((((r1 + (t1 * t2)) * (t3 + t4)) - (r1 + (t3 * t4)) * (t1 + t2))
* (((r1 + (t1 * t3)) * (t2 + t4)) - (r1 + (t2 * t4)) * (t1 + t3)))
+ ((r(2) * ((t3 * t4) - t1 * t2)) * r(2) * ((t2 * t4) - t1 * t3)))
= ((((r1 - t1 * t2) * (t3 + t4)) - (r1 - t3 * t4) * (t1 + t2))
* (((r1 - t1 * t3) * (t2 + t4)) - (r1 - t2 * t4) * (t1 + t3))))
Definition: real-proj
ℙ^n == {b:ℝ^n + 1| ∃k:ℕn + 1. b k ≠ r0}
Lemma: real-proj_wf
∀[n:ℕ]. (ℙ^n ∈ Type)
Lemma: proj-norm-positive
∀n:ℕ. ∀a:ℙ^n. (r0 < ||a||)
Definition: punit
u(a) == (r1/||a||)*a
Lemma: punit_wf
∀[n:ℕ]. ∀[a:ℙ^n]. (u(a) ∈ ℝ^n + 1)
Lemma: punit-norm1
∀[n:ℕ]. ∀[a:ℙ^n]. (||u(a)|| = r1)
Definition: proj-sep
a ≠ b == u(a) ≠ u(b) ∧ u(a) ≠ r(-1)*u(b)
Lemma: proj-sep_wf
∀[n:ℕ]. ∀[a,b:ℙ^n]. (a ≠ b ∈ ℙ)
Lemma: proj-sep_symmetry
∀n:ℕ. ∀a,b:ℙ^n. (a ≠ b ⇒ b ≠ a)
Lemma: proj-sep_antireflexive
∀[n:ℕ]. ∀[a:ℙ^n]. (¬a ≠ a)
Lemma: sq_stable__proj-sep
∀n:ℕ. ∀a,b:ℙ^n. SqStable(a ≠ b)
Lemma: not-proj-sep
∀n:ℕ. ∀a,b:ℙ^n. (¬a ≠ b ⇐⇒ req-vec(n + 1;u(a);u(b)) ∨ req-vec(n + 1;u(a);r(-1)*u(b)))
Lemma: proj-sep-or
∀n:ℕ. ∀a,b,c:ℙ^n. (a ≠ b ⇒ (a ≠ c ∨ b ≠ c))
Definition: proj-eq
a = b == ∀i,j:ℕn + 1. (((a i) * (b j)) = ((b i) * (a j)))
Lemma: proj-eq_wf
∀[n:ℕ]. ∀[a,b:ℙ^n]. (a = b ∈ ℙ)
Lemma: sq_stable__proj-eq
∀[n:ℕ]. ∀[a,b:ℙ^n]. SqStable(a = b)
Lemma: stable__proj-eq
∀[n:ℕ]. ∀[a,b:ℙ^n]. Stable{a = b}
Lemma: proj-eq-iff
∀n:ℕ. ∀a,b:ℙ^n. (a = b ⇐⇒ ↓∃m:{m:ℝ| m ≠ r0} . req-vec(n + 1;a;m*b))
Lemma: proj-eq-equiv
∀[n:ℕ]. EquivRel(ℙ^n;a,b.a = b)
Lemma: proj-eq_inversion
∀[n:ℕ]. ∀[a,b:ℙ^n]. b = a supposing a = b
Lemma: proj-eq_transitivity
∀[n:ℕ]. ∀[a,b,c:ℙ^n]. (a = c) supposing (b = c and a = b)
Lemma: proj-eq_weakening
∀[n:ℕ]. ∀[a,b:ℙ^n]. a = b supposing a = b ∈ ℙ^n
Lemma: proj-eq_functionality
∀[n:ℕ]. ∀[x1,x2,y1,y2:ℙ^n]. (uiff(x1 = y1;x2 = y2)) supposing (y1 = y2 and x1 = x2)
Lemma: not-proj-sep-iff-proj-eq
∀n:ℕ. ∀a,b:ℙ^n. (¬a ≠ b ⇐⇒ a = b)
Lemma: proj-sep_functionality
∀n:ℕ. ∀a1,b1,a2,b2:ℙ^n. (a1 = a2 ⇒ b1 = b2 ⇒ {a1 ≠ b1 ⇐⇒ a2 ≠ b2})
Lemma: proj-sep-implies
∀n:ℕ. ∀a,b:ℙ^n. (a ≠ b ⇒ (∃i,j:ℕn + 1. (a i) * (b j) ≠ (a j) * (b i)))
Definition: proj-rev
proj-rev(n;p) == λi.if i <z n then p i else -(p i) fi
Lemma: proj-rev_wf
∀[n:ℕ]. ∀[p:ℙ^n]. (proj-rev(n;p) ∈ ℙ^n)
Lemma: proj-rev_functionality
∀[n:ℕ]. ∀[p1,p2:ℙ^n]. proj-rev(n;p1) = proj-rev(n;p2) supposing p1 = p2
Definition: proj-incidence
v on p == v⋅proj-rev(n;p) = r0
Lemma: proj-incidence_wf
∀[n:ℕ]. ∀[p,v:ℙ^n]. (v on p ∈ ℙ)
Lemma: proj-incidence_symmetry
∀[n:ℕ]. ∀[p,v:ℙ^n]. uiff(v on p;p on v)
Lemma: proj-incidence_functionality
∀[n:ℕ]. ∀[p1,p2,v1,v2:ℙ^n]. (uiff(v1 on p1;v2 on p2)) supposing (p1 = p2 and v1 = v2)
Lemma: p2-incidence
∀[p,v:ℙ^2]. uiff(v on p;((((v 0) * (p 0)) + ((v 1) * (p 1))) - (v 2) * (p 2)) = r0)
Definition: p2J
p2J(a;b) ==
λi.if (i =z 0) then ((a 1) * (b 2)) - (b 1) * (a 2)
if (i =z 1) then ((a 2) * (b 0)) - (b 2) * (a 0)
else ((a 1) * (b 0)) - (b 1) * (a 0)
fi
Lemma: p2J_wf
∀[a,b:ℙ^2]. p2J(a;b) ∈ ℙ^2 supposing a ≠ b
Lemma: p2J_functionality
∀[a1,b1,a2,b2:ℙ^2]. (p2J(a1;b1) = p2J(a2;b2)) supposing (b1 = b2 and a1 = a2 and a1 ≠ b1)
Lemma: p2J_on
∀[a,b:ℙ^2]. p2J(a;b) on a supposing a ≠ b
Lemma: p2J_symmetry
∀[a,b:ℙ^2]. p2J(a;b) = p2J(b;a) supposing a ≠ b
Lemma: p2J_on_symm
∀[a,b:ℙ^2]. p2J(a;b) on b supposing a ≠ b
Definition: proj-permute
proj-permute(p;f) == p o f
Lemma: proj-permute_wf
∀[n:ℕ]. ∀[p:ℙ^n]. ∀[f:ℕn + 1 ⟶ ℕn + 1]. proj-permute(p;f) ∈ ℙ^n supposing Surj(ℕn + 1;ℕn + 1;f)
Definition: rv-decomp
rv-decomp(rv;x;e) == <x - x ⋅ e*e, x ⋅ e>
Lemma: rv-decomp_wf
∀[rv:InnerProductSpace]. ∀[e,x:Point(rv)].
rv-decomp(rv;x;e) ∈ {p:Point(rv) × ℝ| x ≡ fst(p) + snd(p)*e ∧ (fst(p) ⋅ e = r0)} supposing e^2 = r1
Definition: translation-group-fun
translation-group-fun(rv;e;T) ==
(∀s,t:ℝ. ∀x,y:Point(rv). (T s x # T t y ⇒ (x # y ∨ s ≠ t)))
∧ (∀t,s:ℝ. ∀x:Point(rv). T (t + s) x ≡ T t (T s x))
∧ (∀x:Point(rv). ∀r:ℝ. ∃t:ℝ. (T t x ≡ x + r*e ∧ (∀y:ℝ. (y ≠ t ⇒ T y x # x + r*e))))
∧ (∀x:Point(rv). ∀t:{t:ℝ| r0 ≤ t} . ∃r:{t:ℝ| r0 ≤ t} . T t x ≡ x + r*e)
Lemma: translation-group-fun_wf
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv). (translation-group-fun(rv;e;T) ∈ ℙ)
Definition: trans-apply
T_t(x) == T t x
Lemma: trans-apply_wf
∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv). ∀x:Point(rv). ∀[t:ℝ]. (T_t(x) ∈ Point(rv))
Lemma: trans-apply_functionality
∀[rv:InnerProductSpace]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)].
∀[x1,x2:Point(rv)]. ∀[t1,t2:ℝ]. (T_t1(x1) ≡ T_t2(x2)) supposing ((t1 = t2) and x1 ≡ x2)
supposing ∃e:Point(rv). translation-group-fun(rv;e;T)
Lemma: trans-apply-0
∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
∀x:Point(rv). T_r0(x) ≡ x supposing ∃e:Point(rv). translation-group-fun(rv;e;T)
Lemma: trans-apply-add
∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv). ∀t,s:ℝ.
∀x:Point(rv). T_t + s(x) ≡ T_t(T_s(x)) supposing ∃e:Point(rv). translation-group-fun(rv;e;T)
Lemma: trans-apply-sep
∀rv:InnerProductSpace. ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
((∃e:Point(rv). translation-group-fun(rv;e;T)) ⇒ (∀x:Point(rv). ∀t1,t2:ℝ. (t1 ≠ t2 ⇒ T_t2(x) # T_t1(x))))
Definition: translation-group
translation-group(rv;e;T) == mk-s-subgroup(Perm(rv);fg.∃t:ℝ. ∀x:Point(rv). (fst(fg)) x ≡ T t x)
Lemma: translation-group_wf
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
translation-group(rv;e;T) ∈ s-Group supposing translation-group-fun(rv;e;T)
Lemma: translation-group-point
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
(translation-group-fun(rv;e;T)
⇒ Point(translation-group(rv;e;T)) ≡ {fg:Point(rv) ⟶ Point(rv) × (Point(rv) ⟶ Point(rv))|
∃t:ℝ
((∀x:Point(rv). (fst(fg)) x ≡ T t x)
∧ (∀x:Point(rv). (snd(fg)) x ≡ T -(t) x))} )
Definition: trans-kernel
ρ(h;t) == T_t(h) ⋅ e
Lemma: trans-kernel_wf
∀[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)]. ∀[t:ℝ]. ∀[h:{h:Point(rv)| h ⋅ e = r0} ].
(ρ(h;t) ∈ ℝ)
Lemma: trans-kernel-equation
∀[rv:InnerProductSpace]. ∀[e:{e:Point(rv)| e^2 = r1} ]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)].
∀[t:ℝ]. ∀[h:{h:Point(rv)| h ⋅ e = r0} ]. T_t(h) ≡ h + ρ(h;t)*e supposing translation-group-fun(rv;e;T)
Definition: trans-kernel-fun
trans-kernel-fun(rv;e;f) ==
(∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (f h1 t1 ≠ f h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2)))
∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ((f h r0) = r0))
∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. ((t1 < t2) ⇒ ((f h t1) < (f h t2))))
∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ∃t:ℝ. ((f h t) = r))
Lemma: trans-kernel-fun_wf
∀[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ]. (trans-kernel-fun(rv;e;f) ∈ ℙ)
Lemma: trans-kernel-is-kernel-fun
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
((e^2 = r1) ⇒ translation-group-fun(rv;e;T) ⇒ trans-kernel-fun(rv;e;λh,t. ρ(h;t)))
Lemma: trans-kernel_functionality
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
((e^2 = r1)
⇒ translation-group-fun(rv;e;T)
⇒ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t,s:ℝ. (ρ(h1;t) = ρ(h2;s)) supposing ((t = s) and h1 ≡ h2)))
Lemma: trans-kernel-increasing
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
((e^2 = r1)
⇒ translation-group-fun(rv;e;T)
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t,s:ℝ. ((t < s) ⇒ (ρ(h;t) < ρ(h;s)))))
Lemma: trans-kernel-0
∀rv:InnerProductSpace. ∀e:Point(rv). ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
((e^2 = r1) ⇒ translation-group-fun(rv;e;T) ⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . (ρ(h;r0) = r0)))
Lemma: kernel-fun-properties
∀rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
((e^2 = r1)
⇒ trans-kernel-fun(rv;e;f)
⇒ ((∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((f h1 t1) = (f h2 t2))))
∧ (∀g:h:{h:Point(rv)| h ⋅ e = r0} ⟶ r:ℝ ⟶ ℝ
((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))
⇒ ((∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (g h1 t1 ≠ g h2 t2 ⇒ (h1 # h2 ∨ t1 ≠ t2)))
∧ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . ∀t1,t2:ℝ. (h1 ≡ h2 ⇒ (t1 = t2) ⇒ ((g h1 t1) = (g h2 t2)))))))
∧ (∃g:h:{h:Point(rv)| h ⋅ e = r0} ⟶ r:ℝ ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))))
Definition: separable-kernel
separable-kernel(rv;e;f) ==
∃phi:ℝ ⟶ ℝ. ∃psi:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((phi t) * (psi h)\000C))
Lemma: separable-kernel_wf
∀[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ]. (separable-kernel(rv;e;f) ∈ ℙ)
Lemma: separable-kernel-properties
∀rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∀g:ℝ ⟶ ℝ. ∀k:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ.
((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((g t) * (k h))))
⇒ (∃phi:ℝ ⟶ ℝ
∃psi:{h:Point(rv)| h ⋅ e = r0} ⟶ {r:ℝ| r0 < r}
((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((phi t) * (psi h))))
∧ ((phi r0) = r0)
∧ ((psi 0) = r1)
∧ (∀t,s:ℝ. ((t < s) ⇒ ((phi t) < (phi s))))
∧ (∀t:ℝ. ∃s:ℝ. ((phi s) = t))
∧ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . (psi h1 ≠ psi h2 ⇒ h1 # h2))
∧ (∀t,s:ℝ. (phi t ≠ phi s ⇒ t ≠ s)))))))
Lemma: separable-kernel-iff
∀rv:InnerProductSpace. ∀e:Point(rv). ∀f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (separable-kernel(rv;e;f)
⇐⇒ ∃phi:ℝ ⟶ ℝ
∃psi:{h:Point(rv)| h ⋅ e = r0} ⟶ {r:ℝ| r0 < r}
((∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. ((f h t) = ((phi t) * (psi h))))
∧ ((phi r0) = r0)
∧ ((psi 0) = r1)
∧ (∀t,s:ℝ. ((t < s) ⇒ ((phi t) < (phi s))))
∧ (∀t:ℝ. ∃s:ℝ. ((phi s) = t))
∧ (∀h1,h2:{h:Point(rv)| h ⋅ e = r0} . (psi h1 ≠ psi h2 ⇒ h1 # h2))
∧ (∀t,s:ℝ. (phi t ≠ phi s ⇒ t ≠ s)))))
Definition: trans-from-kernel
trans-from-kernel(rv;e;f;g;t;x) == let h,z = rv-decomp(rv;x;e) in h + f h ((g h z) + t)*e
Lemma: trans-from-kernel_wf
∀[rv:InnerProductSpace]. ∀[e:{e:Point(rv)| e^2 = r1} ]. ∀[f,g:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ]. ∀[t:ℝ].
∀[x:Point(rv)].
(trans-from-kernel(rv;e;f;g;t;x) ∈ Point(rv))
Lemma: trans-from-kernel-sep
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀f,g:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))
⇒ (∀s,t:ℝ. ∀x,y:Point(rv). (trans-from-kernel(rv;e;f;g;s;x) # trans-from-kernel(rv;e;f;g;t;y) ⇒ (x # y ∨ s ≠ t))))
Lemma: trans-from-kernel_functionality
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀f,g:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))
⇒ (∀s,t:ℝ. ∀x,y:Point(rv). ((s = t) ⇒ x ≡ y ⇒ trans-from-kernel(rv;e;f;g;s;x) ≡ trans-from-kernel(rv;e;f;g;t;y))))
Lemma: trans-from-kernel-is-trans
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀f,g:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))
⇒ translation-group-fun(rv;e;λt,x. trans-from-kernel(rv;e;f;g;t;x)))
Lemma: kernel-trans-from-kernel
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀f,g:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀r:ℝ. ((f h (g h r)) = r))
⇒ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. (ρ(h;t) = (f h t))))
Lemma: kernel-fun-is-trans-kernel
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀f:{h:Point(rv)| h ⋅ e = r0} ⟶ ℝ ⟶ ℝ.
(trans-kernel-fun(rv;e;f)
⇒ (∃T:ℝ ⟶ Point(rv) ⟶ Point(rv)
(translation-group-fun(rv;e;T) ∧ (∀h:{h:Point(rv)| h ⋅ e = r0} . ∀t:ℝ. (ρ(h;t) = (f h t))))))
Definition: separable-translation-group
separable-translation-group(rv;e;T) == translation-group-fun(rv;e;T) ∧ separable-kernel(rv;e;λh,t. ρ(h;t))
Lemma: separable-translation-group_wf
∀[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[T:ℝ ⟶ Point(rv) ⟶ Point(rv)]. (separable-translation-group(rv;e;T) ∈ ℙ)
Lemma: separable-translation-group_iff
∀rv:InnerProductSpace. ∀e:{e:Point(rv)| e^2 = r1} . ∀T:ℝ ⟶ Point(rv) ⟶ Point(rv).
(translation-group-fun(rv;e;T)
⇒ (separable-translation-group(rv;e;T)
⇐⇒ (∀a:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} . (a ≠ r0 ⇒ (r0 < ||T_a(h) - h||)))
∧ (∀a,b:ℝ. ∀h:{h:Point(rv)| h ⋅ e = r0} .
(a ≠ r0 ⇒ b ≠ r0 ⇒ ((||T_a(h) - h||/||T_b(h) - h||) = (||T_a(0)||/||T_b(0)||))))))
Definition: hyptrans
hyptrans(rv;e;t;x) == x + (x ⋅ e * (cosh(t) - r1)) + (rsqrt(r1 + x^2) * sinh(t))*e
Lemma: hyptrans_wf
∀[rv:InnerProductSpace]. ∀[e,x:Point(rv)]. ∀[t:ℝ]. (hyptrans(rv;e;t;x) ∈ Point(rv))
Lemma: hyptrans_functionality
∀[rv:InnerProductSpace]. ∀[e1,x1:Point(rv)]. ∀[t1:ℝ]. ∀[e2,x2:Point(rv)]. ∀[t2:ℝ].
(hyptrans(rv;e1;t1;x1) ≡ hyptrans(rv;e2;t2;x2)) supposing (x1 ≡ x2 and e1 ≡ e2 and (t1 = t2))
Lemma: hyptrans_lemma
∀[rv:InnerProductSpace]. ∀[e,h:Point(rv)].
∀tau,t:ℝ. hyptrans(rv;e;t;h + sinh(tau) * rsqrt(r1 + h^2)*e) ≡ h + sinh(tau + t) * rsqrt(r1 + h^2)*e
supposing (e^2 = r1) ∧ (h ⋅ e = r0)
Lemma: hyptrans_decomp
∀rv:InnerProductSpace. ∀e,x:Point(rv).
∃h:Point(rv). ∃tau:ℝ. ((h ⋅ e = r0) ∧ x ≡ h + sinh(tau) * rsqrt(r1 + h^2)*e) supposing e^2 = r1
Lemma: hyptrans_add
∀[rv:InnerProductSpace]. ∀[e,x:Point(rv)]. ∀[t,s:ℝ].
hyptrans(rv;e;t + s;x) ≡ hyptrans(rv;e;t;hyptrans(rv;e;s;x)) supposing e^2 = r1
Lemma: hyptrans_ext
∀rv:InnerProductSpace. ∀e:Point(rv). ∀s,t:ℝ. ∀x,y:Point(rv).
(hyptrans(rv;e;s;x) # hyptrans(rv;e;t;y) ⇒ (x # y ∨ s ≠ t))
Lemma: hyptrans_0
∀[rv:InnerProductSpace]. ∀[e,x:Point(rv)]. hyptrans(rv;e;r0;x) ≡ x
Lemma: hyptrans-is-translation-group-fun
∀rv:InnerProductSpace. ∀e:Point(rv). ((e^2 = r1) ⇒ translation-group-fun(rv;e;λt,x. hyptrans(rv;e;t;x)))
Definition: hyptrans-perm
hyptrans-perm(rv;e;t) == <λx.hyptrans(rv;e;t;x), λx.hyptrans(rv;e;-(t);x)>
Lemma: hyptrans-perm_wf
∀[rv:InnerProductSpace]. ∀[e:Point(rv)]. ∀[t:ℝ].
hyptrans-perm(rv;e;t) ∈ Point(translation-group(rv;e;λt,x. hyptrans(rv;e;t;x))) supposing e^2 = r1
Lemma: hyp-distance-lemma1
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (r1 ≤ ((rsqrt(r1 + x^2) * rsqrt(r1 + y^2)) - x ⋅ y))
Definition: hyp-dist
hyp (x,y) == inv-cosh((rsqrt(r1 + x^2) * rsqrt(r1 + y^2)) - x ⋅ y)
Lemma: hyp-dist_wf
∀[rv:InnerProductSpace]. ∀[x,y:Point(rv)]. (hyp (x,y) ∈ ℝ)
Definition: topspace
Space == X:Type × E:X ⟶ X ⟶ ℙ × EquivRel(X;x,y.E x y)
Lemma: topspace_wf
Space ∈ 𝕌'
Definition: toptype
|X| == fst(X)
Lemma: toptype_wf
∀[X:Space]. (|X| ∈ Type)
Definition: topeq
topeq(X;a;b) == (fst(snd(X))) a b
Lemma: topeq_wf
∀[X:Space]. ∀[a,b:|X|]. (topeq(X;a;b) ∈ ℙ)
Lemma: topeq-equiv
∀X:Space. EquivRel(|X|;a,b.topeq(X;a;b))
Lemma: topeq_weakening
∀X:Space. ∀a,b:|X|. ((a = b ∈ |X|) ⇒ topeq(X;a;b))
Lemma: topeq_inversion
∀X:Space. ∀a,b:|X|. (topeq(X;a;b) ⇒ topeq(X;b;a))
Lemma: topeq_transitivity
∀X:Space. ∀a,b,c:|X|. (topeq(X;a;b) ⇒ topeq(X;b;c) ⇒ topeq(X;a;c))
Definition: topfun
topfun(X;Y) == {f:|X| ⟶ |Y|| ∀a,b:|X|. (topeq(X;a;b) ⇒ topeq(Y;f a;f b))}
Lemma: topfun_wf
∀[X,Y:Space]. (topfun(X;Y) ∈ Type)
Definition: topfuneq
topfuneq(X;Y;f;g) == ∀x:|X|. topeq(Y;f x;g x)
Lemma: topfuneq_wf
∀[X,Y:Space]. ∀[f,g:topfun(X;Y)]. (topfuneq(X;Y;f;g) ∈ ℙ)
Lemma: topfuneq-equiv
∀X,Y:Space. EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
Definition: tfunequiv
tfunequiv(X;Y) ==
<λa,x. let _,_,refl,_,_ = Y in refl (a x)
, λa,b,%,x. let _,_,_,sym,_ = Y in sym (a x) (b x) (% x)
, λa,b,c,%,%2,x. let _,_,_,_,trans = Y in trans (a x) (b x) (c x) (% x) (%2 x)>
Lemma: topfuneq-equiv-ext
∀X,Y:Space. EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g))
Lemma: tfunequiv_wf
∀X,Y:Space. (tfunequiv(X;Y) ∈ EquivRel(topfun(X;Y);f,g.topfuneq(X;Y;f;g)))
Definition: funspace
funspace(X;Y) == <topfun(X;Y), λf,g. topfuneq(X;Y;f;g), tfunequiv(X;Y)>
Lemma: funspace_wf
∀[X,Y:Space]. (funspace(X;Y) ∈ Space)
Definition: mktopspace
mktopspace(T;E;equiv) == <T, E, equiv>
Lemma: mktopspace_wf
∀[T:Type]. ∀[E:T ⟶ T ⟶ ℙ]. ∀[equiv:EquivRel(T;x,y.E x y)]. (mktopspace(T;E;equiv) ∈ Space)
Definition: realspace
realspace() == mktopspace(ℝ;λx,y. (x = y);TERMOF{req-equiv:o, 1:l})
Lemma: realspace_wf
realspace() ∈ Space
Home
Index