:: The Euclidean Space
:: by Agata Darmochwa{\l}
::
:: Received November 21, 1991
:: Copyright (c) 1991-2017 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;
begin
reserve k,j,n for Nat,
r for Real;
definition
let n be Nat;
func REAL n -> FinSequenceSet of REAL equals
:: EUCLID:def 1
n-tuples_on REAL;
end;
registration
let n be Nat;
cluster REAL n -> non empty;
end;
registration
let n;
cluster -> n-element for Element of REAL n;
end;
definition
func absreal -> Function of REAL,REAL means
:: EUCLID:def 2
for r holds it.r = |.r.|;
end;
definition
let x be real-valued FinSequence;
redefine func abs x -> FinSequence of REAL equals
:: EUCLID:def 3
absreal*x;
end;
definition
let n;
func 0*n -> real-valued FinSequence equals
:: EUCLID:def 4
n |-> In(0,REAL);
end;
definition
let n;
redefine func 0*n -> Element of REAL n;
end;
reserve x,x1,x2,y for Element of REAL n;
definition
let n,x;
redefine func -x -> Element of REAL n;
end;
definition
let n,x,y;
redefine func x + y -> Element of REAL n;
redefine func x - y -> Element of REAL n;
end;
definition
let n, x;
let r be Real;
redefine func r*x -> Element of REAL n;
end;
definition
let n,x;
redefine func abs x -> Element of n-tuples_on REAL;
end;
definition
let n,x;
redefine func sqr x -> Element of n-tuples_on REAL;
end;
reserve f for real-valued FinSequence;
definition
let f;
func |. f .| -> Real equals
:: EUCLID:def 5
sqrt Sum sqr f;
end;
::$CT 3
theorem :: EUCLID:4
abs 0*n = n |-> (0 qua Real);
theorem :: EUCLID:5
for f being complex-valued Function holds abs -f = abs f;
theorem :: EUCLID:6
abs(r*f) = |.r.|*(abs f);
theorem :: EUCLID:7
|.0*n.| = 0;
theorem :: EUCLID:8
|. x .| = 0 implies x = 0*n;
theorem :: EUCLID:9
|.f.| >= 0;
registration
let f;
cluster |.f.| -> non negative;
end;
theorem :: EUCLID:10
|.-f.| = |.f.|;
theorem :: EUCLID:11
|.r*f.| = |.r.|*|.f.|;
theorem :: EUCLID:12
|.x1 + x2.| <= |.x1.| + |.x2.|;
theorem :: EUCLID:13
|.x1 - x2.| <= |.x1.| + |.x2.|;
theorem :: EUCLID:14
|.x1.| - |.x2.| <= |.x1 + x2.|;
theorem :: EUCLID:15
|.x1.| - |.x2.| <= |.x1 - x2.|;
theorem :: EUCLID:16
|.x1 - x2.| = 0 iff x1 = x2;
registration
let n,x1;
cluster |. x1 - x1 .| -> zero;
end;
theorem :: EUCLID:17
x1 <> x2 implies |.x1 - x2.| > 0;
theorem :: EUCLID:18
|.x1 - x2.| = |.x2 - x1.|;
theorem :: EUCLID:19
|.x1 - x2.| <= |.x1 - x .| + |.x - x2.|;
definition
let n be Nat;
func Pitag_dist n -> Function of [:REAL n,REAL n:],REAL means
:: EUCLID:def 6
for x,y being Element of REAL n holds it.(x,y) = |.x-y.|;
end;
theorem :: EUCLID:20
for x, y being real-valued FinSequence holds sqr(x-y) = sqr(y-x);
theorem :: EUCLID:21
for n being Nat holds Pitag_dist n is_metric_of REAL n;
definition
let n be Nat;
func Euclid n -> strict MetrSpace equals
:: EUCLID:def 7
MetrStruct(#REAL n,Pitag_dist n#);
end;
registration
let n be Nat;
cluster Euclid n -> non empty;
end;
definition
let n be Nat;
func TOP-REAL n -> strict RLTopStruct means
:: EUCLID:def 8
the TopStruct of it =
TopSpaceMetr Euclid n & the RLSStruct of it = RealVectSpace Seg n;
end;
registration
let n be Nat;
cluster TOP-REAL n -> non empty;
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;
end;
reserve p,p1,p2,p3 for Point of TOP-REAL n,
x,x1,x2,y,y1,y2 for Real;
theorem :: EUCLID:22
the carrier of TOP-REAL n = REAL n;
theorem :: EUCLID:23
p is Function of Seg n, REAL;
theorem :: EUCLID:24
p is FinSequence of REAL;
registration
let n;
cluster TOP-REAL n -> constituted-FinSeqs;
end;
registration
let n;
cluster -> FinSequence-like for Point of TOP-REAL n;
end;
registration
let n;
cluster -> real-valued for Point of TOP-REAL n;
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;
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;
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;
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;
end;
registration
let n;
cluster -> n-element for Point of TOP-REAL n;
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;
end;
theorem :: EUCLID:25
for x being Element of REAL n holds sqr abs x = sqr x;
::$CT 25
reserve p,p1,p2 for Point of TOP-REAL 2;
theorem :: EUCLID:51
ex x,y being Element of REAL st p=<*x,y*>;
definition
let p;
func p`1 -> Real equals
:: EUCLID:def 9
p.1;
func p`2 -> Real equals
:: EUCLID:def 10
p.2;
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;
end;
theorem :: EUCLID:52
|[x,y]|`1 = x & |[x,y]|`2 = y;
theorem :: EUCLID:53
p = |[p`1, p`2]|;
theorem :: EUCLID:54
0.TOP-REAL 2 = |[0,0]|;
theorem :: EUCLID:55
p1 + p2 = |[ p1`1 + p2`1, p1`2 + p2`2]|;
theorem :: EUCLID:56
|[x1, y1]| + |[x2, y2]| = |[ x1 + x2, y1 + y2]|;
theorem :: EUCLID:57
x*p = |[ x*p`1 ,x*p`2 ]|;
theorem :: EUCLID:58
x*|[x1,y1]| = |[ x*x1,x*y1 ]|;
theorem :: EUCLID:59
-p = |[ -p`1, -p`2]|;
theorem :: EUCLID:60
-|[x1,y1]| = |[ -x1, -y1]|;
theorem :: EUCLID:61
p1 - p2 = |[ p1`1 - p2`1, p1`2 - p2`2]|;
theorem :: EUCLID:62
|[x1, y1]| - |[x2, y2]| = |[ x1 - x2, y1 - y2]|;
theorem :: EUCLID:63
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);
:: to enable the 03.2009. revision A.T.
theorem :: EUCLID:64
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 :: EUCLID:65
for p being Point of TOP-REAL n for r being real-valued Function st
p = r holds x*p = x(#)r;
theorem :: EUCLID:66
0.REAL n = 0.TOP-REAL n;
theorem :: EUCLID:67
the carrier of Euclid n = the carrier of TOP-REAL n;
theorem :: EUCLID:68
for p1 being Point of TOP-REAL n for r1 being real-valued Function st
p1 = r1 holds -p1 = -r1;
theorem :: EUCLID:69
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 :: EUCLID:70
0.TOP-REAL n = 0*n;
theorem :: EUCLID:71
for p being Point of TOP-REAL n holds |.-p.| = |.p.|;
registration
let n; let D be set;
cluster n-tuples_on D -> FinSequence-membered;
end;
registration
let n;
cluster REAL n -> FinSequence-membered;
end;
registration
let n;
cluster REAL n -> real-functions-membered;
end;
definition
let n be Nat;
func 1*n -> FinSequence of REAL equals
:: EUCLID:def 11
n |-> 1;
end;
definition
let n be Nat;
redefine func 1*n -> Element of REAL n;
end;
definition
let n be Nat;
func 1.REAL n -> Point of TOP-REAL n equals
:: EUCLID:def 12
1*n;
end;
theorem :: EUCLID:72
abs 1*n = n |-> 1;
theorem :: EUCLID:73
|.1*n.| = sqrt n;
theorem :: EUCLID:74
|. (1.REAL n) .| = sqrt n;
theorem :: EUCLID:75
1<=n implies 1<=|. (1.REAL n) .|;
theorem :: EUCLID:76
for f being FinSequence of REAL holds
f is Element of REAL len f & f is Point of TOP-REAL len f;
theorem :: EUCLID:77
REAL 0 = {0.TOP-REAL 0};