:: The Euclidean Space
:: by Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, FINSEQ_2, FINSEQ_1, SUBSET_1, FUNCT_1, COMPLEX1,
REAL_1, VALUED_0, RELAT_1, TARSKI, CARD_1, ARYTM_1, ARYTM_3, RVSUM_1,
SQUARE_1, CARD_3, XXREAL_0, XCMPLX_0, ZFMISC_1, VALUED_1, PCOMPS_1,
STRUCT_0, METRIC_1, XBOOLE_0, RLTOPSP1, PRE_TOPC, RLVECT_1, FUNCSDOM,
SETFAM_1, ALGSTR_0, FUNCT_2, MONOID_0, BINOP_2, FUNCOP_1, SUPINF_2,
MCART_1, EUCLID, VALUED_2, JORDAN2C, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, SETFAM_1, XREAL_0, COMPLEX1, NAT_1, RELAT_1, FUNCT_1, VALUED_0,
STRUCT_0, METRIC_1, FUNCT_2, BINOP_1, BINOP_2, FUNCOP_1, REAL_1,
VALUED_1, FINSEQ_1, FINSEQ_2, FINSEQOP, SQUARE_1, RVSUM_1, VALUED_2,
MONOID_0, PRE_TOPC, PCOMPS_1, TOPMETR, XXREAL_0, ALGSTR_0, RLVECT_1,
FUNCSDOM, RLTOPSP1;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, FINSEQOP, PCOMPS_1,
MONOID_0, TOPMETR, RLTOPSP1, FUNCSDOM, VALUED_2, NUMBERS;
registrations XBOOLE_0, FUNCT_1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0,
FINSEQ_2, RVSUM_1, METRIC_1, PCOMPS_1, MONOID_0, VALUED_0, VALUED_1,
STRUCT_0, TOPMETR, RLTOPSP1, CARD_1, SQUARE_1, ORDINAL1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions FINSEQ_1, PCOMPS_1, VALUED_2, CARD_1;
equalities FINSEQ_1, STRUCT_0, PCOMPS_1, SQUARE_1, FINSEQ_2, RVSUM_1,
VALUED_1, FUNCSDOM, RLVECT_1;
expansions MONOID_0;
theorems ABSVALUE, BINOP_1, FINSEQ_1, FINSEQ_2, FINSEQOP, FUNCT_1, FUNCT_2,
PCOMPS_1, RVSUM_1, SQUARE_1, TARSKI, XREAL_0, COMPLEX1, XREAL_1,
XXREAL_0, FUNCOP_1, ORDINAL1, VALUED_1, RELAT_1, PRE_TOPC, TOPMETR,
RSSPACE, RLVECT_1, ALGSTR_0, FUNCSDOM, PARTFUN1, RFUNCT_1, CARD_1;
schemes FUNCT_2, BINOP_1;
begin
reserve k,j,n for Nat,
r for Real;
definition
let n be Nat;
func REAL n -> FinSequenceSet of REAL equals
n-tuples_on REAL;
coherence;
end;
registration
let n be Nat;
cluster REAL n -> non empty;
coherence;
end;
registration
let n;
cluster -> n-element for Element of REAL n;
coherence;
end;
definition
func absreal -> Function of REAL,REAL means
:Def2:
for r holds it.r = |.r.|;
existence
proof
deffunc F(Real) = In(|.$1.|,REAL);
consider f be Function of REAL,REAL such that
A1: for r be Element of REAL holds f.r = F(r) from FUNCT_2:sch 4;
take f;
let r;
r in REAL by XREAL_0:def 1;
hence f.r = In(|.r.|,REAL) by A1
.= |.r.|;
end;
uniqueness
proof
let f, g be Function of REAL,REAL such that
A2: for r holds f.r = |.r.| and
A3: for r holds g.r = |.r.|;
now
let x be Element of REAL;
thus f.x = |.x.| by A2
.= g.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
definition
let x be real-valued FinSequence;
redefine func abs x -> FinSequence of REAL equals :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
absreal*x;
coherence
proof
thus rng abs x c= REAL;
end;
compatibility
proof
set g = absreal*x;
dom absreal = REAL by FUNCT_2:def 1;
then rng x c= dom absreal;
then
A1: dom abs x = dom x & dom g = dom x by RELAT_1:27,VALUED_1:def 11;
now
let a be object;
assume
A2: a in dom abs x;
thus (abs x).a = |.x . a.| by VALUED_1:18
.= absreal.(x . a) by Def2
.= g.a by A1,A2,FUNCT_1:12;
end;
hence thesis by A1,FUNCT_1:2;
end;
end;
definition
let n;
func 0*n -> real-valued FinSequence equals
n |-> In(0,REAL);
coherence;
end;
definition
let n;
redefine func 0*n -> Element of REAL n; :: redefines 0* (EUCLID, definition)
coherence;
end;
reserve x,x1,x2,y for Element of REAL n;
definition
let n,x;
redefine func -x -> Element of REAL n; :: redefines - (VALUED_1, definition)
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider R1=x as Element of n-tuples_on REAL;
-R1 in n-tuples_on REAL;
hence thesis;
end;
end;
definition
let n,x,y;
redefine func x + y -> Element of REAL n; :: redefines + (VALUED_1, definition)
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider R1=x,R2=y as Element of n-tuples_on REAL;
R1 + R2 in n-tuples_on REAL;
hence thesis;
end;
redefine func x - y -> Element of REAL n; :: redefines - (VALUED_1, definition)
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider R1=x,R2=y as Element of n-tuples_on REAL;
R1 - R2 in n-tuples_on REAL;
hence thesis;
end;
end;
definition
let n, x;
let r be Real;
redefine func r*x -> Element of REAL n; :: redefines * (RVSUM_1, synonym) → (#) (VALUED_1, definition)
coherence
proof
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider R=x as Element of n-tuples_on REAL;
r*R in n-tuples_on REAL;
hence thesis;
end;
end;
definition
let n,x;
redefine func abs x -> Element of n-tuples_on REAL; :: redefines abs (VALUED_1, synonym) → |. (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
definition
let n,x;
redefine func sqr x -> Element of n-tuples_on REAL; :: redefines sqr (RVSUM_1, synonym) → ^2 (VALUED_1, definition)
coherence by FINSEQ_2:113;
end;
reserve f for real-valued FinSequence;
definition
let f;
func |. f .| -> Real equals
sqrt Sum sqr f;
coherence;
end;
Lm1: f is Element of REAL len f
proof
rng f c= REAL;
then f is FinSequence of REAL by FINSEQ_1:def 4;
then f is Element of REAL* by FINSEQ_1:def 11;
then f in (len f)-tuples_on REAL;
hence thesis;
end;
::$CT 3
theorem
abs 0*n = n |-> (0 qua Real)
proof
reconsider m=n as Element of NAT by ORDINAL1:def 12;
thus abs 0*n = m |-> absreal.(0 qua Real) by FINSEQOP:16
.= n |-> |.0 .| by Def2
.= n |-> 0 by ABSVALUE:2;
end;
theorem Th2:
for f being complex-valued Function holds abs -f = abs f
proof
let f be complex-valued Function;
A1: dom abs(-f) = dom(-f) by VALUED_1:def 11;
A2: dom abs(f) = dom f by VALUED_1:def 11;
A3: dom -f = dom f by VALUED_1:8;
now
let x be object;
assume x in dom abs(-f);
thus abs(-f).x = |.(-f).x.| by VALUED_1:18
.= |.-f.x.| by VALUED_1:8
.= |.f.x.| by COMPLEX1:52
.= abs(f).x by VALUED_1:18;
end;
hence thesis by A1,A2,A3,FUNCT_1:2;
end;
theorem Th3:
abs(r*f) = |.r.|*(abs f) by RFUNCT_1:25;
theorem Th4:
|.0*n.| = 0
proof
thus |.0*n .| = sqrt Sum (n |-> 0^2) by RVSUM_1:56
.= sqrt (n*0) by RVSUM_1:80
.= 0;
end;
Lm2: sqr abs f = sqr f
proof
set n = len f;
reconsider x=f as Element of REAL n by Lm1;
now
let k;
assume k in Seg n;
thus (sqr abs x).k = ((abs x).k)^2 by VALUED_1:11
.= |.x .k.|^2 by VALUED_1:18
.= (x .k)^2 by COMPLEX1:75
.= (sqr x).k by VALUED_1:11;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th5:
|. x .| = 0 implies x = 0*n
proof
assume
A1: |. x .| = 0;
now
let j;
assume
j in Seg n;
reconsider r = x .j as Element of REAL by XREAL_0:def 1;
Sum sqr x = 0 by A1,RVSUM_1:86,SQUARE_1:24;
then Sum sqr abs x = 0 by Lm2;
then (abs x).j = (n|->0).j by RVSUM_1:91;
then |.r.| = (n|-> 0).j by VALUED_1:18;
then |.r.| = 0;
then r = 0 by ABSVALUE:2;
hence x .j = (n|->(0 qua Real)).j;
end;
hence thesis by FINSEQ_2:119;
end;
theorem Th6:
|.f.| >= 0
proof
0 <= Sum sqr f by RVSUM_1:86;
hence thesis by SQUARE_1:def 2;
end;
registration
let f;
cluster |.f.| -> non negative;
coherence by Th6;
end;
theorem Th7:
|.-f.| = |.f.|
proof
thus |.-f.| = sqrt Sum sqr abs -f by Lm2
.= sqrt Sum sqr abs f by Th2
.= |.f.| by Lm2;
end;
theorem
|.r*f.| = |.r.|*|.f.|
proof
set n = len f;
reconsider x=f as Element of REAL n by Lm1;
A1: 0 <= (|.r.|)^2 & 0 <= Sum sqr abs x by RVSUM_1:86,XREAL_1:63;
thus |.r*f.| = sqrt Sum sqr abs(r*x) by Lm2
.= sqrt Sum sqr (|.r.|*abs x) by Th3
.= sqrt Sum ((|.r.|)^2 * sqr abs x) by RVSUM_1:58
.= sqrt ((|.r.|)^2 * Sum sqr abs x) by RVSUM_1:87
.= sqrt (|.r.|)^2 * sqrt Sum sqr abs x by A1,SQUARE_1:29
.= |.r.| * sqrt Sum sqr abs x by COMPLEX1:46,SQUARE_1:22
.= |.r.|*|.f.| by Lm2;
end;
::$N The Triangle Inequality
::$L https://en.wikipedia.org/wiki/Triangle_inequality The Triangle Inequality
theorem Th9:
|.x1 + x2.| <= |.x1.| + |.x2.|
proof
A1: 0 <= Sum sqr (x1 + x2) by RVSUM_1:86;
A2: 0 <= Sum sqr abs x1 by RVSUM_1:86;
then
A3: 0 <= sqrt Sum sqr abs x1 by SQUARE_1:def 2;
A4: k in Seg n implies (sqr abs (x1 + x2)).k <= (sqr (abs x1 + abs x2)).k
proof
len (x1+x2) = n by CARD_1:def 7;
then
A5: dom (x1+x2) = Seg n by FINSEQ_1:def 3;
assume
A6: k in Seg n;
reconsider abs1 = (abs x1).k, abs2 = (abs x2).k as Real;
reconsider r12 = (x1 + x2).k as Element of REAL by XREAL_0:def 1;
reconsider r11 = x1.k, r22 = x2.k as Element of REAL by XREAL_0:def 1;
|.r11 + r22.| <= |.r11.| + |.r22.| by COMPLEX1:56;
then |.r12.| <= |.r11.| + |.r22.| by A6,A5,VALUED_1:def 1;
then |.r12.| <= |.r11.| + abs2 by VALUED_1:18;
then
A7: |.r12.| <= abs1 + abs2 by VALUED_1:18;
reconsider abs912 = (abs (x1 + x2)).k as Real;
reconsider abs12 = (abs x1 + abs x2).k as Real;
set r2 = (sqr (abs x1 + abs x2)).k;
|.r12.| >= 0 by COMPLEX1:46;
then
A8: 0 <= abs912 by VALUED_1:18;
len(abs x1 + abs x2) = n by CARD_1:def 7;
then dom(abs x1 + abs x2) = Seg n by FINSEQ_1:def 3;
then |.r12.| <= abs12 by A6,A7,VALUED_1:def 1;
then abs912 <= abs12 by VALUED_1:18;
then (abs912)^2 <= (abs12)^2 by A8,SQUARE_1:15;
then (abs912)^2 <= r2 by VALUED_1:11;
hence thesis by VALUED_1:11;
end;
0 <= (Sum mlt(abs x1,abs x2))^2 by XREAL_1:63;
then
A9: sqrt(Sum mlt(abs x1,abs x2))^2 <= sqrt((Sum sqr abs x1)*(Sum sqr abs x2
)) by RVSUM_1:92,SQUARE_1:26;
A10: k in Seg n implies 0 <= (mlt(abs x1,abs x2)).k
proof
assume k in Seg n;
set r = (mlt(abs x1,abs x2)).k;
reconsider r1 = x1.k, r2 = x2.k as Element of REAL by XREAL_0:def 1;
(abs x1).k = |.r1.| & (abs x2).k = |.r2.| by VALUED_1:18;
then
A11: r = |.r1.|*|.r2.| by RVSUM_1:60;
0 <= |.r1.| & 0 <= |.r2.| by COMPLEX1:46;
hence thesis by A11;
end;
len mlt(abs x1,abs x2) = n by CARD_1:def 7;
then dom mlt(abs x1,abs x2) = Seg n by FINSEQ_1:def 3;
then Sum mlt(abs x1,abs x2) <= sqrt((Sum sqr abs x1)*(Sum sqr abs x2)) by A10
,A9,RVSUM_1:84,SQUARE_1:22;
then 2*Sum mlt(abs x1,abs x2) <= 2*sqrt((Sum sqr abs x1)*(Sum sqr abs x2))
by XREAL_1:64;
then
Sum sqr abs x1+(2*Sum mlt(abs x1,abs x2)) <= Sum sqr abs x1+2*sqrt((Sum
sqr abs x1)*(Sum sqr abs x2)) by XREAL_1:7;
then
A12: Sum sqr abs x1+(2*Sum mlt(abs x1,abs x2)) + Sum sqr abs x2 <= Sum sqr
abs x1+2*sqrt((Sum sqr abs x1)*(Sum sqr abs x2)) + Sum sqr abs x2 by
XREAL_1:7;
A13: 0 <= Sum sqr abs x2 by RVSUM_1:86;
then
A14: 0 <= sqrt Sum sqr abs x2 by SQUARE_1:def 2;
Sum sqr (abs x1 + abs x2) = Sum (sqr abs x1 + 2*mlt(abs x1,abs x2) + sqr
abs x2) by RVSUM_1:68
.= Sum(sqr abs x1 + 2*mlt(abs x1,abs x2)) + Sum sqr abs x2 by RVSUM_1:89
.= Sum sqr abs x1 + Sum(2*mlt(abs x1,abs x2)) + Sum sqr abs x2 by
RVSUM_1:89
.= Sum sqr abs x1 + (2*Sum mlt(abs x1,abs x2))+Sum sqr abs x2 by RVSUM_1:87
;
then Sum sqr abs (x1 + x2) <= Sum sqr abs x1 + (2*Sum mlt(abs x1,abs x2))+
Sum sqr abs x2 by A4,RVSUM_1:82;
then Sum sqr (x1 + x2) <= Sum sqr abs x1 + (2*Sum mlt(abs x1,abs x2))+Sum
sqr abs x2 by Lm2;
then Sum sqr (x1 + x2) <= Sum sqr abs x1+2*sqrt((Sum sqr abs x1)*(Sum sqr
abs x2)) + Sum sqr abs x2 by A12,XXREAL_0:2;
then
A15: Sum sqr (x1 + x2) <= Sum sqr abs x1+2*((sqrt Sum sqr abs x1)*(sqrt Sum
sqr abs x2)) + Sum sqr abs x2 by A2,A13,SQUARE_1:29;
A16: (sqrt Sum sqr abs x2)^2 = Sum sqr abs x2 by A13,SQUARE_1:def 2;
Sum sqr abs x1 = (sqrt Sum sqr abs x1)^2 by A2,SQUARE_1:def 2;
then sqrt Sum sqr (x1 + x2) <= sqrt(((sqrt Sum sqr abs x1) + (sqrt Sum sqr
abs x2))^2) by A15,A16,A1,SQUARE_1:26;
then
sqrt Sum sqr (x1 + x2) <= (sqrt Sum sqr abs x1) + (sqrt Sum sqr abs x2)
by A3,A14,SQUARE_1:22;
then sqrt Sum sqr (x1 + x2) <= (sqrt Sum sqr abs x1) + (sqrt Sum sqr x2) by
Lm2;
hence thesis by Lm2;
end;
theorem Th10:
|.x1 - x2.| <= |.x1.| + |.x2.|
proof
|.x1 - x2.| <= |.x1.| + |.-x2.| by Th9;
hence thesis by Th7;
end;
theorem
|.x1.| - |.x2.| <= |.x1 + x2.|
proof
reconsider R1=x1,R2=x2 as Element of n-tuples_on REAL;
x1 = R1 + R2 - R2 by RVSUM_1:42;
then |.x1.| <= |.x1 + x2.| + |.x2.| by Th10;
hence thesis by XREAL_1:20;
end;
theorem
|.x1.| - |.x2.| <= |.x1 - x2.|
proof
reconsider R1=x1,R2=x2 as Element of n-tuples_on REAL;
x1 = R1 - R2 + R2 by RVSUM_1:43;
then |.x1.| <= |.x1 - x2.| + |.x2.| by Th9;
hence thesis by XREAL_1:20;
end;
theorem Th13:
|.x1 - x2.| = 0 iff x1 = x2
proof
reconsider R1=x1,R2=x2 as Element of n-tuples_on REAL;
thus |.x1 - x2.| = 0 implies x1 = x2
proof
assume |.x1 - x2.| = 0;
then R1 - R2 = 0*n by Th5
.= n |-> 0;
hence thesis by RVSUM_1:38;
end;
assume x1 = x2;
then R1 - R2 = 0*n by RVSUM_1:37;
hence thesis by Th4;
end;
registration
let n,x1;
cluster |. x1 - x1 .| -> zero;
coherence by Th13;
end;
theorem
x1 <> x2 implies |.x1 - x2.| > 0
proof
assume x1 <> x2;
then 0 <> |.x1 - x2.| by Th13;
hence thesis;
end;
theorem Th15:
|.x1 - x2.| = |.x2 - x1.|
proof
reconsider R1=x1,R2=x2 as Element of n-tuples_on REAL;
thus |.x1 - x2.| = |.-(R2 - R1).| by RVSUM_1:35
.= |.x2 - x1.| by Th7;
end;
theorem Th16:
|.x1 - x2.| <= |.x1 - x .| + |.x - x2.|
proof
reconsider R1=x1,R2=x2,R=x as Element of n-tuples_on REAL;
|.x1 - x2.| = |.R1 - R + R - R2.| by RVSUM_1:43
.= |.(x1 - x) + (x - x2).| by RVSUM_1:40;
hence thesis by Th9;
end;
definition
let n be Nat;
func Pitag_dist n -> Function of [:REAL n,REAL n:],REAL means
:Def6:
for x,y being Element of REAL n holds it.(x,y) = |.x-y.|;
existence
proof
deffunc F(Element of REAL n, Element of REAL n) = In(|.$1-$2.|,REAL);
consider f being Function of [:REAL n, REAL n:], REAL such that
A1: for x,y being Element of REAL n holds f.(x,y) = F(x,y) from
BINOP_1:sch 4;
take f;
let x,y be Element of REAL n;
f.(x,y) = F(x,y) by A1;
hence thesis;
end;
uniqueness
proof
let f,g be Function of [:REAL n, REAL n:], REAL;
assume that
A2: for x,y being Element of REAL n holds f.(x,y) = |.x-y.| and
A3: for x,y being Element of REAL n holds g.(x,y) = |.x-y.|;
reconsider n as Element of NAT by ORDINAL1:def 12;
reconsider f,g as Function of [:REAL n, REAL n:], REAL;
now
let x,y be Element of REAL n;
thus f.(x,y) = |.x-y.| by A2
.= g.(x,y) by A3;
end;
hence thesis by BINOP_1:2;
end;
end;
theorem
for x, y being real-valued FinSequence holds sqr(x-y) = sqr(y-x)
proof
let x, y be real-valued FinSequence;
thus (x-y)^2 = x^2 - 2(#)(x(#)y) + y^2 by RVSUM_1:69
.= sqr y + (- 2*mlt(x,y) + sqr x)
.= sqr y - 2*mlt(y,x) + sqr x by RFUNCT_1:8
.= sqr(y-x) by RVSUM_1:69;
end;
theorem Th18:
for n being Nat holds Pitag_dist n is_metric_of REAL n
proof
let n be Nat;
let x,y,z be Element of REAL n;
A1: (Pitag_dist n).(y,z) = |.y-z.| by Def6;
(Pitag_dist n).(x,y) = |.x-y.| by Def6;
hence (Pitag_dist n).(x,y) = 0 iff x=y by Th13;
thus (Pitag_dist n).(x,y) = |.x-y.| by Def6
.= |.y-x .| by Th15
.= (Pitag_dist n).(y,x) by Def6;
(Pitag_dist n).(x,y) = |.x-y.| & (Pitag_dist n).(x,z) = |.x-z.| by Def6;
hence (Pitag_dist n).(x,z) <= (Pitag_dist n).(x,y) + (Pitag_dist n).(y,z) by
A1,Th16;
end;
definition
let n be Nat;
func Euclid n -> strict MetrSpace equals
MetrStruct(#REAL n,Pitag_dist n#);
coherence
proof
SpaceMetr(REAL n, Pitag_dist n) = MetrStruct(#REAL n,Pitag_dist n#) by Th18
,PCOMPS_1:def 7;
hence thesis;
end;
end;
registration
let n be Nat;
cluster Euclid n -> non empty;
coherence;
end;
definition
let n be Nat;
func TOP-REAL n -> strict RLTopStruct means
:Def8:
the TopStruct of it =
TopSpaceMetr Euclid n & the RLSStruct of it = RealVectSpace Seg n;
existence
proof
set V = RealVectSpace Seg n, T = TopSpaceMetr Euclid n;
reconsider t = the topology of T as Subset-Family of the carrier of V by
FINSEQ_2:93;
take S = RLTopStruct (# the carrier of V, the ZeroF of V, the addF of V,
the Mult of V, t #);
thus the TopStruct of S = TopSpaceMetr Euclid n by FINSEQ_2:93;
thus the RLSStruct of S = RealVectSpace Seg n;
end;
uniqueness;
end;
registration
let n be Nat;
cluster TOP-REAL n -> non empty;
coherence
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
hence thesis;
end;
end;
registration
let n be Nat;
cluster TOP-REAL n -> TopSpace-like Abelian add-associative right_zeroed
right_complementable vector-distributive scalar-distributive
scalar-associative scalar-unital;
coherence
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
hence TOP-REAL n is TopSpace-like by PRE_TOPC:28;
the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
hence thesis by RSSPACE:15;
end;
end;
reserve p,p1,p2,p3 for Point of TOP-REAL n,
x,x1,x2,y,y1,y2 for Real;
theorem Th19:
the carrier of TOP-REAL n = REAL n
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
hence thesis;
end;
theorem Th20:
p is Function of Seg n, REAL
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
then p is Element of Funcs(Seg n,REAL) by FINSEQ_2:93;
hence thesis;
end;
theorem Th21:
p is FinSequence of REAL
proof
p is Function of Seg n, REAL by Th20;
hence thesis by FINSEQ_2:25;
end;
registration
let n;
cluster TOP-REAL n -> constituted-FinSeqs;
coherence
by Th21;
end;
registration
let n;
cluster -> FinSequence-like for Point of TOP-REAL n;
coherence;
end;
registration
let n;
cluster -> real-valued for Point of TOP-REAL n;
coherence by Th21;
end;
Lm3: for r1,r2 being real-valued Function st p1 = r1 & p2 =r2 holds p1+p2 = r1
+r2
proof
A1: REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
let r1,r2 be real-valued Function such that
A2: p1 = r1 & p2 =r2;
reconsider s1 = r1, s2 = r2 as Element of REAL n by A2,Th19;
the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
hence p1+p2 = (RealFuncAdd Seg n).(r1,r2) by A2,ALGSTR_0:def 1
.= s1+s2 by A1,FUNCSDOM:def 1
.= r1+r2;
end;
Lm4: for r being real-valued Function st p = r holds x*p = x(#)r
proof
reconsider x1 = x as Real;
let r be real-valued Function such that
A1: p = r;
reconsider s=r as Element of REAL n by A1,Th19;
REAL n = Funcs(Seg n,REAL) by FINSEQ_2:93;
then reconsider f = s as Function of Seg n,REAL by FUNCT_2:66;
the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
hence x*p = multreal[;](x1,f) by A1,FUNCSDOM:def 3
.= multreal[;](x,(id REAL)*f) by PARTFUN1:7
.= x*s by FUNCOP_1:34
.= x(#)r;
end;
registration
let r,s be Real;
let n;
let p be Element of TOP-REAL n;
let f be real-valued FinSequence;
identify r*p with s*f when r=s, p=f;
compatibility by Lm4;
end;
registration
let n;
let p,q be Element of TOP-REAL n;
let f,g be real-valued FinSequence;
identify p+q with f+g when p=f, q=g;
compatibility by Lm3;
end;
registration
let n;
let p be Element of TOP-REAL n;
let f be real-valued FinSequence;
identify -p with -f when p=f;
compatibility
proof
assume
A1: p=f;
thus -p = (-1)*p by RLVECT_1:16
.= -f by A1;
end;
end;
registration
let n;
let p,q be Element of TOP-REAL n;
let f,g be real-valued FinSequence;
identify p-q with f-g when p=f, q=g;
compatibility;
end;
registration
let n;
cluster -> n-element for Point of TOP-REAL n;
coherence
proof
let p be Point of TOP-REAL n;
A1: p is Function of Seg n, REAL by Th20;
Seg len p = dom p by FINSEQ_1:def 3
.= Seg n by A1,FUNCT_2:def 1;
hence len p = n by FINSEQ_1:6;
end;
end;
notation
let n;
synonym 0.REAL n for 0*n;
end;
definition
let n;
redefine func 0.REAL n -> Point of TOP-REAL n; :: redefines 0.REAL (EUCLID, synonym) → 0* (EUCLID, definition)
coherence
proof
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
hence thesis;
end;
end;
theorem
for x being Element of REAL n holds sqr abs x = sqr x by Lm2;
::$CT 25
reserve p,p1,p2 for Point of TOP-REAL 2;
theorem
ex x,y being Element of REAL st p=<*x,y*>
proof
the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by Def8;
then p is Tuple of 2,REAL by FINSEQ_2:131;
hence thesis by FINSEQ_2:100;
end;
definition
let p;
func p`1 -> Real equals
p.1;
coherence;
func p`2 -> Real equals
p.2;
coherence;
end;
notation
let x,y be Real;
synonym |[ x,y ]| for <*x,y*>;
end;
definition
let x,y be Real;
redefine func |[ x,y ]| -> Point of TOP-REAL 2; :: redefines |[ (EUCLID, synonym) → <* (FINSEQ_1, definition)
coherence
proof
A1: y in REAL by XREAL_0:def 1;
the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 & x in REAL by Def8,
XREAL_0:def 1;
hence thesis by A1,FINSEQ_2:101;
end;
end;
theorem
|[x,y]|`1 = x & |[x,y]|`2 = y by FINSEQ_1:44;
theorem Th25:
p = |[p`1, p`2]|
proof
the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by Def8;
then p is Tuple of 2,REAL by FINSEQ_2:131;
then consider x,y be Element of REAL such that
A1: p = <* x,y *> by FINSEQ_2:100;
p`1 = x by A1,FINSEQ_1:44;
hence thesis by A1,FINSEQ_1:44;
end;
theorem
0.TOP-REAL 2 = |[0,0]|
proof
the RLSStruct of TOP-REAL 2 = RealVectSpace Seg 2 & 0.REAL 2 = |[0,0]|
by Def8,FINSEQ_2:61;
hence thesis;
end;
theorem Th27:
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]|
proof
the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by Def8;
then reconsider p19=p1, p29=p2 as Element of REAL 2;
len(p19+p29) = 2 by CARD_1:def 7;
then
A1: dom(p19+p29) = Seg 2 by FINSEQ_1:def 3;
2 in {1,2} by TARSKI:def 2;
then
A2: (p1+p2)`2 = p1`2 + p2`2 by A1,FINSEQ_1:2,VALUED_1:def 1;
1 in {1,2} by TARSKI:def 2;
then (p1+p2)`1 = p1`1 + p2`1 by A1,FINSEQ_1:2,VALUED_1:def 1;
hence thesis by A2,Th25;
end;
theorem
|[x1, y1]| + |[x2, y2]| = |[ x1 + x2, y1 + y2]|
proof
A1: |[x2, y2]|`1 = x2 & |[x2, y2]|`2 = y2 by FINSEQ_1:44;
|[x1, y1]|`1 = x1 & |[x1, y1]|`2 = y1 by FINSEQ_1:44;
hence thesis by A1,Th27;
end;
theorem Th29:
x*p = |[ x*p`1 ,x*p`2 ]|
proof
(x*p)`1 = x*(p`1) & (x*p)`2 = x*(p`2) by RVSUM_1:44;
hence thesis by Th25;
end;
theorem
x*|[x1,y1]| = |[ x*x1,x*y1 ]|
proof
|[x1,y1]|`1 = x1 & |[x1,y1]|`2 = y1 by FINSEQ_1:44;
hence thesis by Th29;
end;
theorem Th31:
-p = |[ -p`1, -p`2]|
proof
thus -p = (-1)*p .= |[ (-1)*p`1, (-1)*p`2]| by Th29
.= |[ -p`1, -p`2]|;
end;
theorem
-|[x1,y1]| = |[ -x1, -y1]|
proof
|[x1,y1]|`1 = x1 & |[x1,y1]|`2 = y1 by FINSEQ_1:44;
hence thesis by Th31;
end;
theorem Th33:
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]|
proof
-p2 = |[ -p2`1, -p2`2]| by Th31;
then (-p2)`1 = -p2`1 & (-p2)`2 = -p2`2 by FINSEQ_1:44;
hence p1 - p2 = |[ p1`1 + -p2`1, p1`2 + -p2`2]| by Th27
.= |[ p1`1 - p2`1, p1`2 - p2`2]|;
end;
theorem
|[x1, y1]| - |[x2, y2]| = |[ x1 - x2, y1 - y2]|
proof
A1: |[x2, y2]|`1 = x2 & |[x2, y2]|`2 = y2 by FINSEQ_1:44;
|[x1, y1]|`1 = x1 & |[x1, y1]|`2 = y1 by FINSEQ_1:44;
hence thesis by A1,Th33;
end;
theorem
for P being Subset of TOP-REAL n, Q being non empty Subset of Euclid n
holds P = Q implies (TOP-REAL n) |P = TopSpaceMetr((Euclid n) |Q)
proof
let P be Subset of (TOP-REAL n), Q be non empty Subset of Euclid n;
set M = TopSpaceMetr((Euclid n) |Q);
the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by Def8;
then M is SubSpace of the TopStruct of TOP-REAL n by TOPMETR:13;
then reconsider M = TopSpaceMetr((Euclid n) |Q) as SubSpace of TOP-REAL n by
PRE_TOPC:29;
assume P = Q;
then [#](M) = P by TOPMETR:def 2;
hence thesis by PRE_TOPC:def 5;
end;
:: to enable the 03.2009. revision A.T.
theorem
for p1,p2 being Point of TOP-REAL n for r1,r2 being real-valued
Function st p1 = r1 & p2 =r2 holds p1+p2 = r1+r2;
theorem
for p being Point of TOP-REAL n for r being real-valued Function st
p = r holds x*p = x(#)r;
theorem Th38:
0.REAL n = 0.TOP-REAL n
proof
the RLSStruct of TOP-REAL n = RealVectSpace Seg n by Def8;
hence thesis;
end;
theorem Th39:
the carrier of Euclid n = the carrier of TOP-REAL n
proof
thus the carrier of Euclid n = the carrier of TopSpaceMetr Euclid n
.= the carrier of the TopStruct of TOP-REAL n by Def8
.= the carrier of TOP-REAL n;
end;
theorem
for p1 being Point of TOP-REAL n for r1 being real-valued Function st
p1 = r1 holds -p1 = -r1;
theorem
for p1,p2 being Point of TOP-REAL n for r1,r2 being real-valued
Function st p1 = r1 & p2 =r2 holds p1-p2 = r1-r2;
theorem
0.TOP-REAL n = 0*n by Th38;
theorem
for p being Point of TOP-REAL n holds |.-p.| = |.p.| by Th7;
registration
let n; let D be set;
cluster n-tuples_on D -> FinSequence-membered;
coherence;
end;
registration
let n;
cluster REAL n -> FinSequence-membered;
coherence;
end;
registration
let n;
cluster REAL n -> real-functions-membered;
coherence
proof
let x be object;
assume x in REAL n;
then reconsider x as Element of REAL n;
x is real-valued;
hence thesis;
end;
end;
:: from JORDAN2C, 2011.07.28, A.T.
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
definition
let n be Nat;
func 1*n -> FinSequence of REAL equals
n |-> 1;
coherence
proof
n |-> jj is FinSequence of REAL;
hence thesis;
end;
end;
definition
let n be Nat;
redefine func 1*n -> Element of REAL n; :: redefines 1* (EUCLID, definition)
coherence
proof
n |-> jj is Element of REAL n;
hence thesis;
end;
end;
definition
let n be Nat;
func 1.REAL n -> Point of TOP-REAL n equals
1*n;
coherence by Th19;
end;
theorem
abs 1*n = n |-> 1
proof
thus abs 1*n = abs(n |-> jj)
.= n |-> absreal.1 by FINSEQOP:16
.= n |-> |.1.| by Def2
.= n |-> 1 by ABSVALUE:def 1;
end;
theorem Th45:
|.1*n.| = sqrt n
proof
reconsider j=1^2 as Element of REAL by XREAL_0:def 1;
reconsider f= n |-> j as FinSequence of REAL;
thus |.1*n .| = sqrt Sum f by RVSUM_1:56
.= sqrt (n*1) by RVSUM_1:80
.= sqrt n;
end;
theorem
|. (1.REAL n) .| = sqrt n by Th45;
theorem
1<=n implies 1<=|. (1.REAL n) .|
proof
assume
A1: 1<=n;
|.1.REAL n.|=sqrt n by Th45;
hence thesis by A1,SQUARE_1:18,26;
end;
theorem
for f being FinSequence of REAL holds
f is Element of REAL len f & f is Point of TOP-REAL len f
proof
let f be FinSequence of REAL;
f is Element of REAL* by FINSEQ_1:def 11;
then
the carrier of TOP-REAL len f = the carrier of Euclid len f & f in ((len
f) -tuples_on REAL) by Th39;
hence thesis;
end;
theorem
REAL 0 = {0.TOP-REAL 0}
proof
thus REAL 0 = { <*>REAL } by FINSEQ_2:94
.= {0.TOP-REAL 0};
end;