:: 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-2012 Association of Mizar Users


begin

registration
let s be real number ;
let r be non positive real number ;
clusterK510((s - r),(s + r)) ->  empty ;
coherence
 ].(s - r),(s + r).[ is empty
proofend;
clusterK508((s - r),(s + r)) ->  empty ;
coherence
 [.(s - r),(s + r).[ is empty
proofend;
clusterK509((s - r),(s + r)) ->  empty ;
coherence
 ].(s - r),(s + r).] is empty
proofend;
end;

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

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

registration
let c be complex number ;
let n be Nat;
let f be complex-valued n -element FinSequence;
clusterc + f -> n -element ;
coherence
 c + f is n -element
proofend;
clusterf - c -> n -element ;
coherence
 f - c is n -element ;
clusterc (#) f -> n -element ;
coherence
 c (#) f is n -element
proofend;
end;

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

registration
let n be Nat;
let x, y be set ;
let f be n -element FinSequence;
clusterf +* (x,y) -> n -element ;
coherence
 f +* (x,y) is n -element
proofend;
end;

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

theorem Th2: :: EUCLID_9:2
for n being Nat
for f being real-valued b1 -element FinSequence holds f in REAL n
proofend;

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

definition
let n be Nat;
let f1, f2 be real-valued n -element 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 -element 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))))}
proofend;
end;

:: deftheorem  defines max_diff_index EUCLID_9:def_1_:_
 for n being Nat
for f1, f2 being real-valued b1 -element 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 -element FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1
proofend;

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

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

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

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

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

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

theorem :: EUCLID_9:7
for B being Subset of (Euclid 0) holds
( B = {} or B = {{}} ) by EUCLID:77, ZFMISC_1:33;

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 non positive real number ;
cluster Ball (e,r) ->  empty ;
coherence
 Ball (e,r) is empty
proofend;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be positive real number ;
cluster Ball (e,r) ->  non empty ;
coherence
 not Ball (e,r) is empty by GOBOARD6:1;
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))
proofend;

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 &amp; abs ((a . x) - (o . x)) < r )
proofend;

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 &amp; abs ((a . x) - (o . x)) < r )
proofend;

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 &amp; ( 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 &amp; ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = dom f &amp; ( for x being set st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) &amp; dom b2 = dom f &amp; ( for x being set st x in dom f holds
b2 . x = ].((f . x) - r),((f . x) + r).[ ) holds
b1 = b2
proofend;
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 &amp; ( 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
proofend;
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
proofend;
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))
proofend;
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)
proofend;

registration
let n be non zero Nat;
let e be Point of (Euclid n);
let r be non positive real number ;
cluster OpenHypercube (e,r) ->  empty ;
coherence
 OpenHypercube (e,r) is empty
proofend;
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:10;

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:10;
end;

registration
let n be Nat;
let e be Point of (Euclid n);
let r be positive real 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)
proofend;

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 ) &amp; e1 in OpenHypercube (e,r) holds
for x being set holds
( abs ((e1 - e) . x) < r &amp; abs ((e1 . x) - (e . x)) < r )
proofend;

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 &amp; e1 in OpenHypercube (e,r) holds
Sum (sqr (e1 - e)) < n * (r ^2)
proofend;

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 &amp; e1 in OpenHypercube (e,r) holds
dist (e1,e) < r * (sqrt n)
proofend;

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)
proofend;

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)))
proofend;

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)
proofend;

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 &amp; e1 in OpenHypercube (e,r) holds
r > (abs (e1 - e)) . (max_diff_index (e1,e))
proofend;

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)
proofend;

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)
proofend;

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
proofend;
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
proofend;

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 &amp; OpenHypercube (e,r) c= V ) ) holds
V is open
proofend;

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))
proofend;
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 &amp; OpenHypercubes e is open &amp; OpenHypercubes e is @ e -quasi_basis )
proofend;
end;

Lm1: now__::_thesis:_TopSpaceMetr_(Euclid_0)_=_product_({}_-->_R^1)
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;
 { the carrier of (TopSpaceMetr (Euclid 0))} is Basis of (TopSpaceMetr (Euclid 0)) by YELLOW_9:10;
hence  TopSpaceMetr (Euclid 0) = product ({} --> R^1) by A1, CARD_3:10, EUCLID:77, YELLOW_9:10, YELLOW_9:25; ::_thesis: verum
end;

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

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
proofend;

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
proofend;

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