:: The Correspondence Between $n$-dimensional {E}uclidean Space and the Product of $n$ Real Lines
:: by Artur Korni{\l}owicz
::
:: Received November 30, 2009
:: Copyright (c) 2009 Association of Mizar Users


begin

registration
let s be real number ;
let r be real non positive number ;
cluster K486((s - r),(s + r)) -> empty ;
coherence
].(s - r),(s + r).[ is empty
proof end;
cluster K484((s - r),(s + r)) -> empty ;
coherence
[.(s - r),(s + r).[ is empty
proof end;
cluster K485((s - r),(s + r)) -> empty ;
coherence
].(s - r),(s + r).] is empty
proof end;
end;

registration
let s be real number ;
let r be real negative number ;
cluster K483((s - r),(s + r)) -> empty ;
coherence
[.(s - r),(s + r).] is empty
proof end;
end;

registration
let f be empty-yielding Function;
let x be set ;
cluster f . x -> empty ;
coherence
f . x is empty
proof end;
end;

registration
let i be Nat;
cluster i |-> 0 -> empty-yielding ;
coherence
i |-> 0 is empty-yielding
proof end;
end;

registration
let n be Nat;
let f be complex-valued n -long FinSequence;
cluster - f -> n -long ;
coherence
- f is n -long
proof end;
cluster f " -> n -long ;
coherence
f " is n -long
proof end;
cluster f ^2 -> n -long ;
coherence
f ^2 is n -long
proof end;
cluster |.f.| -> n -long ;
coherence
abs f is n -long
proof end;
let g be complex-valued n -long FinSequence;
cluster f + g -> n -long ;
coherence
f + g is n -long
proof end;
cluster f - g -> n -long ;
coherence
f - g is n -long ;
cluster f (#) g -> n -long ;
coherence
f (#) g is n -long
proof end;
cluster f /" g -> n -long ;
coherence
f /" g is n -long ;
end;

registration
let c be complex number ;
let n be Nat;
let f be complex-valued n -long FinSequence;
cluster c + f -> n -long ;
coherence
c + f is n -long
proof end;
cluster f - c -> n -long ;
coherence
f - c is n -long ;
cluster c (#) f -> n -long ;
coherence
c (#) f is n -long
proof end;
end;

registration
let f be real-valued Function;
cluster {f} -> real-functions-membered ;
coherence
{f} is real-functions-membered
proof end;
let g be real-valued Function;
cluster {f,g} -> real-functions-membered ;
coherence
{f,g} is real-functions-membered
proof end;
end;

registration
let n be Nat;
let D be set ;
cluster n -tuples_on D -> FinSequence-membered ;
coherence
n -tuples_on D is FinSequence-membered
proof end;
end;

registration
let n be Nat;
cluster REAL n -> FinSequence-membered ;
coherence
REAL n is FinSequence-membered ;
end;

registration
let n be Nat;
cluster REAL n -> real-functions-membered ;
coherence
REAL n is real-functions-membered
proof end;
end;

registration
let n be Nat;
let x, y be set ;
let f be n -long FinSequence;
cluster f +* x,y -> n -long ;
coherence
f +* x,y is n -long
proof end;
end;

theorem Th1: :: EUCLID_9:1
for n being Nat
for f being b1 -long FinSequence st f is empty holds
n = 0
proof end;

theorem Th2: :: EUCLID_9:2
for n being Nat
for f being real-valued b1 -long FinSequence holds f in REAL n
proof end;

theorem Th3: :: EUCLID_9:3
for f, g being complex-valued Function holds abs (f - g) = abs (g - f)
proof end;

definition
let n be Nat;
let f1, f2 be real-valued n -long FinSequence;
func max_diff_index f1,f2 -> Nat equals :: EUCLID_9:def 1
the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};
coherence
the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} is Nat ;
commutativity
for b1 being Nat
for f1, f2 being real-valued n -long FinSequence st b1 = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds
b1 = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))}
proof end;
end;

:: deftheorem defines max_diff_index EUCLID_9:def 1 :
for n being Nat
for f1, f2 being real-valued b1 -long FinSequence holds max_diff_index f1,f2 = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};

theorem :: EUCLID_9:4
for n being Nat
for f1, f2 being real-valued b1 -long FinSequence st n <> 0 holds
max_diff_index f1,f2 in dom f1
proof end;

theorem Th5: :: EUCLID_9:5
for x being set
for n being Nat
for f1, f2 being real-valued b2 -long FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index f1,f2)
proof end;

registration
cluster RealSpace -> real-membered ;
coherence
RealSpace is real-membered
proof end;
end;

