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

registration

let s be Real;
let r be non positive Real;

cluster K499((s - r),(s + r)) -> empty ;

coherence
].(s - r),(s + r).[ is empty by XREAL_1:6, XXREAL_1:28;

cluster K497((s - r),(s + r)) -> empty ;

coherence
[.(s - r),(s + r).[ is empty by XREAL_1:6, XXREAL_1:27;

cluster K498((s - r),(s + r)) -> empty ;

coherence
].(s - r),(s + r).] is empty by XREAL_1:6, XXREAL_1:26;

end;

registration

let s be Real;
let r be negative Real;

cluster K496((s - r),(s + r)) -> empty ;

coherence
[.(s - r),(s + r).] is empty by XREAL_1:6, XXREAL_1:29;

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;

cluster {f} -> real-functions-membered ;

coherence
{f} is real-functions-membered by TARSKI:def 1;
let g be real-valued Function;

cluster {f,g} -> real-functions-membered ;

coherence
{f,g} is real-functions-membered 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 b₁ -element FinSequence st f is empty holds
n = 0 ;

theorem :: EUCLID_9:2

for n being Nat
for f being b₁ -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 b₁ being Nat
for f1, f2 being n -element real-valued FinSequence st b₁ = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds
b₁ = 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 b₁ -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 b₁ -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 b₂ -element real-valued FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))

proof end;

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 ;

end;

registration

let n be Nat;

cluster -> REAL -valued for Element of the carrier of (Euclid n);

coherence
for b₁ being Point of (Euclid n) holds b₁ is REAL -valued

proof end;

end;

registration

let n be Nat;

cluster -> n -element for Element of the carrier of (Euclid n);

coherence
for b₁ being Point of (Euclid n) holds b₁ is n -element ;

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

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 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 (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
for a, o, p being Element of (TOP-REAL n) 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 (Euclid n) 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 b₁ being Function st
( dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = ].((f . x) - r),((f . x) + r).[ ) )

proof end;

uniqueness
for b₁, b₂ being Function st dom b₁ = dom f & ( for x being object st x in dom f holds
b₁ . x = ].((f . x) - r),((f . x) + r).[ ) & dom b₂ = dom f & ( for x being object st x in dom f holds
b₂ . x = ].((f . x) - r),((f . x) + r).[ ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Intervals EUCLID_9:def 3 :
for f being real-valued Function
for r being Real
for b₃ being Function holds
( b₃ = Intervals (f,r) iff ( dom b₃ = dom f & ( for x being object st x in dom f holds
b₃ . 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 (Euclid n);
let r be Real;

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 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 (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 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 (Euclid 0) holds OpenHypercube (e,r) = {{}} by CARD_3:10;

registration

let e be Point of (Euclid 0);
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 (Euclid n);
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 (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
for e, e1 being Point of (Euclid n) 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 (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
for e, e1 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
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
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
for e, e1 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
for e, e1 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
for e, e1 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
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;

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

proof end;

deffunc H₁( 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 :: 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;
A2: product {} = {{}} by CARD_3:10;
A3: REAL 0 = {(0. (TOP-REAL 0))} by EUCLID:77;
A4: { the carrier of (TopSpaceMetr (Euclid 0))} is Basis of (TopSpaceMetr (Euclid 0)) by YELLOW_9:10;
the carrier of (TopSpaceMetr (Euclid 0)) = the carrier of (product ({} --> R^1)) by A1, A2, A3;
then product ({} --> R^1) is 1 -element ;
then { the carrier of (product ({} --> R^1))} is Basis of (product ({} --> R^1)) by YELLOW_9:10;
hence TopSpaceMetr (Euclid 0) = product ({} --> R^1) by A1, A2, A3, A4, 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))

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;