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

registration
let s be Real;
let r be non positive Real;
cluster K498((s - r),(s + r)) -> empty ;
coherence
].(s - r),(s + r).[ is empty
by ;
cluster K496((s - r),(s + r)) -> empty ;
coherence
[.(s - r),(s + r).[ is empty
by ;
cluster K497((s - r),(s + r)) -> empty ;
coherence
].(s - r),(s + r).] is empty
by ;
end;

registration
let s be Real;
let r be negative Real;
cluster K495((s - r),(s + r)) -> empty ;
coherence
[.(s - r),(s + r).] is empty
by ;
end;

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

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

registration
let f be real-valued Function;
coherence by TARSKI:def 1;
let g be real-valued Function;
coherence by TARSKI:def 2;
end;

registration
let n be Nat;
let x, y be object ;
let f be n -element FinSequence;
cluster f +* (x,y) -> n -element ;
coherence
f +* (x,y) is n -element
proof end;
end;

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

theorem :: EUCLID_9:2
for n being Nat
for f being b1 -element real-valued 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 n -element real-valued 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 n -element real-valued 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 b1 -element real-valued 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 b1 -element real-valued FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1
proof end;

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

registration
coherence by EUCLID:77;
end;

registration
let n be Nat;
coherence ;
end;

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

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

theorem Th6: :: EUCLID_9:6
proof end;

theorem :: EUCLID_9:7
for B being Subset of () holds
( B = {} or B = ) by ;

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

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

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

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

theorem Th8: :: EUCLID_9:8
for i, n being Nat
for p1, p2 being Point of () 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
for a, o, p being Element of () st a in Ball (o,r) holds
for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )
proof end;

theorem Th10: :: EUCLID_9:10
for n being Nat
for r being Real
for a, o being Point of () st a in Ball (o,r) holds
for x being object holds
( |.((a - o) . x).| < r & |.((a . x) - (o . x)).| < r )
proof end;

definition
let f be real-valued Function;
let r be Real;
func Intervals (f,r) -> Function means :Def3: :: EUCLID_9:def 3
( dom it = dom f & ( for x being object 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 object 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 object st x in dom f holds
b1 . x = ].((f . x) - r),((f . x) + r).[ ) & dom b2 = dom f & ( for x being object 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
for b3 being Function holds
( b3 = Intervals (f,r) iff ( dom b3 = dom f & ( for x being object st x in dom f holds
b3 . x = ].((f . x) - r),((f . x) + r).[ ) ) );

registration
let r be Real;
cluster Intervals ({},r) -> empty ;
coherence
Intervals ({},r) is empty
proof end;
end;

registration
let f be real-valued FinSequence;
let r be Real;
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 ();
let r be Real;
func OpenHypercube (e,r) -> Subset of () equals :: EUCLID_9:def 4
product (Intervals (e,r));
coherence
product (Intervals (e,r)) is Subset of ()
proof end;
end;

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

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

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

theorem Th12: :: EUCLID_9:12
for r being Real
for e being Point of () holds OpenHypercube (e,r) = by CARD_3:10;

registration
let e be Point of ();
let r be Real;
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 ();
let r be positive Real;
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
for e being Point of () 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
for e, e1 being Point of () st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds
for x being set holds
( |.((e1 - e) . x).| < r & |.((e1 . x) - (e . x)).| < r )
proof end;

theorem Th15: :: EUCLID_9:15
for n being Nat
for r being Real
for e, e1 being Point of () 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
for e, e1 being Point of () 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
for e being Point of () 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
for e being Point of () 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
for e, e1 being Point of () 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
for e, e1 being Point of () 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
for e, e1 being Point of () 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
for e being Point of () holds Ball (e,r) c= OpenHypercube (e,r)
proof end;

registration
let n be Nat;
let e be Point of ();
let r be Real;
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 () st V is open holds
for e being Point of () 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 () st ( for e being Point of () st e in V holds
ex r being Real 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 ();
func OpenHypercubes e -> Subset-Family of () 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 ()
proof end;
end;

:: deftheorem defines OpenHypercubes EUCLID_9:def 5 :
for n being Nat
for e being Point of () 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 ();
coherence
( not OpenHypercubes e is empty & OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )
proof end;
end;

Lm1: now :: thesis:
set J = {} --> R^1;
set C = Carrier ();
set P = product ();
set T = TopSpaceMetr ();
A1: the carrier of (product ()) = product (Carrier ()) by WAYBEL18:def 3;
{ the carrier of ()} is Basis of () by YELLOW_9:10;
hence TopSpaceMetr () = product () by ; :: 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 () 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 () st PP = product_prebasis ((Seg n) --> R^1) holds
PP is open
proof end;

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