registration
cluster TopSpaceMetr (Euclid 0 ) -> trivial ;
coherence
TopSpaceMetr (Euclid 0 ) is trivial by JORDAN2C:113;
end;

registration
let n be Nat;
cluster Euclid n -> constituted-FinSeqs ;
coherence
Euclid n is constituted-FinSeqs
proof end;
end;

registration
let n be Nat;
cluster -> REAL -valued Element of the carrier of (Euclid n);
coherence
for b1 being Point of (Euclid n) holds b1 is REAL -valued
proof end;
end;

registration
let n be Nat;
cluster -> n -long Element of the carrier of (Euclid n);
coherence
for b1 being Point of (Euclid n) holds b1 is n -long ;
end;

theorem Th6: :: EUCLID_9:6
Family_open_set (Euclid 0 ) = {{} ,{{} }}
proof end;

theorem :: EUCLID_9:7
for B being Subset of (Euclid 0 ) holds
( B = {} or B = {{} } ) by ZFMISC_1:39, JORDAN2C:113;

definition
let n be Nat;
let e be Point of (Euclid n);
func @ e -> Point of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 2
e;
coherence
e is Point of (TopSpaceMetr (Euclid n)) ;
end;

:: deftheorem defines @ EUCLID_9:def 2 :
for n being Nat
for e being Point of (Euclid n) holds @ e = e;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be real non positive number ;
cluster Ball e,r -> empty ;
coherence
Ball e,r is empty
proof end;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be real positive number ;
cluster Ball e,r -> non empty ;
coherence
not Ball e,r is empty by GOBOARD6:4;
end;

theorem Th8: :: EUCLID_9:8
for n, i being Nat
for p1, p2 being Point of (TOP-REAL n) st i in dom p1 holds
((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2))
proof end;

theorem Th9: :: EUCLID_9:9
for n being Nat
for r being real number
for a, o, p being Element of (TOP-REAL n) st a in Ball o,r holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
proof end;

theorem Th10: :: EUCLID_9:10
for n being Nat
for r being real number
for a, o being Point of (Euclid n) st a in Ball o,r holds
for x being set holds
( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r )
proof end;

