:: Completeness of the Real {E}uclidean Space
:: by Noboru Endou and Yasunari Shidama
::
:: Received December 28, 2005
:: Copyright (c) 2005-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, SUBSET_1, NAT_1, BINOP_1, FUNCT_1, ARYTM_3, FINSEQ_2,
ZFMISC_1, RELAT_1, COMPLEX1, STRUCT_0, XBOOLE_0, NORMSP_1, SUPINF_2,
EUCLID, ALGSTR_0, RLVECT_1, PRE_TOPC, REAL_1, CARD_1, XXREAL_0, ARYTM_1,
FINSEQ_1, CARD_3, ORDINAL4, TARSKI, RVSUM_1, SQUARE_1, SEQ_2, ORDINAL2,
SEQ_1, VALUED_1, RSSPACE3, LOPBAN_1, REWRITE1, BHSP_1, PROB_2, BINOP_2,
METRIC_1, BHSP_3, REAL_NS1, RELAT_2, NORMSP_0, FUNCT_7, XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, BINOP_1,
PRE_TOPC, ORDINAL1, XCMPLX_0, NAT_1, FINSEQ_1, FINSEQ_2, FUNCT_2,
STRUCT_0, ALGSTR_0, FUNCOP_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1,
COMPLEX1, REAL_1, RLVECT_1, BHSP_1, BHSP_2, BINOP_2, VALUED_1, SEQ_1,
SEQ_2, RVSUM_1, NORMSP_0, NORMSP_1, EUCLID, RSSPACE3, LOPBAN_1, BHSP_3;
constructors REAL_1, SQUARE_1, BINOP_2, COMPLEX1, SEQ_2, FINSEQOP, REALSET2,
BHSP_2, BHSP_3, RSSPACE3, LOPBAN_1, RVSUM_1, EUCLID, RELSET_1, COMSEQ_2,
BINOP_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, NUMBERS,
XXREAL_0, XREAL_0, MEMBERED, FINSEQ_2, STRUCT_0, NORMSP_0, NORMSP_1,
BHSP_1, REVROT_1, RSSPACE3, VALUED_0, VALUED_1, FUNCT_2, EUCLID,
FINSEQ_1, CARD_1, SQUARE_1, RVSUM_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
begin :: R^n space as RealLinearSpace
reserve n for Nat;
definition
let n be Nat;
func Euclid_add n -> BinOp of REAL n means
:: REAL_NS1:def 1
for a,b being Element of REAL n holds it.(a,b) = a+b;
end;
registration
let n be Nat;
cluster Euclid_add n -> commutative associative;
end;
definition
let n be Nat;
func Euclid_mult n -> Function of [: REAL, REAL n :], REAL n means
:: REAL_NS1:def 2
for r be Real, x be Element of REAL n holds it.(r,x) = r*x;
end;
definition
let n be Nat;
func Euclid_norm n -> Function of REAL n,REAL means
:: REAL_NS1:def 3
for x being Element of REAL n holds it.x = |.x.|;
end;
definition
let n be Nat;
func REAL-NS n -> strict non empty NORMSTR means
:: REAL_NS1:def 4
the carrier of it =
REAL n & 0.it = 0*n & the addF of it = Euclid_add n & the Mult of it =
Euclid_mult n & the normF of it = Euclid_norm n;
end;
registration
let n be non zero Nat;
cluster REAL-NS n -> non trivial;
end;
theorem :: REAL_NS1:1
for x be VECTOR of REAL-NS n, y be Element of REAL n st x=y holds
||.x.|| = |.y.|;
theorem :: REAL_NS1:2
for n be Nat for x,y be VECTOR of REAL-NS n, a,b be
Element of REAL n st x=a & y=b holds x+y = a + b;
theorem :: REAL_NS1:3
for x be VECTOR of REAL-NS n, y be Element of REAL n, a be Real
st x=y holds a * x = a * y;
registration
let n be Nat;
cluster REAL-NS n -> reflexive discerning RealNormSpace-like
vector-distributive scalar-distributive scalar-associative scalar-unital
Abelian add-associative right_zeroed right_complementable;
end;
theorem :: REAL_NS1:4
for x be VECTOR of REAL-NS n, a be Element of REAL n st x=a holds -x = -a;
theorem :: REAL_NS1:5
for x,y be VECTOR of REAL-NS n, a,b be Element of REAL n st x=a &
y=b holds x-y = a - b;
theorem :: REAL_NS1:6
for f be FinSequence of REAL st dom f = Seg n holds f is Element of REAL n;
theorem :: REAL_NS1:7
for n be Nat, x be Element of REAL n st (for i be
Nat st i in Seg n holds 0 <= x.i) holds 0 <= Sum x & for i be
Nat st i in Seg n holds x.i <= Sum x;
theorem :: REAL_NS1:8
for x be Element of REAL n, i be Nat st i in Seg n holds |.x.i.| <= |.x.|;
theorem :: REAL_NS1:9
for x be Point of REAL-NS n, y be Element of REAL n st x=y holds
for i be Nat st i in Seg n holds |.y.i.| <= ||.x.||;
theorem :: REAL_NS1:10
for x be Element of REAL (n+1) holds |.x.|^2 = |.(x|n).|^2 + (x. (n+1))^2;
definition
let n be Nat;
let f be sequence of REAL n, k be Nat;
redefine func f.k -> Element of REAL n;
end;
theorem :: REAL_NS1:11
for n be Nat for x be Point of REAL-NS n, xs be
Element of REAL n, seq be sequence of REAL-NS n, xseq be sequence of REAL
n st xs = x & xseq = seq holds ( seq is convergent & lim seq = x iff
for i be Nat st i in Seg n ex rseqi be Real_Sequence st
for k be Nat
holds rseqi.k = (xseq.k).i & rseqi is convergent & xs.i = lim rseqi );
theorem :: REAL_NS1:12
for f be sequence of REAL-NS n st f is Cauchy_sequence_by_Norm
holds f is convergent;
registration
let n;
cluster REAL-NS n -> complete;
end;
begin :: R^n space as RealNormSpace
definition
let n be Nat;
func Euclid_scalar n -> Function of [:REAL n,REAL n:],REAL means
:: REAL_NS1:def 5
for x,y being Element of REAL n holds it.(x,y) = Sum mlt(x,y);
end;
definition
let n be Nat;
func REAL-US n -> strict non empty UNITSTR means
:: REAL_NS1:def 6
the carrier of it =
REAL n & 0.it = 0*n & the addF of it = Euclid_add n & the Mult of it =
Euclid_mult n & the scalar of it = Euclid_scalar n;
end;
registration
let n be non zero Nat;
cluster REAL-US n -> non trivial;
end;
registration
let n be Nat;
cluster REAL-US n -> RealUnitarySpace-like vector-distributive
scalar-distributive scalar-associative scalar-unital Abelian
add-associative right_zeroed right_complementable;
end;
theorem :: REAL_NS1:13
for n be Nat, a be Real, x1,y1 be Point of REAL-NS n,
x2,y2 be Point of REAL-US n st x1 = x2 & y1 = y2 holds x1 + y1 = x2 + y2 & -x1
= -x2 & a * x1 = a * x2;
theorem :: REAL_NS1:14
for n be Nat, x1 be Point of REAL-NS n, x2 be Point of
REAL-US n st x1 = x2 holds ||.x1.||^2 = x2 .|. x2;
theorem :: REAL_NS1:15
for n be Nat, f be set holds f is sequence of REAL-NS
n iff f is sequence of REAL-US n;
theorem :: REAL_NS1:16
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 holds (seq1 is convergent implies seq2 is
convergent & lim seq1 = lim seq2) & (seq2 is convergent implies seq1 is
convergent & lim seq1 = lim seq2);
theorem :: REAL_NS1:17
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm holds
seq2 is Cauchy;
theorem :: REAL_NS1:18
for n be Nat, seq1 be sequence of REAL-NS n, seq2 be
sequence of REAL-US n st seq1 = seq2 & seq2 is Cauchy holds seq1 is
Cauchy_sequence_by_Norm;
registration
let n;
cluster REAL-US n -> complete;
end;