:: The Euclidean Space :: by Agata Darmochwa{\l} :: :: Received November 21, 1991 :: Copyright (c) 1991-2021 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};