:: by Artur Korni{\l}owicz

::

:: Received November 30, 2009

:: Copyright (c) 2009-2017 Association of Mizar Users

registration

let s be Real;

let r be non positive Real;

coherence

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

coherence

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

coherence

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

end;
let r be non positive Real;

coherence

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

coherence

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

coherence

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

registration

let s be Real;

let r be negative Real;

coherence

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

end;
let r be negative Real;

coherence

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

registration

let n be Nat;

let f be n -element complex-valued FinSequence;

coherence

- f is n -element

f " is n -element

f ^2 is n -element

abs f is n -element

coherence

f + g is n -element

f - g is n -element ;

coherence

f (#) g is n -element

f /" g is n -element ;

end;
let f be n -element complex-valued FinSequence;

coherence

- f is n -element

proof end;

coherence f " is n -element

proof end;

coherence f ^2 is n -element

proof end;

coherence abs f is n -element

proof end;

let g be n -element complex-valued FinSequence;coherence

f + g is n -element

proof end;

coherence f - g is n -element ;

coherence

f (#) g is n -element

proof end;

coherence f /" g is n -element ;

registration

let c be Complex;

let n be Nat;

let f be n -element complex-valued FinSequence;

coherence

c + f is n -element

f - c is n -element ;

coherence

c (#) f is n -element

end;
let n be Nat;

let f be n -element complex-valued FinSequence;

coherence

c + f is n -element

proof end;

coherence f - c is n -element ;

coherence

c (#) f is n -element

proof end;

registration

let f be real-valued Function;

coherence

{f} is real-functions-membered by TARSKI:def 1;

let g be real-valued Function;

coherence

{f,g} is real-functions-membered by TARSKI:def 2;

end;
coherence

{f} is real-functions-membered by TARSKI:def 1;

let g be real-valued Function;

coherence

{f,g} is real-functions-membered by TARSKI:def 2;

registration

let n be Nat;

let x, y be object ;

let f be n -element FinSequence;

coherence

f +* (x,y) is n -element

end;
let x, y be object ;

let f be n -element FinSequence;

coherence

f +* (x,y) is n -element

proof end;

theorem :: EUCLID_9:1

definition

let n be Nat;

let f1, f2 be n -element real-valued FinSequence;

the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} is Nat ;

commutativity

for b_{1} being Nat

for f1, f2 being n -element real-valued FinSequence st b_{1} = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds

b_{1} = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))}

end;
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))))};

the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} is Nat ;

commutativity

for b

for f1, f2 being n -element real-valued FinSequence st b

b

proof end;

:: deftheorem defines max_diff_index EUCLID_9:def 1 :

for n being Nat

for f1, f2 being b_{1} -element real-valued FinSequence holds max_diff_index (f1,f2) = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};

for n being Nat

for f1, f2 being b

theorem :: EUCLID_9:4

for n being Nat

for f1, f2 being b_{1} -element real-valued FinSequence st n <> 0 holds

max_diff_index (f1,f2) in dom f1

for f1, f2 being b

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_{2} -element real-valued FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))

for n being Nat

for f1, f2 being b

proof end;

registration
end;

registration
end;

registration
end;

theorem :: EUCLID_9:7

definition
end;

:: deftheorem defines @ EUCLID_9:def 2 :

for n being Nat

for e being Point of (Euclid n) holds @ e = e;

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;

coherence

Ball (e,r) is empty

end;
let e be Point of (Euclid n);

let r be non positive Real;

coherence

Ball (e,r) is empty

proof end;

registration

let n be Nat;

let e be Point of (Euclid n);

let r be positive Real;

coherence

not Ball (e,r) is empty by GOBOARD6:1;

end;
let e be Point of (Euclid n);

let r be positive Real;

coherence

not Ball (e,r) is empty by GOBOARD6:1;

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

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 )

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 )

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;

ex b_{1} being Function st

( dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = ].((f . x) - r),((f . x) + r).[ ) )

for b_{1}, b_{2} being Function st dom b_{1} = dom f & ( for x being object st x in dom f holds

b_{1} . x = ].((f . x) - r),((f . x) + r).[ ) & dom b_{2} = dom f & ( for x being object st x in dom f holds

b_{2} . x = ].((f . x) - r),((f . x) + r).[ ) holds

b_{1} = b_{2}

end;
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 ( dom it = dom f & ( for x being object st x in dom f holds

it . x = ].((f . x) - r),((f . x) + r).[ ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def3 defines Intervals EUCLID_9:def 3 :

for f being real-valued Function

for r being Real

for b_{3} being Function holds

( b_{3} = Intervals (f,r) iff ( dom b_{3} = dom f & ( for x being object st x in dom f holds

b_{3} . x = ].((f . x) - r),((f . x) + r).[ ) ) );

for f being real-valued Function

for r being Real

for b

( b

b

registration
end;

registration

let f be real-valued FinSequence;

let r be Real;

coherence

Intervals (f,r) is FinSequence-like

end;
let r be Real;

coherence

Intervals (f,r) is FinSequence-like

proof end;

definition

let n be Nat;

let e be Point of (Euclid n);

let r be Real;

product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n))

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

product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n))

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

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)

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;

coherence

OpenHypercube (e,r) is empty

end;
let e be Point of (Euclid n);

let r be non positive Real;

coherence

OpenHypercube (e,r) is empty

proof end;

registration

let e be Point of (Euclid 0);

let r be Real;

coherence

not OpenHypercube (e,r) is empty by CARD_3:10;

end;
let r be Real;

coherence

not OpenHypercube (e,r) is empty by CARD_3:10;

registration

let n be Nat;

let e be Point of (Euclid n);

let r be positive Real;

coherence

not OpenHypercube (e,r) is empty by Th11;

end;
let e be Point of (Euclid n);

let r be positive Real;

coherence

not OpenHypercube (e,r) is empty by Th11;

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)

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 )

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)

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)

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)

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

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)

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

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)

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)

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;

coherence

OpenHypercube (e,r) is open

end;
let e be Point of (Euclid n);

let r be Real;

coherence

OpenHypercube (e,r) is open

proof 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

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

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

definition

let n be Nat;

let e be Point of (Euclid n);

{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n))

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

{ (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n))

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

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

coherence

( not OpenHypercubes e is empty & OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )

end;
let e be Point of (Euclid n);

coherence

( not OpenHypercubes e is empty & OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis )

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

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

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

for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds

PP is open

proof end;