definition
let f be real-valued Function;
let r be real number ;
func Intervals f,r -> Function means :Def3: :: EUCLID_9:def 3
( dom it = dom f & ( for x being set st x in dom f holds
it . x = ].((f . x) - r),((f . x) + r).[ ) );
existence
ex b1 being Function st
( dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) & dom b2 = dom f & ( for x being set st x in dom f holds
b2 . x = ].((f . x) - r),((f . x) + r).[ ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines Intervals EUCLID_9:def 3 :
for f being real-valued Function
for r being real number
for b3 being Function holds
( b3 = Intervals f,r iff ( dom b3 = dom f & ( for x being set st x in dom f holds
b3 . x = ].((f . x) - r),((f . x) + r).[ ) ) );

registration
let r be real number ;
cluster Intervals {} ,r -> empty ;
coherence
Intervals {} ,r is empty
proof end;
end;

registration
let f be real-valued FinSequence;
let r be real number ;
cluster Intervals f,r -> FinSequence-like ;
coherence
Intervals f,r is FinSequence-like
proof end;
end;

definition
let n be Nat;
let e be Point of (Euclid n);
let r be real number ;
func OpenHypercube e,r -> Subset of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 4
 product (Intervals e,r);
coherence
product (Intervals e,r) is Subset of (TopSpaceMetr (Euclid n))
proof end;
end;

:: deftheorem defines OpenHypercube EUCLID_9:def 4 :
for n being Nat
for e being Point of (Euclid n)
for r being real number holds OpenHypercube e,r = product (Intervals e,r);

theorem Th11: :: EUCLID_9:11
for n being Nat
for r being real number
for e being Point of (Euclid n) st 0 < r holds
e in OpenHypercube e,r
proof end;

registration
let n be non zero Nat;
let e be Point of (Euclid n);
let r be real non positive number ;
cluster OpenHypercube e,r -> empty ;
coherence
OpenHypercube e,r is empty
proof end;
end;

theorem Th12: :: EUCLID_9:12
for r being real number
for e being Point of (Euclid 0 ) holds OpenHypercube e,r = {{} } by CARD_3:19;

registration
let e be Point of (Euclid 0 );
let r be real number ;
cluster OpenHypercube e,r -> non empty ;
coherence
not OpenHypercube e,r is empty by CARD_3:19;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be real positive number ;
cluster OpenHypercube e,r -> non empty ;
coherence
not OpenHypercube e,r is empty by Th11;
end;

theorem Th13: :: EUCLID_9:13
for n being Nat
for r, s being real number
for e being Point of (Euclid n) st r <= s holds
OpenHypercube e,r c= OpenHypercube e,s
proof end;

theorem Th14: :: EUCLID_9:14
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube e,r holds
for x being set holds
( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r )
proof end;

theorem Th15: :: EUCLID_9:15
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
Sum (sqr (e1 - e)) < n * (r ^2 )
proof end;

theorem Th16: :: EUCLID_9:16
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
dist e1,e < r * (sqrt n)
proof end;

theorem Th17: :: EUCLID_9:17
for n being Nat
for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube e,(r / (sqrt n)) c= Ball e,r
proof end;

theorem :: EUCLID_9:18
for n being Nat
for r being real number
for e being Point of (Euclid n) st n <> 0 holds
OpenHypercube e,r c= Ball e,(r * (sqrt n))
proof end;

theorem Th19: :: EUCLID_9:19
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st e1 in Ball e,r holds
ex m being non zero Element of NAT st OpenHypercube e1,(1 / m) c= Ball e,r
proof end;

theorem Th20: :: EUCLID_9:20
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube e,r holds
r > (abs (e1 - e)) . (max_diff_index e1,e)
proof end;

theorem Th21: :: EUCLID_9:21
for n being Nat
for r being real number
for e1, e being Point of (Euclid n) holds OpenHypercube e1,(r - ((abs (e1 - e)) . (max_diff_index e1,e))) c= OpenHypercube e,r
proof end;

theorem Th22: :: EUCLID_9:22
for n being Nat
for r being real number
for e being Point of (Euclid n) holds Ball e,r c= OpenHypercube e,r
proof end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be real number ;
cluster OpenHypercube e,r -> open ;
coherence
OpenHypercube e,r is open
proof end;
end;

theorem :: EUCLID_9:23
for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st V is open holds
for e being Point of (Euclid n) st e in V holds
ex m being non zero Element of NAT st OpenHypercube e,(1 / m) c= V
proof end;

theorem :: EUCLID_9:24
for n being Nat
for V being Subset of (TopSpaceMetr (Euclid n)) st ( for e being Point of (Euclid n) st e in V holds
ex r being real number st
( r > 0 & OpenHypercube e,r c= V ) ) holds
V is open
proof end;

deffunc H1( Nat, Point of (Euclid $1)) -> set = { (OpenHypercube $2,(1 / m)) where m is non zero Element of NAT : verum } ;

definition
let n be Nat;
let e be Point of (Euclid n);
func OpenHypercubes e -> Subset-Family of (TopSpaceMetr (Euclid n)) equals :: EUCLID_9:def 5
{ (OpenHypercube e,(1 / m)) where m is non zero Element of NAT : verum } ;
coherence
{ (OpenHypercube e,(1 / m)) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n))
proof end;
end;

:: deftheorem defines OpenHypercubes EUCLID_9:def 5 :
for n being Nat
for e being Point of (Euclid n) holds OpenHypercubes e = { (OpenHypercube e,(1 / m)) where m is non zero Element of NAT : verum } ;

registration
let n be Nat;
let e be Point of (Euclid n);
cluster OpenHypercubes e -> non empty open @ e -quasi_basis ;
coherence
( not OpenHypercubes e is empty & OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )
proof end;
end;

Lm1: now
set J = {} --> R^1 ;
set C = Carrier ({} --> R^1 );
set P = product ({} --> R^1 );
set T = TopSpaceMetr (Euclid 0 );
A1: the carrier of (product ({} --> R^1 )) = product (Carrier ({} --> R^1 )) by WAYBEL18:def 3;
dom (Carrier ({} --> R^1 )) = {} by PARTFUN1:def 4;
then A2: Carrier ({} --> R^1 ) = {} ;
{the carrier of (TopSpaceMetr (Euclid 0 ))} is Basis of (TopSpaceMetr (Euclid 0 )) by YELLOW_9:10;
hence TopSpaceMetr (Euclid 0 ) = product ({} --> R^1 ) by A2, A1, YELLOW_9:10, YELLOW_9:25, CARD_3:19, JORDAN2C:113; :: thesis: verum
end;

theorem Th25: :: EUCLID_9:25
for n being Nat holds Funcs (Seg n),REAL = product (Carrier ((Seg n) --> R^1 ))
proof end;

theorem Th26: :: EUCLID_9:26
for n being Nat st n <> 0 holds
for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1 ) holds
PP is quasi_prebasis
proof end;

theorem Th27: :: EUCLID_9:27
for n being Nat
for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1 ) holds
PP is open
proof end;

theorem :: EUCLID_9:28
for n being Nat holds TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1 )
proof end;