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

environ

vocabularies HIDDEN, RELAT_1, FUNCT_1, VALUED_0, ARYTM_1, COMPLEX1, ARYTM_3, XCMPLX_0, FINSEQ_1, EUCLID, PRE_TOPC, ORDINAL2, METRIC_1, TOPMETR, RCOMP_1, PCOMPS_1, FINSEQ_2, RVSUM_1, SQUARE_1, FUNCT_4, VALUED_2, SUBSET_1, FUNCOP_1, PARTFUN1, CARD_3, MONOID_0, CANTOR_1, QC_LANG1, SETFAM_1, RLVECT_2, WAYBEL18, RLVECT_3, PBOOLE, TOPGEN_2, STRUCT_0, FINSET_1, FUNCT_2, TARSKI, CARD_1, YELLOW_8, NAT_1, ZFMISC_1, XBOOLE_0, VALUED_1, NUMBERS, XXREAL_0, XXREAL_1, EUCLID_9, REAL_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, FINSET_1, TOPS_2, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, VALUED_0, VALUED_1, XCMPLX_0, XREAL_0, XXREAL_0, XXREAL_2, REAL_1, CARD_3, COMPLEX1, SQUARE_1, CANTOR_1, FUNCOP_1, FINSEQ_1, FINSEQ_2, RCOMP_1, FUNCT_7, VALUED_2, STRUCT_0, RVSUM_1, MONOID_0, PRE_TOPC, METRIC_1, PCOMPS_1, TOPMETR, ALGSTR_0, EUCLID, PRALG_1, YELLOW_8, WAYBEL18, TOPGEN_2, TOPREAL9, TOPREALB;
definitions RELAT_1, FINSEQ_1, MONOID_0, TOPS_2, CANTOR_1, YELLOW_8, TARSKI, XBOOLE_0, LATTICE7, VALUED_2, CARD_1;
theorems FUNCT_1, PARTFUN1, FUNCT_2, VALUED_1, FUNCT_7, VALUED_2, TOPMETR, TOPREAL9, EUCLID, GOBOARD6, METRIC_1, XBOOLE_1, XXREAL_0, XREAL_1, XBOOLE_0, RCOMP_1, FINSEQ_2, XREAL_0, FRECHET, FINSEQ_1, FUNCOP_1, PRE_TOPC, SQUARE_1, RVSUM_1, COMPLEX1, XXREAL_1, RELAT_1, XCMPLX_1, ORDINAL1, MATRPROB, TARSKI, ZFMISC_1, WAYBEL18, FINSEQ_3, CANTOR_1, XXREAL_2, YELLOW_9, CARD_3, FCONT_3, PRALG_1, PCOMPS_1, SETFAM_1, TOPGEN_2, RINFSUP1, CARD_1;
schemes FUNCT_1, PBOOLE, PRE_CIRC;
registrations XBOOLE_0, RELAT_1, FUNCT_1, VALUED_0, VALUED_1, MEMBERED, XCMPLX_0, XREAL_0, VALUED_2, STRUCT_0, EUCLID, MONOID_0, TOPREALB, XXREAL_0, NAT_1, TOPMETR, RVSUM_1, TOPREAL9, SQUARE_1, PCOMPS_1, RCOMP_1, FUNCT_7, FINSEQ_1, FUNCOP_1, WAYBEL18, JORDAN2B, SERIES_3, FINSEQ_2, XXREAL_2, FINSET_1, PARTFUN3, CARD_1, ORDINAL1;
constructors HIDDEN, MONOID_0, FUNCT_7, VALUED_2, TOPREAL9, TOPREALB, COMPLEX1, SQUARE_1, FUNCSDOM, WAYBEL18, BINOP_2, TOPGEN_2, PCOMPS_1, SEQ_4, REAL_1, FCONT_1, WAYBEL_8, PARTFUN3, LATTICE3, BORSUK_2;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities CARD_3, XCMPLX_0, SQUARE_1, VALUED_1, FINSEQ_2, METRIC_1, PCOMPS_1, TOPMETR, EUCLID, TOPREALB;
expansions MONOID_0, TARSKI, XBOOLE_0, VALUED_2;


registration
let s be Real;
let r be non positive Real;
cluster K496((s - r),(s + r)) -> empty ;
coherence
].(s - r),(s + r).[ is empty by XREAL_1:6, XXREAL_1:28;
cluster K494((s - r),(s + r)) -> empty ;
coherence
[.(s - r),(s + r).[ is empty by XREAL_1:6, XXREAL_1:27;
cluster K495((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 K493((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 b1 -element FinSequence st f is empty holds
n = 0 ;

theorem Th2: :: 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
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 b1 being Point of (Euclid n) holds b1 is REAL -valued
proof end;
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) = {{},{{}}}
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 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 (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 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 :: 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))
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;