:: EUCLID_9 semantic presentation 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 proof s + r <= s - r by XREAL_1:6; hence ].(s - r),(s + r).[ is empty by XXREAL_1:28; ::_thesis: verum end; clusterK508((s - r),(s + r)) -> empty ; coherence [.(s - r),(s + r).[ is empty proof s + r <= s - r by XREAL_1:6; hence [.(s - r),(s + r).[ is empty by XXREAL_1:27; ::_thesis: verum end; clusterK509((s - r),(s + r)) -> empty ; coherence ].(s - r),(s + r).] is empty proof s + r <= s - r by XREAL_1:6; hence ].(s - r),(s + r).] is empty by XXREAL_1:26; ::_thesis: verum end; 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 proof s + r < s - r by XREAL_1:6; hence [.(s - r),(s + r).] is empty by XXREAL_1:29; ::_thesis: verum end; end; registration let n be Nat; let f be complex-valued n -element FinSequence; cluster - f -> n -element ; coherence - f is n -element proof A1: dom (- f) = dom f by VALUED_1:8; len f = n by CARD_1:def_7; hence len (- f) = n by A1, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; clusterf " -> n -element ; coherence f " is n -element proof A2: dom (f ") = dom f by VALUED_1:def_7; len f = n by CARD_1:def_7; hence len (f ") = n by A2, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; clusterf ^2 -> n -element ; coherence f ^2 is n -element proof A3: dom (f ^2) = dom f by VALUED_1:11; len f = n by CARD_1:def_7; hence len (f ^2) = n by A3, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; cluster|.f.| -> n -element ; coherence abs f is n -element proof A4: dom (abs f) = dom f by VALUED_1:def_11; len f = n by CARD_1:def_7; hence len (abs f) = n by A4, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; let g be complex-valued n -element FinSequence; clusterf + g -> n -element ; coherence f + g is n -element proof A5: n in NAT by ORDINAL1:def_12; A6: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def_1; ( len f = n & len g = n ) by CARD_1:def_7; then ( dom f = Seg n & dom g = Seg n ) by FINSEQ_1:def_3; hence len (f + g) = n by A5, A6, FINSEQ_1:def_3; :: according to CARD_1:def_7 ::_thesis: verum end; clusterf - g -> n -element ; coherence f - g is n -element ; clusterf (#) g -> n -element ; coherence f (#) g is n -element proof A7: n in NAT by ORDINAL1:def_12; A8: dom (f (#) g) = (dom f) /\ (dom g) by VALUED_1:def_4; ( len f = n & len g = n ) by CARD_1:def_7; then ( dom f = Seg n & dom g = Seg n ) by FINSEQ_1:def_3; hence len (f (#) g) = n by A7, A8, FINSEQ_1:def_3; :: according to CARD_1:def_7 ::_thesis: verum end; 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 proof A1: dom (c + f) = dom f by VALUED_1:def_2; len f = n by CARD_1:def_7; hence len (c + f) = n by A1, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; clusterf - c -> n -element ; coherence f - c is n -element ; clusterc (#) f -> n -element ; coherence c (#) f is n -element proof A2: dom (c (#) f) = dom f by VALUED_1:def_5; len f = n by CARD_1:def_7; hence len (c (#) f) = n by A2, FINSEQ_3:29; :: according to CARD_1:def_7 ::_thesis: verum end; end; registration let f be real-valued Function; cluster{f} -> real-functions-membered ; coherence {f} is real-functions-membered proof let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in {f} or x is set ) thus ( not x in {f} or x is set ) by TARSKI:def_1; ::_thesis: verum end; let g be real-valued Function; cluster{f,g} -> real-functions-membered ; coherence {f,g} is real-functions-membered proof let x be set ; :: according to VALUED_2:def_4 ::_thesis: ( not x in {f,g} or x is set ) thus ( not x in {f,g} or x is set ) by TARSKI:def_2; ::_thesis: verum end; 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 proof dom (f +* (x,y)) = dom f by FUNCT_7:30; hence len (f +* (x,y)) = len f by FINSEQ_3:29 .= n by CARD_1:def_7 ; :: according to CARD_1:def_7 ::_thesis: verum end; end; theorem Th1: :: EUCLID_9:1 for n being Nat for f being b1 -element FinSequence st f is empty holds n = 0 proof let n be Nat; ::_thesis: for f being n -element FinSequence st f is empty holds n = 0 let f be n -element FinSequence; ::_thesis: ( f is empty implies n = 0 ) assume f is empty ; ::_thesis: n = 0 then A1: dom f = Seg 0 ; len f = n by CARD_1:def_7; hence n = 0 by A1, FINSEQ_1:def_3; ::_thesis: verum end; theorem Th2: :: EUCLID_9:2 for n being Nat for f being real-valued b1 -element FinSequence holds f in REAL n proof let n be Nat; ::_thesis: for f being real-valued n -element FinSequence holds f in REAL n let f be real-valued n -element FinSequence; ::_thesis: f in REAL n rng f c= REAL ; then f is FinSequence of REAL by FINSEQ_1:def_4; then A1: f is Element of REAL * by FINSEQ_1:def_11; len f = n by CARD_1:def_7; hence f in REAL n by A1; ::_thesis: verum end; theorem Th3: :: EUCLID_9:3 for f, g being complex-valued Function holds abs (f - g) = abs (g - f) proof let f, g be complex-valued Function; ::_thesis: abs (f - g) = abs (g - f) f - g = - (g - f) by VALUED_2:18; hence abs (f - g) = abs (g - f) by EUCLID:5; ::_thesis: verum end; 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))))} proof let i be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence st i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} let f1, f2 be real-valued n -element FinSequence; ::_thesis: ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} ) abs (f1 - f2) = abs (f2 - f1) by Th3; hence ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} ) ; ::_thesis: verum end; 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 proof let n be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence st n <> 0 holds max_diff_index (f1,f2) in dom f1 let f1, f2 be real-valued n -element FinSequence; ::_thesis: ( n <> 0 implies max_diff_index (f1,f2) in dom f1 ) set F = abs (f1 - f2); assume n <> 0 ; ::_thesis: max_diff_index (f1,f2) in dom f1 then not abs (f1 - f2) is empty by Th1; then sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def_6; then A1: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} by FUNCT_1:72; A2: dom f1 = Seg n by FINSEQ_1:89; A3: dom (abs (f1 - f2)) = Seg n by FINSEQ_1:89; A4: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} c= dom (abs (f1 - f2)) by RELAT_1:132; max_diff_index (f1,f2) in (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} by A1; hence max_diff_index (f1,f2) in dom f1 by A4, A2, A3; ::_thesis: verum end; 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)) proof let x be set ; ::_thesis: for n being Nat for f1, f2 being real-valued b1 -element FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) let n be Nat; ::_thesis: for f1, f2 being real-valued n -element FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) let f1, f2 be real-valued n -element FinSequence; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) set F = abs (f1 - f2); A1: dom (abs (f1 - f2)) = dom (f1 - f2) by VALUED_1:def_11 .= (dom f1) /\ (dom f2) by VALUED_1:12 ; set m = max_diff_index (f1,f2); A2: ( dom f1 = Seg n & dom f2 = Seg n ) by FINSEQ_1:89; percases ( x in dom f1 or not x in dom f1 ) ; suppose x in dom f1 ; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) then A3: (abs (f1 - f2)) . x in rng (abs (f1 - f2)) by A2, A1, FUNCT_1:def_3; then sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def_6; then (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} by FUNCT_1:72; then (abs (f1 - f2)) . (max_diff_index (f1,f2)) in {(sup (rng (abs (f1 - f2))))} by FUNCT_1:def_7; then (abs (f1 - f2)) . (max_diff_index (f1,f2)) = sup (rng (abs (f1 - f2))) by TARSKI:def_1; hence (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A3, XXREAL_2:4; ::_thesis: verum end; suppose not x in dom f1 ; ::_thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) then A4: not x in dom (abs (f1 - f2)) by A1, XBOOLE_0:def_4; (abs (f1 - f2)) . (max_diff_index (f1,f2)) = abs ((f1 - f2) . (max_diff_index (f1,f2))) by VALUED_1:18; hence (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A4, FUNCT_1:def_2; ::_thesis: verum end; end; 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 proof let a be Element of (Euclid n); :: according to MONOID_0:def_2 ::_thesis: a is set thus a is set ; ::_thesis: verum end; 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 let a be Element of (Euclid n); ::_thesis: a is REAL -valued let y be set ; :: according to RELAT_1:def_19,TARSKI:def_3 ::_thesis: ( not y in rng a or y in REAL ) assume y in rng a ; ::_thesis: y in REAL hence y in REAL by XREAL_0:def_1; ::_thesis: verum 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 A1: TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def_8; thus Family_open_set (Euclid 0) = {{},{{}}} by A1, EUCLID:77, YELLOW_9:9; ::_thesis: verum 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 number ; cluster Ball (e,r) -> empty ; coherence Ball (e,r) is empty proof assume not Ball (e,r) is empty ; ::_thesis: contradiction then consider x being Point of (Euclid n) such that A1: x in Ball (e,r) by SUBSET_1:4; dist (x,e) < r by A1, METRIC_1:11; hence contradiction by METRIC_1:5; ::_thesis: verum end; 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)) proof let n, i be Nat; ::_thesis: for p1, p2 being Point of (TOP-REAL n) st i in dom p1 holds ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( i in dom p1 implies ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) ) assume A1: i in dom p1 ; ::_thesis: ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) set e = sqr (p1 - p2); A2: now__::_thesis:_for_i_being_Nat_st_i_in_dom_(sqr_(p1_-_p2))_holds_ 0_<=_(sqr_(p1_-_p2))_._i let i be Nat; ::_thesis: ( i in dom (sqr (p1 - p2)) implies 0 <= (sqr (p1 - p2)) . i ) assume i in dom (sqr (p1 - p2)) ; ::_thesis: 0 <= (sqr (p1 - p2)) . i (sqr (p1 - p2)) . i = ((p1 - p2) . i) ^2 by VALUED_1:11; hence 0 <= (sqr (p1 - p2)) . i ; ::_thesis: verum end; A3: dom (sqr (p1 - p2)) = dom (p1 - p2) by VALUED_1:11; A4: dom (p1 - p2) = (dom p1) /\ (dom p2) by VALUED_1:12; A5: dom p1 = Seg n by FINSEQ_1:89 .= dom p2 by FINSEQ_1:89 ; A6: p1 . i = p1 /. i by A1, PARTFUN1:def_6; A7: p2 . i = p2 /. i by A1, A5, PARTFUN1:def_6; (sqr (p1 - p2)) . i = ((p1 - p2) . i) ^2 by VALUED_1:11 .= ((p1 /. i) - (p2 /. i)) ^2 by A6, A7, A1, A5, A4, VALUED_1:13 ; hence ((p1 /. i) - (p2 /. i)) ^2 <= Sum (sqr (p1 - p2)) by A1, A2, A3, A5, A4, MATRPROB:5; ::_thesis: verum end; 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 & abs ((a . x) - (o . x)) < r ) proof let n be Nat; ::_thesis: 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 & abs ((a . x) - (o . x)) < r ) let r be real number ; ::_thesis: 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 & abs ((a . x) - (o . x)) < r ) let a, o, p be Element of (TOP-REAL n); ::_thesis: ( a in Ball (o,r) implies for x being set holds ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) ) A1: n in NAT by ORDINAL1:def_12; assume A2: a in Ball (o,r) ; ::_thesis: for x being set holds ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) then A3: |.(a - o).| < r by A1, TOPREAL9:7; 0 <= Sum (sqr (a - o)) by RVSUM_1:86; then (sqrt (Sum (sqr (a - o)))) ^2 = Sum (sqr (a - o)) by SQUARE_1:def_2; then A4: Sum (sqr (a - o)) < r ^2 by A3, SQUARE_1:16; A5: sqr (a - o) = sqr (o - a) by EUCLID:20; A6: r > 0 by A2; let x be set ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) A7: dom (a - o) = (dom a) /\ (dom o) by VALUED_1:12; A8: ( dom a = Seg n & dom o = Seg n ) by FINSEQ_1:89; percases ( x in dom a or not x in dom a ) ; supposeA9: x in dom a ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) then reconsider x = x as Nat ; A10: (a - o) . x = (a . x) - (o . x) by A9, A7, A8, VALUED_1:13; A11: ( a /. x = a . x & o /. x = o . x ) by A9, A8, PARTFUN1:def_6; now__::_thesis:_not_(o_._x)_-_(a_._x)_>=_r assume (o . x) - (a . x) >= r ; ::_thesis: contradiction then A12: ((o . x) - (a . x)) ^2 >= r ^2 by A6, SQUARE_1:15; Sum (sqr (o - a)) >= ((o /. x) - (a /. x)) ^2 by A9, A8, Th8; hence contradiction by A4, A12, A5, A11, XXREAL_0:2; ::_thesis: verum end; then A13: (o . x) - r < a . x by XREAL_1:11; now__::_thesis:_not_(a_._x)_-_(o_._x)_>=_r assume (a . x) - (o . x) >= r ; ::_thesis: contradiction then A14: ((a . x) - (o . x)) ^2 >= r ^2 by A6, SQUARE_1:15; Sum (sqr (a - o)) >= ((a /. x) - (o /. x)) ^2 by A9, Th8; hence contradiction by A4, A14, A11, XXREAL_0:2; ::_thesis: verum end; then a . x < (o . x) + r by XREAL_1:19; hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A10, A13, RINFSUP1:1; ::_thesis: verum end; supposeA15: not x in dom a ; ::_thesis: ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) then not x in dom (abs (a - o)) by A7, A8, VALUED_1:def_11; then (abs (a - o)) . x = 0 by FUNCT_1:def_2; then A16: abs ((a - o) . x) = 0 by VALUED_1:18; ( a . x = 0 & o . x = 0 ) by A8, A15, FUNCT_1:def_2; hence ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) by A16, A2; ::_thesis: verum end; end; end; 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 & abs ((a . x) - (o . x)) < r ) proof let n be Nat; ::_thesis: 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 & abs ((a . x) - (o . x)) < r ) let r be real number ; ::_thesis: 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 & abs ((a . x) - (o . x)) < r ) let a, o be Point of (Euclid n); ::_thesis: ( a in Ball (o,r) implies for x being set holds ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) ) reconsider a1 = a, o1 = o as Point of (TOP-REAL n) by EUCLID:67; n in NAT by ORDINAL1:def_12; then A1: Ball (o,r) = Ball (o1,r) by TOPREAL9:13; a - o = a1 - o1 ; hence ( a in Ball (o,r) implies for x being set holds ( abs ((a - o) . x) < r & abs ((a . x) - (o . x)) < r ) ) by A1, Th9; ::_thesis: verum end; 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 & ( 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 & ( for x being set st x in dom f holds b1 . x = ].((f . x) - r),((f . x) + r).[ ) ) proof deffunc H1( set ) -> Element of K19(REAL) = ].((f . \$1) - r),((f . \$1) + r).[; ex g being Function st ( dom g = dom f & ( for x being set st x in dom f holds g . x = H1(x) ) ) from FUNCT_1:sch_3(); hence ex b1 being Function st ( dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = ].((f . x) - r),((f . x) + r).[ ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = dom f & ( for x being set st x in dom f holds b1 . x = ].((f . x) - r),((f . x) + r).[ ) & dom b2 = dom f & ( for x being set st x in dom f holds b2 . x = ].((f . x) - r),((f . x) + r).[ ) holds b1 = b2 proof let g, h be Function; ::_thesis: ( dom g = dom f & ( for x being set st x in dom f holds g . x = ].((f . x) - r),((f . x) + r).[ ) & dom h = dom f & ( for x being set st x in dom f holds h . x = ].((f . x) - r),((f . x) + r).[ ) implies g = h ) assume that A1: dom g = dom f and A2: for x being set st x in dom f holds g . x = ].((f . x) - r),((f . x) + r).[ and A3: dom h = dom f and A4: for x being set st x in dom f holds h . x = ].((f . x) - r),((f . x) + r).[ ; ::_thesis: g = h now__::_thesis:_for_x_being_set_st_x_in_dom_g_holds_ g_._x_=_h_._x let x be set ; ::_thesis: ( x in dom g implies g . x = h . x ) assume A5: x in dom g ; ::_thesis: g . x = h . x hence g . x = ].((f . x) - r),((f . x) + r).[ by A1, A2 .= h . x by A1, A4, A5 ; ::_thesis: verum end; hence g = h by A1, A3, FUNCT_1:2; ::_thesis: verum end; 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 & ( 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 proof dom (Intervals ({},r)) = dom {} by Def3; hence Intervals ({},r) is empty ; ::_thesis: verum end; 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 proof take len f ; :: according to FINSEQ_1:def_2 ::_thesis: dom (Intervals (f,r)) = Seg (len f) dom (Intervals (f,r)) = dom f by Def3; hence dom (Intervals (f,r)) = Seg (len f) by FINSEQ_1:def_3; ::_thesis: verum end; 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)) proof set T = TopSpaceMetr (Euclid n); set f = Intervals (e,r); product (Intervals (e,r)) c= the carrier of (TopSpaceMetr (Euclid n)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Intervals (e,r)) or x in the carrier of (TopSpaceMetr (Euclid n)) ) assume x in product (Intervals (e,r)) ; ::_thesis: x in the carrier of (TopSpaceMetr (Euclid n)) then consider g being Function such that A1: x = g and A2: dom g = dom (Intervals (e,r)) and A3: for y being set st y in dom (Intervals (e,r)) holds g . y in (Intervals (e,r)) . y by CARD_3:def_5; A4: dom (Intervals (e,r)) = dom e by Def3; dom e = Seg n by FINSEQ_1:89; then reconsider x = x as FinSequence by A1, A2, A4, FINSEQ_1:def_2; rng x c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng x or b in REAL ) assume b in rng x ; ::_thesis: b in REAL then consider a being set such that A5: a in dom x and A6: x . a = b by FUNCT_1:def_3; A7: g . a in (Intervals (e,r)) . a by A1, A2, A3, A5; (Intervals (e,r)) . a = ].((e . a) - r),((e . a) + r).[ by A1, A2, A4, A5, Def3; hence b in REAL by A1, A6, A7; ::_thesis: verum end; then x is FinSequence of REAL by FINSEQ_1:def_4; then A8: x in REAL * by FINSEQ_1:def_11; len e = n by CARD_1:def_7; then len x = n by A1, A2, A4, FINSEQ_3:29; hence x in the carrier of (TopSpaceMetr (Euclid n)) by A8; ::_thesis: verum end; hence product (Intervals (e,r)) is Subset of (TopSpaceMetr (Euclid n)) ; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: for r being real number for e being Point of (Euclid n) st 0 < r holds e in OpenHypercube (e,r) let r be real number ; ::_thesis: for e being Point of (Euclid n) st 0 < r holds e in OpenHypercube (e,r) let e be Point of (Euclid n); ::_thesis: ( 0 < r implies e in OpenHypercube (e,r) ) assume A1: 0 < r ; ::_thesis: e in OpenHypercube (e,r) set f = Intervals (e,r); A2: dom (Intervals (e,r)) = dom e by Def3; now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_ e_._x_in_(Intervals_(e,r))_._x let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies e . x in (Intervals (e,r)) . x ) assume x in dom (Intervals (e,r)) ; ::_thesis: e . x in (Intervals (e,r)) . x then A3: (Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A2, Def3; A4: (e . x) - r < (e . x) - 0 by A1, XREAL_1:10; (e . x) + 0 < (e . x) + r by A1, XREAL_1:8; hence e . x in (Intervals (e,r)) . x by A3, A4, XXREAL_1:4; ::_thesis: verum end; hence e in OpenHypercube (e,r) by A2, CARD_3:9; ::_thesis: verum end; 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 proof assume not OpenHypercube (e,r) is empty ; ::_thesis: contradiction then consider x being set such that A1: x in OpenHypercube (e,r) by XBOOLE_0:def_1; reconsider e1 = e as real-valued Function ; set f = Intervals (e,r); A2: dom (Intervals (e,r)) = dom e by Def3; A3: dom e = Seg n by FINSEQ_1:89; consider N being set such that A4: N in Seg n by XBOOLE_0:def_1; (Intervals (e,r)) . N = ].((e1 . N) - r),((e1 . N) + r).[ by A4, A3, Def3; hence contradiction by A1, A2, A3, A4, CARD_3:9; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: for r, s being real number for e being Point of (Euclid n) st r <= s holds OpenHypercube (e,r) c= OpenHypercube (e,s) let r, s be real number ; ::_thesis: for e being Point of (Euclid n) st r <= s holds OpenHypercube (e,r) c= OpenHypercube (e,s) let e be Point of (Euclid n); ::_thesis: ( r <= s implies OpenHypercube (e,r) c= OpenHypercube (e,s) ) assume A1: r <= s ; ::_thesis: OpenHypercube (e,r) c= OpenHypercube (e,s) A2: dom (Intervals (e,s)) = dom e by Def3; A3: dom (Intervals (e,r)) = dom e by Def3; now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_ (Intervals_(e,r))_._x_c=_(Intervals_(e,s))_._x let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies (Intervals (e,r)) . x c= (Intervals (e,s)) . x ) assume A4: x in dom (Intervals (e,r)) ; ::_thesis: (Intervals (e,r)) . x c= (Intervals (e,s)) . x reconsider u = e . x as real number ; A5: ( (Intervals (e,r)) . x = ].(u - r),(u + r).[ & (Intervals (e,s)) . x = ].(u - s),(u + s).[ ) by A4, A3, Def3; ( u - s <= u - r & u + r <= u + s ) by A1, XREAL_1:6, XREAL_1:10; hence (Intervals (e,r)) . x c= (Intervals (e,s)) . x by A5, XXREAL_1:46; ::_thesis: verum end; hence OpenHypercube (e,r) c= OpenHypercube (e,s) by A2, A3, CARD_3:27; ::_thesis: verum end; 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 ) & e1 in OpenHypercube (e,r) holds for x being set holds ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) proof let n be Nat; ::_thesis: for r being real number for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds for x being set holds ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) holds for x being set holds ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) let e1, e be Point of (Euclid n); ::_thesis: ( ( n <> 0 or 0 < r ) & e1 in OpenHypercube (e,r) implies for x being set holds ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) ) assume that A1: ( n <> 0 or 0 < r ) and A2: e1 in OpenHypercube (e,r) ; ::_thesis: for x being set holds ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) A3: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89; A4: dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12; let x be set ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) percases ( x in dom e1 or not x in dom e1 ) ; supposeA5: x in dom e1 ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) then A6: (e1 - e) . x = (e1 . x) - (e . x) by A3, A4, VALUED_1:13; A7: ( e1 . x in REAL & e . x in REAL & r in REAL ) by XREAL_0:def_1; dom e = dom (Intervals (e,r)) by Def3; then A8: e1 . x in (Intervals (e,r)) . x by A5, A3, A2, CARD_3:9; (Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A3, A5, Def3; hence ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A6, A8, A7, FCONT_3:1; ::_thesis: verum end; supposeA9: not x in dom e1 ; ::_thesis: ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) then not x in dom (abs (e1 - e)) by A4, A3, VALUED_1:def_11; then (abs (e1 - e)) . x = 0 by FUNCT_1:def_2; then A10: abs ((e1 - e) . x) = 0 by VALUED_1:18; ( e1 . x = 0 & e . x = 0 ) by A3, A9, FUNCT_1:def_2; hence ( abs ((e1 - e) . x) < r & abs ((e1 . x) - (e . x)) < r ) by A10, A1, A2; ::_thesis: verum end; end; end; 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 & e1 in OpenHypercube (e,r) holds Sum (sqr (e1 - e)) < n * (r ^2) proof let n be Nat; ::_thesis: for r being real number for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds Sum (sqr (e1 - e)) < n * (r ^2) let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds Sum (sqr (e1 - e)) < n * (r ^2) let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies Sum (sqr (e1 - e)) < n * (r ^2) ) assume that A1: n <> 0 and A2: e1 in OpenHypercube (e,r) ; ::_thesis: Sum (sqr (e1 - e)) < n * (r ^2) set R1 = sqr (e1 - e); set R2 = n |-> (r ^2); A3: REAL n = n -tuples_on REAL ; A4: sqr (e1 - e) in n -tuples_on REAL by Th2; A5: n |-> (r ^2) in n -tuples_on REAL by A3, Th2; A6: now__::_thesis:_for_i_being_Nat_st_i_in_Seg_n_holds_ (sqr_(e1_-_e))_._i_<_(n_|->_(r_^2))_._i let i be Nat; ::_thesis: ( i in Seg n implies (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) assume A7: i in Seg n ; ::_thesis: (sqr (e1 - e)) . i < (n |-> (r ^2)) . i A8: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89; dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12; then A9: (e1 - e) . i = (e1 . i) - (e . i) by A7, A8, VALUED_1:13; A10: (sqr (e1 - e)) . i = ((e1 - e) . i) ^2 by VALUED_1:11; A11: (n |-> (r ^2)) . i = r ^2 by A7, FINSEQ_2:57; A12: abs ((e1 . i) - (e . i)) < r by A1, A2, Th14; ((e1 - e) . i) ^2 = (abs ((e1 - e) . i)) ^2 by COMPLEX1:75; hence (sqr (e1 - e)) . i < (n |-> (r ^2)) . i by A9, A10, A11, A12, SQUARE_1:16; ::_thesis: verum end; then A13: for i being Nat st i in Seg n holds (sqr (e1 - e)) . i <= (n |-> (r ^2)) . i ; ex i being Nat st ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) proof consider i being set such that A14: i in Seg n by A1, XBOOLE_0:def_1; reconsider i = i as Nat by A14; take i ; ::_thesis: ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) thus ( i in Seg n & (sqr (e1 - e)) . i < (n |-> (r ^2)) . i ) by A14, A6; ::_thesis: verum end; then Sum (sqr (e1 - e)) < Sum (n |-> (r ^2)) by A4, A5, A13, RVSUM_1:83; hence Sum (sqr (e1 - e)) < n * (r ^2) by RVSUM_1:80; ::_thesis: verum end; 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 & e1 in OpenHypercube (e,r) holds dist (e1,e) < r * (sqrt n) proof let n be Nat; ::_thesis: for r being real number for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds dist (e1,e) < r * (sqrt n) let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds dist (e1,e) < r * (sqrt n) let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies dist (e1,e) < r * (sqrt n) ) assume that A1: n <> 0 and A2: e1 in OpenHypercube (e,r) ; ::_thesis: dist (e1,e) < r * (sqrt n) A3: dist (e1,e) = |.(e1 - e).| by EUCLID:def_6; 0 <= Sum (sqr (e1 - e)) by RVSUM_1:86; then A4: sqrt (Sum (sqr (e1 - e))) < sqrt (n * (r ^2)) by A1, A2, Th15, SQUARE_1:27; 0 <= r by A1, A2; then sqrt (r ^2) = r by SQUARE_1:22; hence dist (e1,e) < r * (sqrt n) by A3, A4, SQUARE_1:29; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: 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) let r be real number ; ::_thesis: for e being Point of (Euclid n) st n <> 0 holds OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r) let e be Point of (Euclid n); ::_thesis: ( n <> 0 implies OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r) ) assume A1: n <> 0 ; ::_thesis: OpenHypercube (e,(r / (sqrt n))) c= Ball (e,r) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in OpenHypercube (e,(r / (sqrt n))) or x in Ball (e,r) ) assume A2: x in OpenHypercube (e,(r / (sqrt n))) ; ::_thesis: x in Ball (e,r) then reconsider x = x as Point of (Euclid n) ; A3: dist (x,e) < (r / (sqrt n)) * (sqrt n) by A1, A2, Th16; (r / (sqrt n)) * (sqrt n) = r by A1, XCMPLX_1:87; hence x in Ball (e,r) by A3, METRIC_1:11; ::_thesis: verum end; 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))) proof let n be Nat; ::_thesis: 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))) let r be real number ; ::_thesis: for e being Point of (Euclid n) st n <> 0 holds OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) let e be Point of (Euclid n); ::_thesis: ( n <> 0 implies OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) ) assume A1: n <> 0 ; ::_thesis: OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) then A2: OpenHypercube (e,((r * (sqrt n)) / (sqrt n))) c= Ball (e,(r * (sqrt n))) by Th17; (r / (sqrt n)) * (sqrt n) = r by A1, XCMPLX_1:87; hence OpenHypercube (e,r) c= Ball (e,(r * (sqrt n))) by A2, XCMPLX_1:74; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: 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) let r be real number ; ::_thesis: 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) let e1, e be Point of (Euclid n); ::_thesis: ( e1 in Ball (e,r) implies ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ) reconsider B = Ball (e,r) as Subset of (TopSpaceMetr (Euclid n)) ; assume A1: e1 in Ball (e,r) ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) B is open by TOPMETR:14; then consider s being real number such that A2: s > 0 and A3: Ball (e1,s) c= B by A1, TOPMETR:15; A4: s / (sqrt n) is Real by XREAL_0:def_1; percases ( n <> 0 or n = 0 ) ; supposeA5: n <> 0 ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) then consider m being Element of NAT such that A6: 1 / m < s / (sqrt n) and A7: m > 0 by A2, A4, FRECHET:36; reconsider m = m as non zero Element of NAT by A7; A8: OpenHypercube (e1,(s / (sqrt n))) c= Ball (e1,s) by A5, Th17; OpenHypercube (e1,(1 / m)) c= OpenHypercube (e1,(s / (sqrt n))) by A6, Th13; then OpenHypercube (e1,(1 / m)) c= Ball (e1,s) by A8, XBOOLE_1:1; hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) by A3, XBOOLE_1:1; ::_thesis: verum end; suppose n = 0 ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) then ( ( OpenHypercube (e1,(1 / 1)) = {} or OpenHypercube (e1,(1 / 1)) = {{}} ) & Ball (e,r) = {{}} ) by A1, EUCLID:77, ZFMISC_1:33; hence ex m being non zero Element of NAT st OpenHypercube (e1,(1 / m)) c= Ball (e,r) ; ::_thesis: verum end; end; end; 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 & e1 in OpenHypercube (e,r) holds r > (abs (e1 - e)) . (max_diff_index (e1,e)) proof let n be Nat; ::_thesis: for r being real number for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds r > (abs (e1 - e)) . (max_diff_index (e1,e)) let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) st n <> 0 & e1 in OpenHypercube (e,r) holds r > (abs (e1 - e)) . (max_diff_index (e1,e)) let e1, e be Point of (Euclid n); ::_thesis: ( n <> 0 & e1 in OpenHypercube (e,r) implies r > (abs (e1 - e)) . (max_diff_index (e1,e)) ) set d = max_diff_index (e1,e); (abs (e1 - e)) . (max_diff_index (e1,e)) = abs ((e1 - e) . (max_diff_index (e1,e))) by VALUED_1:18; hence ( n <> 0 & e1 in OpenHypercube (e,r) implies r > (abs (e1 - e)) . (max_diff_index (e1,e)) ) by Th14; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: 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) let r be real number ; ::_thesis: for e1, e being Point of (Euclid n) holds OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r) let e1, e be Point of (Euclid n); ::_thesis: OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) c= OpenHypercube (e,r) set d = max_diff_index (e1,e); set F = abs (e1 - e); set s = r - ((abs (e1 - e)) . (max_diff_index (e1,e))); A1: ( dom e1 = Seg n & dom e = Seg n ) by FINSEQ_1:89; let y be Point of (TopSpaceMetr (Euclid n)); :: according to LATTICE7:def_1 ::_thesis: ( not y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) or y in OpenHypercube (e,r) ) assume A2: y in OpenHypercube (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e))))) ; ::_thesis: y in OpenHypercube (e,r) reconsider y = y as Point of (Euclid n) ; A3: dom y = dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) by A2, CARD_3:9; A4: dom (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) = dom e1 by Def3; then A5: dom y = dom (Intervals (e,r)) by A1, A3, Def3; now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_ y_._x_in_(Intervals_(e,r))_._x let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies y . x in (Intervals (e,r)) . x ) assume A6: x in dom (Intervals (e,r)) ; ::_thesis: y . x in (Intervals (e,r)) . x then A7: (Intervals (e,r)) . x = ].((e . x) - r),((e . x) + r).[ by A1, A3, A4, A5, Def3; A8: (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x = ].((e1 . x) - (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))),((e1 . x) + (r - ((abs (e1 - e)) . (max_diff_index (e1,e))))).[ by A3, A4, A5, A6, Def3; y . x in (Intervals (e1,(r - ((abs (e1 - e)) . (max_diff_index (e1,e)))))) . x by A2, A3, A5, A6, CARD_3:9; then A9: abs ((y . x) - (e1 . x)) < r - ((abs (e1 - e)) . (max_diff_index (e1,e))) by A8, RCOMP_1:1; dom (e1 - e) = (dom e1) /\ (dom e) by VALUED_1:12; then abs ((e1 . x) - (e . x)) = abs ((e1 - e) . x) by A1, A3, A4, A5, A6, VALUED_1:13 .= (abs (e1 - e)) . x by VALUED_1:18 ; then A10: (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) < (r - ((abs (e1 - e)) . (max_diff_index (e1,e)))) + ((abs (e1 - e)) . (max_diff_index (e1,e))) by A9, Th5, XREAL_1:8; abs ((y . x) - (e . x)) <= (abs ((y . x) - (e1 . x))) + (abs ((e1 . x) - (e . x))) by COMPLEX1:63; then abs ((y . x) - (e . x)) < r by A10, XXREAL_0:2; hence y . x in (Intervals (e,r)) . x by A7, RCOMP_1:1; ::_thesis: verum end; hence y in OpenHypercube (e,r) by A5, CARD_3:9; ::_thesis: verum end; 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) proof let n be Nat; ::_thesis: for r being real number for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r) let r be real number ; ::_thesis: for e being Point of (Euclid n) holds Ball (e,r) c= OpenHypercube (e,r) let e be Point of (Euclid n); ::_thesis: Ball (e,r) c= OpenHypercube (e,r) let g be set ; :: according to TARSKI:def_3 ::_thesis: ( not g in Ball (e,r) or g in OpenHypercube (e,r) ) assume A1: g in Ball (e,r) ; ::_thesis: g in OpenHypercube (e,r) then reconsider g = g as Point of (Euclid n) ; A2: dom (Intervals (e,r)) = dom e by Def3; A3: ( dom g = Seg n & dom e = Seg n ) by FINSEQ_1:89; now__::_thesis:_for_x_being_set_st_x_in_dom_(Intervals_(e,r))_holds_ g_._x_in_(Intervals_(e,r))_._x let x be set ; ::_thesis: ( x in dom (Intervals (e,r)) implies g . x in (Intervals (e,r)) . x ) reconsider u = e . x, v = g . x as Real by XREAL_0:def_1; assume A4: x in dom (Intervals (e,r)) ; ::_thesis: g . x in (Intervals (e,r)) . x then A5: (Intervals (e,r)) . x = ].(u - r),(u + r).[ by A2, Def3; dom (g - e) = (dom g) /\ (dom e) by VALUED_1:12; then A6: (g - e) . x = v - u by A2, A3, A4, VALUED_1:13; A7: v = u + (v - u) ; abs ((g - e) . x) < r by A1, Th10; hence g . x in (Intervals (e,r)) . x by A6, A5, A7, FCONT_3:3; ::_thesis: verum end; hence g in OpenHypercube (e,r) by A2, A3, CARD_3:9; ::_thesis: verum end; 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 proof percases ( n <> 0 or n = 0 ) ; supposeA1: n <> 0 ; ::_thesis: OpenHypercube (e,r) is open for p being Point of (Euclid n) st p in OpenHypercube (e,r) holds ex s being real number st ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) proof let p be Point of (Euclid n); ::_thesis: ( p in OpenHypercube (e,r) implies ex s being real number st ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) ) assume A2: p in OpenHypercube (e,r) ; ::_thesis: ex s being real number st ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) set d = (abs (p - e)) . (max_diff_index (p,e)); take s = r - ((abs (p - e)) . (max_diff_index (p,e))); ::_thesis: ( s > 0 & Ball (p,s) c= OpenHypercube (e,r) ) r - ((abs (p - e)) . (max_diff_index (p,e))) > ((abs (p - e)) . (max_diff_index (p,e))) - ((abs (p - e)) . (max_diff_index (p,e))) by A1, A2, Th20, XREAL_1:8; hence s > 0 ; ::_thesis: Ball (p,s) c= OpenHypercube (e,r) A3: OpenHypercube (p,s) c= OpenHypercube (e,r) by Th21; Ball (p,s) c= OpenHypercube (p,s) by Th22; hence Ball (p,s) c= OpenHypercube (e,r) by A3, XBOOLE_1:1; ::_thesis: verum end; hence OpenHypercube (e,r) is open by TOPMETR:15; ::_thesis: verum end; supposeA4: n = 0 ; ::_thesis: OpenHypercube (e,r) is open then OpenHypercube (e,r) = {{}} by Th12; then OpenHypercube (e,r) in the topology of (TopSpaceMetr (Euclid 0)) by Th6, TARSKI:def_2; hence OpenHypercube (e,r) is open by A4, PRE_TOPC:def_2; ::_thesis: verum end; end; 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 let n be Nat; ::_thesis: 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 let V be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( V is open implies 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 ) assume A1: V is open ; ::_thesis: 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 let e be Point of (Euclid n); ::_thesis: ( e in V implies ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V ) assume e in V ; ::_thesis: ex m being non zero Element of NAT st OpenHypercube (e,(1 / m)) c= V then consider r being real number such that A2: r > 0 and A3: Ball (e,r) c= V by A1, TOPMETR:15; consider m being non zero Element of NAT such that A4: OpenHypercube (e,(1 / m)) c= Ball (e,r) by A2, Th19, GOBOARD6:1; take m ; ::_thesis: OpenHypercube (e,(1 / m)) c= V thus OpenHypercube (e,(1 / m)) c= V by A3, A4, XBOOLE_1:1; ::_thesis: verum 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 number st ( r > 0 & OpenHypercube (e,r) c= V ) ) holds V is open proof let n be Nat; ::_thesis: 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 & OpenHypercube (e,r) c= V ) ) holds V is open let V be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( ( for e being Point of (Euclid n) st e in V holds ex r being real number st ( r > 0 & OpenHypercube (e,r) c= V ) ) implies V is open ) assume A1: for e being Point of (Euclid n) st e in V holds ex r being real number st ( r > 0 & OpenHypercube (e,r) c= V ) ; ::_thesis: V is open for e being Point of (Euclid n) st e in V holds ex r being real number st ( r > 0 & Ball (e,r) c= V ) proof let e be Point of (Euclid n); ::_thesis: ( e in V implies ex r being real number st ( r > 0 & Ball (e,r) c= V ) ) assume e in V ; ::_thesis: ex r being real number st ( r > 0 & Ball (e,r) c= V ) then consider r being real number such that A2: r > 0 and A3: OpenHypercube (e,r) c= V by A1; Ball (e,r) c= OpenHypercube (e,r) by Th22; hence ex r being real number st ( r > 0 & Ball (e,r) c= V ) by A2, A3, XBOOLE_1:1; ::_thesis: verum end; hence V is open by TOPMETR:15; ::_thesis: verum 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 H1(n,e) c= bool the carrier of (TopSpaceMetr (Euclid n)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1(n,e) or x in bool the carrier of (TopSpaceMetr (Euclid n)) ) assume x in H1(n,e) ; ::_thesis: x in bool the carrier of (TopSpaceMetr (Euclid n)) then ex m being non zero Element of NAT st x = OpenHypercube (e,(1 / m)) ; hence x in bool the carrier of (TopSpaceMetr (Euclid n)) by ZFMISC_1:def_1; ::_thesis: verum end; hence { (OpenHypercube (e,(1 / m))) where m is non zero Element of NAT : verum } is Subset-Family of (TopSpaceMetr (Euclid n)) ; ::_thesis: verum 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 set T = TopSpaceMetr (Euclid n); OpenHypercube (e,(1 / 1)) in OpenHypercubes e ; hence not OpenHypercubes e is empty ; ::_thesis: ( OpenHypercubes e is open & OpenHypercubes e is @ e -quasi_basis ) hereby :: according to TOPS_2:def_1 ::_thesis: OpenHypercubes e is @ e -quasi_basis let A be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( A in OpenHypercubes e implies A is open ) assume A in OpenHypercubes e ; ::_thesis: A is open then ex m being non zero Element of NAT st A = OpenHypercube (e,(1 / m)) ; hence A is open ; ::_thesis: verum end; now__::_thesis:_for_Y_being_set_st_Y_in_OpenHypercubes_e_holds_ @_e_in_Y let Y be set ; ::_thesis: ( Y in OpenHypercubes e implies @ e in Y ) assume Y in OpenHypercubes e ; ::_thesis: @ e in Y then ex m being non zero Element of NAT st Y = OpenHypercube (e,(1 / m)) ; hence @ e in Y by Th11; ::_thesis: verum end; hence @ e in Intersect (OpenHypercubes e) by SETFAM_1:43; :: according to YELLOW_8:def_1 ::_thesis: for b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) holds ( not b1 is open or not @ e in b1 or ex b2 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st ( b2 in OpenHypercubes e & b2 c= b1 ) ) let S be Subset of (TopSpaceMetr (Euclid n)); ::_thesis: ( not S is open or not @ e in S or ex b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st ( b1 in OpenHypercubes e & b1 c= S ) ) assume that A1: S is open and A2: @ e in S ; ::_thesis: ex b1 being Element of K19( the carrier of (TopSpaceMetr (Euclid n))) st ( b1 in OpenHypercubes e & b1 c= S ) consider r being real number such that A3: r > 0 and A4: Ball (e,r) c= S by A1, A2, TOPMETR:15; consider m being non zero Element of NAT such that A5: OpenHypercube (e,(1 / m)) c= Ball (e,r) by A3, Th19, GOBOARD6:1; take V = OpenHypercube (e,(1 / m)); ::_thesis: ( V in OpenHypercubes e & V c= S ) thus V in OpenHypercubes e ; ::_thesis: V c= S thus V c= S by A4, A5, XBOOLE_1:1; ::_thesis: verum 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 let n be Nat; ::_thesis: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) set J = (Seg n) --> R^1; set C = Carrier ((Seg n) --> R^1); A1: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2; thus Funcs ((Seg n),REAL) c= product (Carrier ((Seg n) --> R^1)) :: according to XBOOLE_0:def_10 ::_thesis: product (Carrier ((Seg n) --> R^1)) c= Funcs ((Seg n),REAL) proof let f be set ; :: according to TARSKI:def_3 ::_thesis: ( not f in Funcs ((Seg n),REAL) or f in product (Carrier ((Seg n) --> R^1)) ) assume f in Funcs ((Seg n),REAL) ; ::_thesis: f in product (Carrier ((Seg n) --> R^1)) then reconsider f = f as Function of (Seg n),REAL by FUNCT_2:66; A2: dom f = Seg n by FUNCT_2:def_1; now__::_thesis:_for_x_being_set_st_x_in_dom_(Carrier_((Seg_n)_-->_R^1))_holds_ f_._x_in_(Carrier_((Seg_n)_-->_R^1))_._x let x be set ; ::_thesis: ( x in dom (Carrier ((Seg n) --> R^1)) implies f . x in (Carrier ((Seg n) --> R^1)) . x ) assume A3: x in dom (Carrier ((Seg n) --> R^1)) ; ::_thesis: f . x in (Carrier ((Seg n) --> R^1)) . x then A4: ex R being 1-sorted st ( R = ((Seg n) --> R^1) . x & (Carrier ((Seg n) --> R^1)) . x = the carrier of R ) by PRALG_1:def_13; f . x in REAL by A3, FUNCT_2:5; hence f . x in (Carrier ((Seg n) --> R^1)) . x by A4, A3, FUNCOP_1:7; ::_thesis: verum end; hence f in product (Carrier ((Seg n) --> R^1)) by A2, A1, CARD_3:9; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in product (Carrier ((Seg n) --> R^1)) or x in Funcs ((Seg n),REAL) ) assume x in product (Carrier ((Seg n) --> R^1)) ; ::_thesis: x in Funcs ((Seg n),REAL) then consider g being Function such that A5: x = g and A6: dom g = dom (Carrier ((Seg n) --> R^1)) and A7: for y being set st y in dom (Carrier ((Seg n) --> R^1)) holds g . y in (Carrier ((Seg n) --> R^1)) . y by CARD_3:def_5; rng g c= REAL proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng g or z in REAL ) assume z in rng g ; ::_thesis: z in REAL then consider a being set such that A8: a in dom g and A9: g . a = z by FUNCT_1:def_3; A10: ex R being 1-sorted st ( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A6, A8, PRALG_1:def_13; ((Seg n) --> R^1) . a = R^1 by A6, A8, FUNCOP_1:7; hence z in REAL by A6, A7, A8, A9, A10; ::_thesis: verum end; hence x in Funcs ((Seg n),REAL) by A1, A5, A6, FUNCT_2:def_2; ::_thesis: verum 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 let n be Nat; ::_thesis: ( n <> 0 implies for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds PP is quasi_prebasis ) assume A1: n <> 0 ; ::_thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds PP is quasi_prebasis set E = Euclid n; set T = TopSpaceMetr (Euclid n); let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ::_thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is quasi_prebasis ) set J = (Seg n) --> R^1; set C = Carrier ((Seg n) --> R^1); set S = Seg n; reconsider S = Seg n as non empty finite set by A1; assume A2: PP = product_prebasis ((Seg n) --> R^1) ; ::_thesis: PP is quasi_prebasis A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93; A4: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2; A5: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25; defpred S1[ set , set ] means ex e being Point of (Euclid n) st ( e = \$1 & \$2 = OpenHypercubes e ); A6: for i being Element of (TopSpaceMetr (Euclid n)) ex j being set st S1[i,j] proof let i be Element of (TopSpaceMetr (Euclid n)); ::_thesis: ex j being set st S1[i,j] reconsider j = i as Point of (Euclid n) ; take OpenHypercubes j ; ::_thesis: S1[i, OpenHypercubes j] take j ; ::_thesis: ( j = i & OpenHypercubes j = OpenHypercubes j ) thus ( j = i & OpenHypercubes j = OpenHypercubes j ) ; ::_thesis: verum end; consider NS being ManySortedSet of (TopSpaceMetr (Euclid n)) such that A7: for x being Point of (TopSpaceMetr (Euclid n)) holds S1[x,NS . x] from PBOOLE:sch_6(A6); now__::_thesis:_for_x_being_Point_of_(TopSpaceMetr_(Euclid_n))_holds_NS_._x_is_Basis_of_x let x be Point of (TopSpaceMetr (Euclid n)); ::_thesis: NS . x is Basis of x reconsider y = x as Point of (Euclid n) ; S1[y,NS . y] by A7; hence NS . x is Basis of x ; ::_thesis: verum end; then reconsider NS = NS as Neighborhood_System of TopSpaceMetr (Euclid n) by TOPGEN_2:def_3; take B = Union NS; :: according to CANTOR_1:def_4 ::_thesis: B c= FinMeetCl PP let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in B or b in FinMeetCl PP ) assume b in B ; ::_thesis: b in FinMeetCl PP then consider Z being set such that A8: b in Z and A9: Z in rng NS by TARSKI:def_4; consider x being set such that A10: x in dom NS and A11: NS . x = Z by A9, FUNCT_1:def_3; reconsider x = x as Point of (Euclid n) by A10; A12: dom x = Seg n by FINSEQ_1:89; S1[x,NS . x] by A7; then consider m being non zero Element of NAT such that A13: b = OpenHypercube (x,(1 / m)) by A8, A11; deffunc H2( set ) -> set = product ((Carrier ((Seg n) --> R^1)) +* (\$1,(R^1 ].((x . \$1) - (1 / m)),((x . \$1) + (1 / m)).[))); defpred S2[ set ] means verum; set Y = { H2(q) where q is Element of S : S2[q] } ; A14: { H2(q) where q is Element of S : S2[q] } is finite from PRE_CIRC:sch_1(); { H2(q) where q is Element of S : S2[q] } c= bool the carrier of (TopSpaceMetr (Euclid n)) proof let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { H2(q) where q is Element of S : S2[q] } or s in bool the carrier of (TopSpaceMetr (Euclid n)) ) assume s in { H2(q) where q is Element of S : S2[q] } ; ::_thesis: s in bool the carrier of (TopSpaceMetr (Euclid n)) then consider q being Element of S such that A15: s = H2(q) ; H2(q) c= the carrier of (TopSpaceMetr (Euclid n)) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in H2(q) or z in the carrier of (TopSpaceMetr (Euclid n)) ) set f = (Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[)); assume z in H2(q) ; ::_thesis: z in the carrier of (TopSpaceMetr (Euclid n)) then consider g being Function such that A16: z = g and A17: dom g = dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) and A18: for d being set st d in dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) holds g . d in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . d by CARD_3:def_5; A19: dom ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; then reconsider g = g as FinSequence by A4, A17, FINSEQ_1:def_2; rng g c= REAL proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng g or b in REAL ) assume b in rng g ; ::_thesis: b in REAL then consider a being set such that A20: a in dom g and A21: g . a = b by FUNCT_1:def_3; A22: g . a in ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a by A17, A18, A20; percases ( a = q or a <> q ) ; suppose a = q ; ::_thesis: b in REAL then ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[ by A17, A19, A20, FUNCT_7:31; hence b in REAL by A21, A22; ::_thesis: verum end; suppose a <> q ; ::_thesis: b in REAL then A23: ((Carrier ((Seg n) --> R^1)) +* (q,(R^1 ].((x . q) - (1 / m)),((x . q) + (1 / m)).[))) . a = (Carrier ((Seg n) --> R^1)) . a by FUNCT_7:32; ex R being 1-sorted st ( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A20, A17, A19, PRALG_1:def_13; hence b in REAL by A21, A22, A23, A20, A17, A19, FUNCOP_1:7; ::_thesis: verum end; end; end; then g is FinSequence of REAL by FINSEQ_1:def_4; then A24: g is Element of REAL * by FINSEQ_1:def_11; n in NAT by ORDINAL1:def_12; then len g = n by A4, A17, A19, FINSEQ_1:def_3; hence z in the carrier of (TopSpaceMetr (Euclid n)) by A16, A24; ::_thesis: verum end; hence s in bool the carrier of (TopSpaceMetr (Euclid n)) by A15, ZFMISC_1:def_1; ::_thesis: verum end; then reconsider Y = { H2(q) where q is Element of S : S2[q] } as Subset-Family of (TopSpaceMetr (Euclid n)) ; A25: Y c= PP proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Y or z in PP ) assume A26: z in Y ; ::_thesis: z in PP then consider i being Element of S such that A27: z = H2(i) ; ((Seg n) --> R^1) . i = R^1 by FUNCOP_1:7; hence z in PP by A2, A5, A26, A3, A27, WAYBEL18:def_2; ::_thesis: verum end; consider N being set such that A28: N in S by XBOOLE_0:def_1; A29: H2(N) in Y by A28; then A30: Intersect Y = meet Y by SETFAM_1:def_9; A31: dom (Intervals (x,(1 / m))) = dom x by Def3; A32: now__::_thesis:_for_i_being_Element_of_S_holds_product_(Intervals_(x,(1_/_m)))_c=_product_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[))) let i be Element of S; ::_thesis: product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) set f = (Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[)); thus product (Intervals (x,(1 / m))) c= product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ::_thesis: verum proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in product (Intervals (x,(1 / m))) or d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ) assume d in product (Intervals (x,(1 / m))) ; ::_thesis: d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) then consider d1 being Function such that A33: d = d1 and A34: dom d1 = dom (Intervals (x,(1 / m))) and A35: for a being set st a in dom (Intervals (x,(1 / m))) holds d1 . a in (Intervals (x,(1 / m))) . a by CARD_3:def_5; A36: dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; now__::_thesis:_for_k_being_set_st_k_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[)))_holds_ d1_._k_in_((Carrier_((Seg_n)_-->_R^1))_+*_(i,(R^1_].((x_._i)_-_(1_/_m)),((x_._i)_+_(1_/_m)).[)))_._k let k be set ; ::_thesis: ( k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) implies d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 ) assume A37: k in dom ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 then A38: (Intervals (x,(1 / m))) . k = ].((x . k) - (1 / m)),((x . k) + (1 / m)).[ by A36, A12, Def3; A39: d1 . k in (Intervals (x,(1 / m))) . k by A35, A31, A12, A36, A37; percases ( k = i or k <> i ) ; suppose k = i ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 hence d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A38, A39, A37, A36, FUNCT_7:31; ::_thesis: verum end; suppose k <> i ; ::_thesis: d1 . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . b1 then A40: ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k = (Carrier ((Seg n) --> R^1)) . k by FUNCT_7:32; A41: ex R being 1-sorted st ( R = ((Seg n) --> R^1) . k & (Carrier ((Seg n) --> R^1)) . k = the carrier of R ) by A37, A36, PRALG_1:def_13; d1 . k in REAL by A38, A39; hence d1 . k in ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) . k by A40, A41, A37, A36, FUNCOP_1:7; ::_thesis: verum end; end; end; hence d in product ((Carrier ((Seg n) --> R^1)) +* (i,(R^1 ].((x . i) - (1 / m)),((x . i) + (1 / m)).[))) by A33, A4, A34, A31, A12, A36, CARD_3:9; ::_thesis: verum end; end; b = Intersect Y proof now__::_thesis:_for_M_being_set_st_M_in_Y_holds_ b_c=_M let M be set ; ::_thesis: ( M in Y implies b c= M ) assume M in Y ; ::_thesis: b c= M then ex i being Element of S st M = H2(i) ; hence b c= M by A13, A32; ::_thesis: verum end; hence b c= Intersect Y by A30, A29, SETFAM_1:5; :: according to XBOOLE_0:def_10 ::_thesis: Intersect Y c= b let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in Intersect Y or q in b ) assume A42: q in Intersect Y ; ::_thesis: q in b then reconsider q = q as Function ; A43: dom q = Seg n by A42, FINSEQ_1:89; now__::_thesis:_for_a_being_set_st_a_in_dom_(Intervals_(x,(1_/_m)))_holds_ q_._a_in_(Intervals_(x,(1_/_m)))_._a let a be set ; ::_thesis: ( a in dom (Intervals (x,(1 / m))) implies q . a in (Intervals (x,(1 / m))) . a ) assume A44: a in dom (Intervals (x,(1 / m))) ; ::_thesis: q . a in (Intervals (x,(1 / m))) . a A45: (Intervals (x,(1 / m))) . a = ].((x . a) - (1 / m)),((x . a) + (1 / m)).[ by A44, A31, Def3; set f = (Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[)); H2(a) in Y by A44, A31, A12; then A46: q in H2(a) by A42, SETFAM_1:43; then A47: dom q = dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) by CARD_3:9; then A48: q . a in ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) . a by A43, A44, A31, A12, A46, CARD_3:9; dom ((Carrier ((Seg n) --> R^1)) +* (a,(R^1 ].((x . a) - (1 / m)),((x . a) + (1 / m)).[))) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; hence q . a in (Intervals (x,(1 / m))) . a by A45, A48, A43, A44, A31, A12, A47, FUNCT_7:31; ::_thesis: verum end; hence q in b by A13, A43, A31, A12, CARD_3:9; ::_thesis: verum end; hence b in FinMeetCl PP by A25, A14, CANTOR_1:def_3; ::_thesis: verum 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 let n be Nat; ::_thesis: for PP being Subset-Family of (TopSpaceMetr (Euclid n)) st PP = product_prebasis ((Seg n) --> R^1) holds PP is open let PP be Subset-Family of (TopSpaceMetr (Euclid n)); ::_thesis: ( PP = product_prebasis ((Seg n) --> R^1) implies PP is open ) set J = (Seg n) --> R^1; set C = Carrier ((Seg n) --> R^1); set T = TopSpaceMetr (Euclid n); set E = Euclid n; assume A1: PP = product_prebasis ((Seg n) --> R^1) ; ::_thesis: PP is open let x be Subset of (TopSpaceMetr (Euclid n)); :: according to TOPS_2:def_1 ::_thesis: ( not x in PP or x is open ) assume x in PP ; ::_thesis: x is open then consider i being set , R being TopStruct , V being Subset of R such that A2: i in Seg n and A3: V is open and A4: R = ((Seg n) --> R^1) . i and A5: x = product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A1, WAYBEL18:def_2; A6: dom (Carrier ((Seg n) --> R^1)) = Seg n by PARTFUN1:def_2; A7: now__::_thesis:_for_i_being_set_ for_e,_y_being_Point_of_(Euclid_n) for_r_being_real_number_st_y_in_Ball_(e,r)_holds_ y_in_product_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[)) let i be set ; ::_thesis: for e, y being Point of (Euclid n) for r being real number st y in Ball (e,r) holds y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) let e, y be Point of (Euclid n); ::_thesis: for r being real number st y in Ball (e,r) holds y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) let r be real number ; ::_thesis: ( y in Ball (e,r) implies y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ) assume A8: y in Ball (e,r) ; ::_thesis: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) set O = ].((e . i) - r),((e . i) + r).[; set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[); A9: dom y = Seg n by FINSEQ_1:89; A10: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; now__::_thesis:_for_a_being_set_st_a_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_holds_ y_._a_in_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_._a let a be set ; ::_thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 ) assume A11: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 percases ( a = i or a <> i ) ; supposeA12: a = i ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 A13: ( r is Real & e . i is Real & y . i is Real & (y . i) - (e . i) is Real ) by XREAL_0:def_1; A14: y . i = (e . i) + ((y . i) - (e . i)) ; A15: dom e = Seg n by FINSEQ_1:89; dom (y - e) = (dom y) /\ (dom e) by VALUED_1:12; then A16: (y - e) . i = (y . i) - (e . i) by A9, A15, A11, A12, A10, VALUED_1:13; abs ((y - e) . i) < r by A8, Th10; then y . i in ].((e . i) - r),((e . i) + r).[ by A16, A13, A14, FCONT_3:3; hence y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A12, A10, A11, FUNCT_7:31; ::_thesis: verum end; suppose a <> i ; ::_thesis: y . b1 in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 then A17: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a by FUNCT_7:32; A18: ex R being 1-sorted st ( R = ((Seg n) --> R^1) . a & (Carrier ((Seg n) --> R^1)) . a = the carrier of R ) by A11, A10, PRALG_1:def_13; y . a in REAL by XREAL_0:def_1; hence y . a in ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a by A17, A11, A10, A18, FUNCOP_1:7; ::_thesis: verum end; end; end; hence y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A10, A6, A9, CARD_3:9; ::_thesis: verum end; set F = (Carrier ((Seg n) --> R^1)) +* (i,V); A19: R = R^1 by A2, A4, FUNCOP_1:7; for e being Element of (Euclid n) st e in x holds ex r being Real st ( r > 0 & Ball (e,r) c= x ) proof let e be Element of (Euclid n); ::_thesis: ( e in x implies ex r being Real st ( r > 0 & Ball (e,r) c= x ) ) assume A20: e in x ; ::_thesis: ex r being Real st ( r > 0 & Ball (e,r) c= x ) A21: dom ((Carrier ((Seg n) --> R^1)) +* (i,V)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; then A22: e . i in ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i by A2, A6, A20, A5, CARD_3:9; A23: ((Carrier ((Seg n) --> R^1)) +* (i,V)) . i = V by A2, A6, FUNCT_7:31; then consider r being Real such that A24: r > 0 and A25: ].((e . i) - r),((e . i) + r).[ c= V by A3, A19, A22, FRECHET:8; take r ; ::_thesis: ( r > 0 & Ball (e,r) c= x ) thus r > 0 by A24; ::_thesis: Ball (e,r) c= x let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Ball (e,r) or y in x ) assume A26: y in Ball (e,r) ; ::_thesis: y in x then reconsider y = y as Point of (Euclid n) ; set O = ].((e . i) - r),((e . i) + r).[; set G = (Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[); A27: dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) = dom (Carrier ((Seg n) --> R^1)) by FUNCT_7:30; A28: y in product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) by A26, A7; now__::_thesis:_for_a_being_set_st_a_in_dom_((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_holds_ ((Carrier_((Seg_n)_-->_R^1))_+*_(i,].((e_._i)_-_r),((e_._i)_+_r).[))_._a_c=_((Carrier_((Seg_n)_-->_R^1))_+*_(i,V))_._a let a be set ; ::_thesis: ( a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) implies ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 ) assume A29: a in dom ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 percases ( a = i or a <> i ) ; suppose a = i ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a by A25, A23, A27, A29, FUNCT_7:31; ::_thesis: verum end; suppose a <> i ; ::_thesis: ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . b1 c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . b1 then ( ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a = (Carrier ((Seg n) --> R^1)) . a & ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a = (Carrier ((Seg n) --> R^1)) . a ) by FUNCT_7:32; hence ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) . a c= ((Carrier ((Seg n) --> R^1)) +* (i,V)) . a ; ::_thesis: verum end; end; end; then product ((Carrier ((Seg n) --> R^1)) +* (i,].((e . i) - r),((e . i) + r).[)) c= product ((Carrier ((Seg n) --> R^1)) +* (i,V)) by A21, CARD_3:27, FUNCT_7:30; hence y in x by A28, A5; ::_thesis: verum end; then x in the topology of (TopSpaceMetr (Euclid n)) by PCOMPS_1:def_4; hence x is open by PRE_TOPC:def_2; ::_thesis: verum end; theorem :: EUCLID_9:28 for n being Nat holds TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) proof let n be Nat; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) set J = (Seg n) --> R^1; percases ( n = 0 or n <> 0 ) ; supposeA1: n = 0 ; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) then (Seg n) --> R^1 = {} --> R^1 ; hence TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) by A1, Lm1; ::_thesis: verum end; supposeA2: n <> 0 ; ::_thesis: TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) A3: REAL n = Funcs ((Seg n),REAL) by FINSEQ_2:93; A4: Funcs ((Seg n),REAL) = product (Carrier ((Seg n) --> R^1)) by Th25; then reconsider PP = product_prebasis ((Seg n) --> R^1) as Subset-Family of (TopSpaceMetr (Euclid n)) by FINSEQ_2:93; A5: PP is open by Th27; PP is quasi_prebasis by A2, Th26; hence TopSpaceMetr (Euclid n) = product ((Seg n) --> R^1) by A4, A3, A5, WAYBEL18:def_3; ::_thesis: verum end; end; end;