:: TOPS_4 semantic presentation begin theorem Th1: :: TOPS_4:1 for A, B, S, T being TopSpace for f being Function of A,S for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds g is open proof let A, B, S, T be TopSpace; ::_thesis: for f being Function of A,S for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds g is open let f be Function of A,S; ::_thesis: for g being Function of B,T st TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open holds g is open let g be Function of B,T; ::_thesis: ( TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) & TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) & f = g & f is open implies g is open ) assume that A1: TopStruct(# the U1 of A, the topology of A #) = TopStruct(# the U1 of B, the topology of B #) and A2: TopStruct(# the U1 of S, the topology of S #) = TopStruct(# the U1 of T, the topology of T #) and A3: f = g and A4: f is open ; ::_thesis: g is open let b be Subset of B; :: according to T_0TOPSP:def_2 ::_thesis: ( not b is open or g .: b is open ) assume A5: b is open ; ::_thesis: g .: b is open reconsider a = b as Subset of A by A1; a is open by A1, A5, TOPS_3:76; then f .: a is open by A4, T_0TOPSP:def_2; hence g .: b is open by A2, A3, TOPS_3:76; ::_thesis: verum end; theorem :: TOPS_4:2 for m being Nat for P being Subset of (TOP-REAL m) holds ( P is open iff for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P ) proof let m be Nat; ::_thesis: for P being Subset of (TOP-REAL m) holds ( P is open iff for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P ) let P be Subset of (TOP-REAL m); ::_thesis: ( P is open iff for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider P1 = P as Subset of (TopSpaceMetr (Euclid m)) ; A2: m in NAT by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P ) implies P is open ) assume A3: P is open ; ::_thesis: for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P let p be Point of (TOP-REAL m); ::_thesis: ( p in P implies ex r being real positive number st Ball (p,r) c= P ) assume A4: p in P ; ::_thesis: ex r being real positive number st Ball (p,r) c= P reconsider e = p as Point of (Euclid m) by EUCLID:67; P1 is open by A3, A1, TOPS_3:76; then consider r being real number such that A5: r > 0 and A6: Ball (e,r) c= P1 by A4, TOPMETR:15; reconsider r = r as real positive number by A5; take r = r; ::_thesis: Ball (p,r) c= P thus Ball (p,r) c= P by A2, A6, TOPREAL9:13; ::_thesis: verum end; assume A7: for p being Point of (TOP-REAL m) st p in P holds ex r being real positive number st Ball (p,r) c= P ; ::_thesis: P is open for p being Point of (Euclid m) st p in P1 holds ex r being real number st ( r > 0 & Ball (p,r) c= P1 ) proof let p be Point of (Euclid m); ::_thesis: ( p in P1 implies ex r being real number st ( r > 0 & Ball (p,r) c= P1 ) ) assume A8: p in P1 ; ::_thesis: ex r being real number st ( r > 0 & Ball (p,r) c= P1 ) reconsider e = p as Point of (TOP-REAL m) by EUCLID:67; consider r being real positive number such that A9: Ball (e,r) c= P1 by A7, A8; take r ; ::_thesis: ( r > 0 & Ball (p,r) c= P1 ) thus ( r > 0 & Ball (p,r) c= P1 ) by A2, A9, TOPREAL9:13; ::_thesis: verum end; then P1 is open by TOPMETR:15; hence P is open by A1, TOPS_3:76; ::_thesis: verum end; theorem Th3: :: TOPS_4:3 for X, Y being non empty TopSpace for f being Function of X,Y holds ( f is open iff for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) proof let X, Y be non empty TopSpace; ::_thesis: for f being Function of X,Y holds ( f is open iff for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) let f be Function of X,Y; ::_thesis: ( f is open iff for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) thus ( f is open implies for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) ::_thesis: ( ( for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) let p be Point of X; ::_thesis: for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) let V be open Subset of X; ::_thesis: ( p in V implies ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ) assume A2: p in V ; ::_thesis: ex W being open Subset of Y st ( f . p in W & W c= f .: V ) V is a_neighborhood of p by A2, CONNSP_2:3; then consider W being open a_neighborhood of f . p such that A3: W c= f .: V by A1, TOPGRP_1:22; take W ; ::_thesis: ( f . p in W & W c= f .: V ) thus f . p in W by CONNSP_2:4; ::_thesis: W c= f .: V thus W c= f .: V by A3; ::_thesis: verum end; assume A4: for p being Point of X for V being open Subset of X st p in V holds ex W being open Subset of Y st ( f . p in W & W c= f .: V ) ; ::_thesis: f is open for p being Point of X for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P proof let p be Point of X; ::_thesis: for P being open a_neighborhood of p ex R being a_neighborhood of f . p st R c= f .: P let P be open a_neighborhood of p; ::_thesis: ex R being a_neighborhood of f . p st R c= f .: P consider W being open Subset of Y such that A5: f . p in W and A6: W c= f .: P by A4, CONNSP_2:4; W is a_neighborhood of f . p by A5, CONNSP_2:3; hence ex R being a_neighborhood of f . p st R c= f .: P by A6; ::_thesis: verum end; hence f is open by TOPGRP_1:23; ::_thesis: verum end; theorem Th4: :: TOPS_4:4 for T being non empty TopSpace for M being non empty MetrSpace for f being Function of T,(TopSpaceMetr M) holds ( f is open iff for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) proof let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace for f being Function of T,(TopSpaceMetr M) holds ( f is open iff for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) let M be non empty MetrSpace; ::_thesis: for f being Function of T,(TopSpaceMetr M) holds ( f is open iff for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) let f be Function of T,(TopSpaceMetr M); ::_thesis: ( f is open iff for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) thus ( f is open implies for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) ::_thesis: ( ( for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let p be Point of T; ::_thesis: for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let V be open Subset of T; ::_thesis: for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let q be Point of M; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V ) assume A2: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V ) assume p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V then consider W being open Subset of (TopSpaceMetr M) such that A3: f . p in W and A4: W c= f .: V by A1, Th3; ex r being real number st ( r > 0 & Ball (q,r) c= W ) by A2, A3, TOPMETR:15; hence ex r being real positive number st Ball (q,r) c= f .: V by A4, XBOOLE_1:1; ::_thesis: verum end; assume A5: for p being Point of T for V being open Subset of T for q being Point of M st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V ; ::_thesis: f is open for p being Point of T for V being open Subset of T st p in V holds ex W being open Subset of (TopSpaceMetr M) st ( f . p in W & W c= f .: V ) proof let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds ex W being open Subset of (TopSpaceMetr M) st ( f . p in W & W c= f .: V ) let V be open Subset of T; ::_thesis: ( p in V implies ex W being open Subset of (TopSpaceMetr M) st ( f . p in W & W c= f .: V ) ) reconsider q = f . p as Point of M ; assume p in V ; ::_thesis: ex W being open Subset of (TopSpaceMetr M) st ( f . p in W & W c= f .: V ) then consider r being real positive number such that A6: Ball (q,r) c= f .: V by A5; reconsider W = Ball (q,r) as open Subset of (TopSpaceMetr M) by TOPMETR:14; take W ; ::_thesis: ( f . p in W & W c= f .: V ) thus f . p in W by GOBOARD6:1; ::_thesis: W c= f .: V thus W c= f .: V by A6; ::_thesis: verum end; hence f is open by Th3; ::_thesis: verum end; theorem Th5: :: TOPS_4:5 for T being non empty TopSpace for M being non empty MetrSpace for f being Function of (TopSpaceMetr M),T holds ( f is open iff for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) proof let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace for f being Function of (TopSpaceMetr M),T holds ( f is open iff for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) let M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M),T holds ( f is open iff for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) let f be Function of (TopSpaceMetr M),T; ::_thesis: ( f is open iff for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) hereby ::_thesis: ( ( for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open ) assume A1: f is open ; ::_thesis: for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) let p be Point of M; ::_thesis: for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) A2: p in Ball (p,r) by GOBOARD6:1; reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M) ; V is open by TOPMETR:14; then consider W being open Subset of T such that A3: ( f . p in W & W c= f .: V ) by A1, A2, Th3; take W = W; ::_thesis: ( f . p in W & W c= f .: (Ball (p,r)) ) thus ( f . p in W & W c= f .: (Ball (p,r)) ) by A3; ::_thesis: verum end; assume A4: for p being Point of M for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ; ::_thesis: f is open for p being Point of (TopSpaceMetr M) for V being open Subset of (TopSpaceMetr M) st p in V holds ex W being open Subset of T st ( f . p in W & W c= f .: V ) proof let p be Point of (TopSpaceMetr M); ::_thesis: for V being open Subset of (TopSpaceMetr M) st p in V holds ex W being open Subset of T st ( f . p in W & W c= f .: V ) let V be open Subset of (TopSpaceMetr M); ::_thesis: ( p in V implies ex W being open Subset of T st ( f . p in W & W c= f .: V ) ) reconsider q = p as Point of M ; assume p in V ; ::_thesis: ex W being open Subset of T st ( f . p in W & W c= f .: V ) then consider r being real number such that A5: r > 0 and A6: Ball (q,r) c= V by TOPMETR:15; consider W being open Subset of T such that A7: f . p in W and A8: W c= f .: (Ball (q,r)) by A4, A5; take W ; ::_thesis: ( f . p in W & W c= f .: V ) thus f . p in W by A7; ::_thesis: W c= f .: V f .: (Ball (q,r)) c= f .: V by A6, RELAT_1:123; hence W c= f .: V by A8, XBOOLE_1:1; ::_thesis: verum end; hence f is open by Th3; ::_thesis: verum end; theorem Th6: :: TOPS_4:6 for M1, M2 being non empty MetrSpace for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds ( f is open iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) proof let M1, M2 be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds ( f is open iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); ::_thesis: ( f is open iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) thus ( f is open implies for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) ::_thesis: ( ( for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) let p be Point of M1; ::_thesis: for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) let q be Point of M2; ::_thesis: for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) assume A2: q = f . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) reconsider V = Ball (p,r) as Subset of (TopSpaceMetr M1) ; A3: p in V by GOBOARD6:1; V is open by TOPMETR:14; hence ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) by A1, A2, A3, Th4; ::_thesis: verum end; assume A4: for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ; ::_thesis: f is open for p being Point of (TopSpaceMetr M1) for V being open Subset of (TopSpaceMetr M1) for q being Point of M2 st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V proof let p be Point of (TopSpaceMetr M1); ::_thesis: for V being open Subset of (TopSpaceMetr M1) for q being Point of M2 st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let V be open Subset of (TopSpaceMetr M1); ::_thesis: for q being Point of M2 st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let q be Point of M2; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V ) assume A5: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V ) reconsider p1 = p as Point of M1 ; assume p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V then consider r being real number such that A6: r > 0 and A7: Ball (p1,r) c= V by TOPMETR:15; A8: f .: (Ball (p1,r)) c= f .: V by A7, RELAT_1:123; ex s being real positive number st Ball (q,s) c= f .: (Ball (p1,r)) by A4, A5, A6; hence ex r being real positive number st Ball (q,r) c= f .: V by A8, XBOOLE_1:1; ::_thesis: verum end; hence f is open by Th4; ::_thesis: verum end; theorem :: TOPS_4:7 for m being Nat for T being non empty TopSpace for f being Function of T,(TOP-REAL m) holds ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) proof let m be Nat; ::_thesis: for T being non empty TopSpace for f being Function of T,(TOP-REAL m) holds ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL m) holds ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) let f be Function of T,(TOP-REAL m); ::_thesis: ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider f1 = f as Function of T,(TopSpaceMetr (Euclid m)) ; A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ; A3: m in NAT by ORDINAL1:def_12; thus ( f is open implies for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) ::_thesis: ( ( for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ) implies f is open ) proof assume A4: f is open ; ::_thesis: for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V let V be open Subset of T; ::_thesis: ( p in V implies ex r being real positive number st Ball ((f . p),r) c= f .: V ) assume A5: p in V ; ::_thesis: ex r being real positive number st Ball ((f . p),r) c= f .: V reconsider fp = f . p as Point of (Euclid m) by EUCLID:67; f1 is open by A4, A1, A2, Th1; then consider r being real positive number such that A6: Ball (fp,r) c= f1 .: V by A5, Th4; Ball ((f . p),r) = Ball (fp,r) by A3, TOPREAL9:13; hence ex r being real positive number st Ball ((f . p),r) c= f .: V by A6; ::_thesis: verum end; assume A7: for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st Ball ((f . p),r) c= f .: V ; ::_thesis: f is open for p being Point of T for V being open Subset of T for q being Point of (Euclid m) st q = f1 . p & p in V holds ex r being real positive number st Ball (q,r) c= f1 .: V proof let p be Point of T; ::_thesis: for V being open Subset of T for q being Point of (Euclid m) st q = f1 . p & p in V holds ex r being real positive number st Ball (q,r) c= f1 .: V let V be open Subset of T; ::_thesis: for q being Point of (Euclid m) st q = f1 . p & p in V holds ex r being real positive number st Ball (q,r) c= f1 .: V let q be Point of (Euclid m); ::_thesis: ( q = f1 . p & p in V implies ex r being real positive number st Ball (q,r) c= f1 .: V ) assume A8: q = f1 . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f1 .: V ) assume p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f1 .: V then consider r being real positive number such that A9: Ball ((f . p),r) c= f .: V by A7; Ball ((f . p),r) = Ball (q,r) by A3, A8, TOPREAL9:13; hence ex r being real positive number st Ball (q,r) c= f1 .: V by A9; ::_thesis: verum end; then f1 is open by Th4; hence f is open by A1, A2, Th1; ::_thesis: verum end; theorem :: TOPS_4:8 for m being Nat for T being non empty TopSpace for f being Function of (TOP-REAL m),T holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) proof let m be Nat; ::_thesis: for T being non empty TopSpace for f being Function of (TOP-REAL m),T holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) let T be non empty TopSpace; ::_thesis: for f being Function of (TOP-REAL m),T holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) let f be Function of (TOP-REAL m),T; ::_thesis: ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),T ; A2: TopStruct(# the U1 of T, the topology of T #) = TopStruct(# the U1 of T, the topology of T #) ; A3: m in NAT by ORDINAL1:def_12; thus ( f is open implies for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) ::_thesis: ( ( for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ) implies f is open ) proof assume A4: f is open ; ::_thesis: for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) reconsider q = p as Point of (Euclid m) by EUCLID:67; f1 is open by A4, A1, A2, Th1; then consider W being open Subset of T such that A5: ( f1 . p in W & W c= f1 .: (Ball (q,r)) ) by Th5; Ball (p,r) = Ball (q,r) by A3, TOPREAL9:13; hence ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) by A5; ::_thesis: verum end; assume A6: for p being Point of (TOP-REAL m) for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) ; ::_thesis: f is open for p being Point of (Euclid m) for r being real positive number ex W being open Subset of T st ( f1 . p in W & W c= f1 .: (Ball (p,r)) ) proof let p be Point of (Euclid m); ::_thesis: for r being real positive number ex W being open Subset of T st ( f1 . p in W & W c= f1 .: (Ball (p,r)) ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( f1 . p in W & W c= f1 .: (Ball (p,r)) ) reconsider q = p as Point of (TOP-REAL m) by EUCLID:67; consider W being open Subset of T such that A7: ( f . q in W & W c= f .: (Ball (q,r)) ) by A6; Ball (p,r) = Ball (q,r) by A3, TOPREAL9:13; hence ex W being open Subset of T st ( f1 . p in W & W c= f1 .: (Ball (p,r)) ) by A7; ::_thesis: verum end; then f1 is open by Th5; hence f is open by A1, A2, Th1; ::_thesis: verum end; theorem :: TOPS_4:9 for m, n being Nat for f being Function of (TOP-REAL m),(TOP-REAL n) holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) proof let m, n be Nat; ::_thesis: for f being Function of (TOP-REAL m),(TOP-REAL n) holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) let f be Function of (TOP-REAL m),(TOP-REAL n); ::_thesis: ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def_8; then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ; A2: ( m in NAT & n in NAT ) by ORDINAL1:def_12; thus ( f is open implies for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) ::_thesis: ( ( for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ) implies f is open ) proof assume A3: f is open ; ::_thesis: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) let r be real positive number ; ::_thesis: ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) reconsider p1 = p as Point of (Euclid m) by EUCLID:67; reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67; f1 is open by A1, A3, Th1; then consider s being real positive number such that A4: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6; ( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball ((f . p),s) ) by A2, TOPREAL9:13; hence ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) by A4; ::_thesis: verum end; assume A5: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: (Ball (p,r)) ; ::_thesis: f is open for p being Point of (Euclid m) for q being Point of (Euclid n) for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) proof let p be Point of (Euclid m); ::_thesis: for q being Point of (Euclid n) for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) let q be Point of (Euclid n); ::_thesis: for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) ) assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67; reconsider q1 = q as Point of (TOP-REAL n) by EUCLID:67; consider s being real positive number such that A7: Ball (q1,s) c= f .: (Ball (p1,r)) by A5, A6; ( Ball (p1,r) = Ball (p,r) & Ball (q1,s) = Ball (q,s) ) by A2, TOPREAL9:13; hence ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) by A7; ::_thesis: verum end; then f1 is open by Th6; hence f is open by A1, Th1; ::_thesis: verum end; theorem :: TOPS_4:10 for T being non empty TopSpace for f being Function of T,R^1 holds ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 holds ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) let f be Function of T,R^1; ::_thesis: ( f is open iff for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) thus ( f is open implies for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) ::_thesis: ( ( for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V let p be Point of T; ::_thesis: for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V let V be open Subset of T; ::_thesis: ( p in V implies ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ) assume A2: p in V ; ::_thesis: ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V reconsider fp = f . p as Point of RealSpace ; consider r being real positive number such that A3: Ball (fp,r) c= f .: V by A1, A2, Th4; r in REAL by XREAL_0:def_1; then ].(fp - r),(fp + r).[ = Ball (fp,r) by FRECHET:7; hence ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V by A3; ::_thesis: verum end; assume A4: for p being Point of T for V being open Subset of T st p in V holds ex r being real positive number st ].((f . p) - r),((f . p) + r).[ c= f .: V ; ::_thesis: f is open for p being Point of T for V being open Subset of T for q being Point of RealSpace st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V proof let p be Point of T; ::_thesis: for V being open Subset of T for q being Point of RealSpace st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let V be open Subset of T; ::_thesis: for q being Point of RealSpace st q = f . p & p in V holds ex r being real positive number st Ball (q,r) c= f .: V let q be Point of RealSpace; ::_thesis: ( q = f . p & p in V implies ex r being real positive number st Ball (q,r) c= f .: V ) assume A5: q = f . p ; ::_thesis: ( not p in V or ex r being real positive number st Ball (q,r) c= f .: V ) assume p in V ; ::_thesis: ex r being real positive number st Ball (q,r) c= f .: V then consider r being real positive number such that A6: ].((f . p) - r),((f . p) + r).[ c= f .: V by A4; r in REAL by XREAL_0:def_1; then ].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7; hence ex r being real positive number st Ball (q,r) c= f .: V by A5, A6; ::_thesis: verum end; hence f is open by Th4; ::_thesis: verum end; theorem :: TOPS_4:11 for T being non empty TopSpace for f being Function of R^1,T holds ( f is open iff for p being Point of R^1 for r being real positive number ex V being open Subset of T st ( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of R^1,T holds ( f is open iff for p being Point of R^1 for r being real positive number ex V being open Subset of T st ( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) let f be Function of R^1,T; ::_thesis: ( f is open iff for p being Point of R^1 for r being real positive number ex V being open Subset of T st ( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) thus ( f is open implies for p being Point of R^1 for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ) ::_thesis: ( ( for p being Point of R^1 for r being real positive number ex V being open Subset of T st ( f . p in V & V c= f .: ].(p - r),(p + r).[ ) ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of R^1 for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) let p be Point of R^1; ::_thesis: for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) reconsider q = p as Point of RealSpace ; consider W being open Subset of T such that A2: ( f . p in W & W c= f .: (Ball (q,r)) ) by A1, Th5; r in REAL by XREAL_0:def_1; then ].(q - r),(q + r).[ = Ball (q,r) by FRECHET:7; hence ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) by A2; ::_thesis: verum end; assume A3: for p being Point of R^1 for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: ].(p - r),(p + r).[ ) ; ::_thesis: f is open for p being Point of RealSpace for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) proof let p be Point of RealSpace; ::_thesis: for r being real positive number ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) reconsider q = p as Point of R^1 ; consider W being open Subset of T such that A4: ( f . q in W & W c= f .: ].(p - r),(p + r).[ ) by A3; r in REAL by XREAL_0:def_1; then ].(p - r),(p + r).[ = Ball (p,r) by FRECHET:7; hence ex W being open Subset of T st ( f . p in W & W c= f .: (Ball (p,r)) ) by A4; ::_thesis: verum end; hence f is open by Th5; ::_thesis: verum end; theorem :: TOPS_4:12 for f being Function of R^1,R^1 holds ( f is open iff for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) proof let f be Function of R^1,R^1; ::_thesis: ( f is open iff for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) thus ( f is open implies for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) ::_thesis: ( ( for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ) implies f is open ) proof assume A1: f is open ; ::_thesis: for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ let r be real positive number ; ::_thesis: ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ reconsider p1 = p, q1 = f . p as Point of RealSpace ; consider s being real positive number such that A2: Ball (q1,s) c= f .: (Ball (p1,r)) by A1, Th6; ( r in REAL & s in REAL ) by XREAL_0:def_1; then ( ].(p - r),(p + r).[ = Ball (p1,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q1,s) ) by FRECHET:7; hence ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A2; ::_thesis: verum end; assume A3: for p being Point of R^1 for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ ; ::_thesis: f is open for p, q being Point of RealSpace for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) proof let p, q be Point of RealSpace; ::_thesis: for r being real positive number st q = f . p holds ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) ) assume A4: q = f . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) consider s being real positive number such that A5: ].((f . p) - s),((f . p) + s).[ c= f .: ].(p - r),(p + r).[ by A3; ( r in REAL & s in REAL ) by XREAL_0:def_1; then ( ].(p - r),(p + r).[ = Ball (p,r) & ].((f . p) - s),((f . p) + s).[ = Ball (q,s) ) by A4, FRECHET:7; hence ex s being real positive number st Ball (q,s) c= f .: (Ball (p,r)) by A5; ::_thesis: verum end; hence f is open by Th6; ::_thesis: verum end; theorem :: TOPS_4:13 for m being Nat for f being Function of (TOP-REAL m),R^1 holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) proof let m be Nat; ::_thesis: for f being Function of (TOP-REAL m),R^1 holds ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) let f be Function of (TOP-REAL m),R^1; ::_thesis: ( f is open iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) A1: m in NAT by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ) implies f is open ) assume A2: f is open ; ::_thesis: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) let r be real positive number ; ::_thesis: ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) p in Ball (p,r) by A1, TOPGEN_5:13; then A3: f . p in f .: (Ball (p,r)) by FUNCT_2:35; f .: (Ball (p,r)) is open by A2, T_0TOPSP:def_2; then consider s being Element of REAL such that A4: s > 0 and A5: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A3, FRECHET:8; reconsider s = s as real positive number by A4; take s = s; ::_thesis: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) thus ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) by A5; ::_thesis: verum end; assume A6: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,r)) ; ::_thesis: f is open let A be Subset of (TOP-REAL m); :: according to T_0TOPSP:def_2 ::_thesis: ( not A is open or f .: A is open ) assume A7: A is open ; ::_thesis: f .: A is open for x being set holds ( x in f .: A iff ex Q being Subset of R^1 st ( Q is open & Q c= f .: A & x in Q ) ) proof let x be set ; ::_thesis: ( x in f .: A iff ex Q being Subset of R^1 st ( Q is open & Q c= f .: A & x in Q ) ) hereby ::_thesis: ( ex Q being Subset of R^1 st ( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) assume x in f .: A ; ::_thesis: ex Q being Element of K6( the U1 of K414()) st ( Q is open & Q c= f .: A & x in Q ) then consider p being Point of (TOP-REAL m) such that A8: p in A and A9: x = f . p by FUNCT_2:65; reconsider u = p as Point of (Euclid m) by EUCLID:67; A = Int A by A7, TOPS_1:23; then consider e being real number such that A10: e > 0 and A11: Ball (u,e) c= A by A8, GOBOARD6:5; A12: Ball (u,e) = Ball (p,e) by A1, TOPREAL9:13; consider s being real positive number such that A13: ].((f . p) - s),((f . p) + s).[ c= f .: (Ball (p,e)) by A6, A10; take Q = R^1 ].((f . p) - s),((f . p) + s).[; ::_thesis: ( Q is open & Q c= f .: A & x in Q ) thus Q is open ; ::_thesis: ( Q c= f .: A & x in Q ) f .: (Ball (p,e)) c= f .: A by A11, A12, RELAT_1:123; hence Q c= f .: A by A13, XBOOLE_1:1; ::_thesis: x in Q thus x in Q by A9, TOPREAL6:15; ::_thesis: verum end; thus ( ex Q being Subset of R^1 st ( Q is open & Q c= f .: A & x in Q ) implies x in f .: A ) ; ::_thesis: verum end; hence f .: A is open by TOPS_1:25; ::_thesis: verum end; theorem :: TOPS_4:14 for m being Nat for f being Function of R^1,(TOP-REAL m) holds ( f is open iff for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) proof let m be Nat; ::_thesis: for f being Function of R^1,(TOP-REAL m) holds ( f is open iff for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) let f be Function of R^1,(TOP-REAL m); ::_thesis: ( f is open iff for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider f1 = f as Function of R^1,(TopSpaceMetr (Euclid m)) ; A2: m in NAT by ORDINAL1:def_12; thus ( f is open implies for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) ::_thesis: ( ( for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ) implies f is open ) proof assume A3: f is open ; ::_thesis: for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ let r be real positive number ; ::_thesis: ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ reconsider p1 = p as Point of RealSpace ; reconsider q1 = f . p as Point of (Euclid m) by EUCLID:67; f1 is open by A1, A3, Th1; then consider s being real positive number such that A4: Ball (q1,s) c= f1 .: (Ball (p1,r)) by Th6; r in REAL by XREAL_0:def_1; then ( ].(p - r),(p + r).[ = Ball (p1,r) & Ball ((f . p),s) = Ball (q1,s) ) by A2, FRECHET:7, TOPREAL9:13; hence ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ by A4; ::_thesis: verum end; assume A5: for p being Point of R^1 for r being real positive number ex s being real positive number st Ball ((f . p),s) c= f .: ].(p - r),(p + r).[ ; ::_thesis: f is open for p being Point of RealSpace for q being Point of (Euclid m) for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) proof let p be Point of RealSpace; ::_thesis: for q being Point of (Euclid m) for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) let q be Point of (Euclid m); ::_thesis: for r being real positive number st q = f1 . p holds ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) ) assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) reconsider p1 = p as Point of R^1 ; consider s being real positive number such that A7: Ball ((f . p1),s) c= f .: ].(p1 - r),(p1 + r).[ by A5; ( r in REAL & s in REAL ) by XREAL_0:def_1; then ( ].(p1 - r),(p1 + r).[ = Ball (p,r) & Ball ((f . p1),s) = Ball (q,s) ) by A2, A6, FRECHET:7, TOPREAL9:13; hence ex s being real positive number st Ball (q,s) c= f1 .: (Ball (p,r)) by A7; ::_thesis: verum end; then f1 is open by Th6; hence f is open by A1, Th1; ::_thesis: verum end; begin theorem :: TOPS_4:15 for T being non empty TopSpace for M being non empty MetrSpace for f being Function of T,(TopSpaceMetr M) holds ( f is continuous iff for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) proof let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace for f being Function of T,(TopSpaceMetr M) holds ( f is continuous iff for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) let M be non empty MetrSpace; ::_thesis: for f being Function of T,(TopSpaceMetr M) holds ( f is continuous iff for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) let f be Function of T,(TopSpaceMetr M); ::_thesis: ( f is continuous iff for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) thus ( f is continuous implies for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) ::_thesis: ( ( for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) implies f is continuous ) proof assume A1: f is continuous ; ::_thesis: for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) let p be Point of T; ::_thesis: for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) let q be Point of M; ::_thesis: for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) let r be real positive number ; ::_thesis: ( q = f . p implies ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ) assume A2: f . p = q ; ::_thesis: ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) reconsider V = Ball (q,r) as Subset of (TopSpaceMetr M) ; A3: q in Ball (q,r) by GOBOARD6:1; V is open by TOPMETR:14; then ex W being Subset of T st ( p in W & W is open & f .: W c= V ) by A1, A2, A3, JGRAPH_2:10; hence ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ; ::_thesis: verum end; assume A4: for p being Point of T for q being Point of M for r being real positive number st q = f . p holds ex W being open Subset of T st ( p in W & f .: W c= Ball (q,r) ) ; ::_thesis: f is continuous for p being Point of T for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) proof let p be Point of T; ::_thesis: for V being Subset of (TopSpaceMetr M) st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) let V be Subset of (TopSpaceMetr M); ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) assume A5: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) reconsider u = f . p as Point of M ; assume V is open ; ::_thesis: ex W being Subset of T st ( p in W & W is open & f .: W c= V ) then Int V = V by TOPS_1:23; then consider e being real number such that A6: ( e > 0 & Ball (u,e) c= V ) by A5, GOBOARD6:4; ex W being open Subset of T st ( p in W & f .: W c= Ball (u,e) ) by A4, A6; hence ex W being Subset of T st ( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPS_4:16 for T being non empty TopSpace for M being non empty MetrSpace for f being Function of (TopSpaceMetr M),T holds ( f is continuous iff for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) proof let T be non empty TopSpace; ::_thesis: for M being non empty MetrSpace for f being Function of (TopSpaceMetr M),T holds ( f is continuous iff for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) let M be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M),T holds ( f is continuous iff for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) let f be Function of (TopSpaceMetr M),T; ::_thesis: ( f is continuous iff for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) hereby ::_thesis: ( ( for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V let p be Point of M; ::_thesis: for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: (Ball (p,s)) c= V ) assume f . p in V ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= V then consider W being Subset of (TopSpaceMetr M) such that A2: p in W and A3: W is open and A4: f .: W c= V by A1, JGRAPH_2:10; Int W = W by A3, TOPS_1:23; then consider s being real number such that A5: s > 0 and A6: Ball (p,s) c= W by A2, GOBOARD6:4; reconsider s = s as real positive number by A5; take s = s; ::_thesis: f .: (Ball (p,s)) c= V f .: (Ball (p,s)) c= f .: W by A6, RELAT_1:123; hence f .: (Ball (p,s)) c= V by A4, XBOOLE_1:1; ::_thesis: verum end; assume A7: for p being Point of M for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ; ::_thesis: f is continuous for p being Point of (TopSpaceMetr M) for V being Subset of T st f . p in V & V is open holds ex W being Subset of (TopSpaceMetr M) st ( p in W & W is open & f .: W c= V ) proof let p be Point of (TopSpaceMetr M); ::_thesis: for V being Subset of T st f . p in V & V is open holds ex W being Subset of (TopSpaceMetr M) st ( p in W & W is open & f .: W c= V ) let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of (TopSpaceMetr M) st ( p in W & W is open & f .: W c= V ) ) assume that A8: f . p in V and A9: V is open ; ::_thesis: ex W being Subset of (TopSpaceMetr M) st ( p in W & W is open & f .: W c= V ) reconsider u = p as Point of M ; consider s being real positive number such that A10: f .: (Ball (u,s)) c= V by A7, A8, A9; reconsider W = Ball (u,s) as Subset of (TopSpaceMetr M) ; take W ; ::_thesis: ( p in W & W is open & f .: W c= V ) thus p in W by GOBOARD6:1; ::_thesis: ( W is open & f .: W c= V ) thus W is open by TOPMETR:14; ::_thesis: f .: W c= V thus f .: W c= V by A10; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem Th17: :: TOPS_4:17 for M1, M2 being non empty MetrSpace for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds ( f is continuous iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) proof let M1, M2 be non empty MetrSpace; ::_thesis: for f being Function of (TopSpaceMetr M1),(TopSpaceMetr M2) holds ( f is continuous iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) let f be Function of (TopSpaceMetr M1),(TopSpaceMetr M2); ::_thesis: ( f is continuous iff for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) hereby ::_thesis: ( ( for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let p be Point of M1; ::_thesis: for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let q be Point of M2; ::_thesis: for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) assume A2: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) r in REAL by XREAL_0:def_1; then consider s being Element of REAL such that A3: s > 0 and A4: for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (p,w) < s holds dist (q,w1) < r by A1, A2, UNIFORM1:4; reconsider s = s as real positive number by A3; take s = s; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r) thus f .: (Ball (p,s)) c= Ball (q,r) ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in f .: (Ball (p,s)) or y in Ball (q,r) ) assume y in f .: (Ball (p,s)) ; ::_thesis: y in Ball (q,r) then consider x being Point of (TopSpaceMetr M1) such that A5: x in Ball (p,s) and A6: f . x = y by FUNCT_2:65; reconsider x1 = x as Point of M1 ; reconsider y1 = y as Point of M2 by A6; dist (p,x1) < s by A5, METRIC_1:11; then dist (q,y1) < r by A6, A4; hence y in Ball (q,r) by METRIC_1:11; ::_thesis: verum end; end; assume A7: for p being Point of M1 for q being Point of M2 for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ; ::_thesis: f is continuous for r being real number for u being Element of M1 for u1 being Element of M2 st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) proof let r be real number ; ::_thesis: for u being Element of M1 for u1 being Element of M2 st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u be Element of M1; ::_thesis: for u1 being Element of M2 st r > 0 & u1 = f . u holds ex s being real number st ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) let u1 be Element of M2; ::_thesis: ( r > 0 & u1 = f . u implies ex s being real number st ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) ) assume ( r > 0 & u1 = f . u ) ; ::_thesis: ex s being real number st ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) then consider s being real positive number such that A8: f .: (Ball (u,s)) c= Ball (u1,r) by A7; take s ; ::_thesis: ( s > 0 & ( for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r ) ) thus s > 0 ; ::_thesis: for w being Element of M1 for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r let w be Element of M1; ::_thesis: for w1 being Element of M2 st w1 = f . w & dist (u,w) < s holds dist (u1,w1) < r let w1 be Element of M2; ::_thesis: ( w1 = f . w & dist (u,w) < s implies dist (u1,w1) < r ) assume A9: w1 = f . w ; ::_thesis: ( not dist (u,w) < s or dist (u1,w1) < r ) assume dist (u,w) < s ; ::_thesis: dist (u1,w1) < r then w in Ball (u,s) by METRIC_1:11; then f . w in f .: (Ball (u,s)) by FUNCT_2:35; hence dist (u1,w1) < r by A8, A9, METRIC_1:11; ::_thesis: verum end; hence f is continuous by UNIFORM1:3; ::_thesis: verum end; theorem :: TOPS_4:18 for m being Nat for T being non empty TopSpace for f being Function of T,(TOP-REAL m) holds ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) proof let m be Nat; ::_thesis: for T being non empty TopSpace for f being Function of T,(TOP-REAL m) holds ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) let T be non empty TopSpace; ::_thesis: for f being Function of T,(TOP-REAL m) holds ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) let f be Function of T,(TOP-REAL m); ::_thesis: ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) A1: m in NAT by ORDINAL1:def_12; thus ( f is continuous implies for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) ::_thesis: ( ( for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ) implies f is continuous ) proof assume A2: f is continuous ; ::_thesis: for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) let p be Point of T; ::_thesis: for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) f . p in Ball ((f . p),r) by A1, TOPGEN_5:13; then ex W being Subset of T st ( p in W & W is open & f .: W c= Ball ((f . p),r) ) by A2, JGRAPH_2:10; hence ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ; ::_thesis: verum end; assume A3: for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),r) ) ; ::_thesis: f is continuous for p being Point of T for V being Subset of (TOP-REAL m) st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) proof let p be Point of T; ::_thesis: for V being Subset of (TOP-REAL m) st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) let V be Subset of (TOP-REAL m); ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) assume A4: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) reconsider u = f . p as Point of (Euclid m) by EUCLID:67; assume V is open ; ::_thesis: ex W being Subset of T st ( p in W & W is open & f .: W c= V ) then Int V = V by TOPS_1:23; then consider e being real number such that A5: e > 0 and A6: Ball (u,e) c= V by A4, GOBOARD6:5; A7: Ball (u,e) = Ball ((f . p),e) by A1, TOPREAL9:13; ex W being open Subset of T st ( p in W & f .: W c= Ball ((f . p),e) ) by A3, A5; hence ex W being Subset of T st ( p in W & W is open & f .: W c= V ) by A6, A7, XBOOLE_1:1; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPS_4:19 for m being Nat for T being non empty TopSpace for f being Function of (TOP-REAL m),T holds ( f is continuous iff for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) proof let m be Nat; ::_thesis: for T being non empty TopSpace for f being Function of (TOP-REAL m),T holds ( f is continuous iff for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) let T be non empty TopSpace; ::_thesis: for f being Function of (TOP-REAL m),T holds ( f is continuous iff for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) let f be Function of (TOP-REAL m),T; ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) A1: m in NAT by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ) implies f is continuous ) assume A2: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V let p be Point of (TOP-REAL m); ::_thesis: for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: (Ball (p,s)) c= V ) assume f . p in V ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= V then consider W being Subset of (TOP-REAL m) such that A3: p in W and A4: W is open and A5: f .: W c= V by A2, JGRAPH_2:10; reconsider u = p as Point of (Euclid m) by EUCLID:67; Int W = W by A4, TOPS_1:23; then consider s being real number such that A6: s > 0 and A7: Ball (u,s) c= W by A3, GOBOARD6:5; reconsider s = s as real positive number by A6; take s = s; ::_thesis: f .: (Ball (p,s)) c= V Ball (u,s) = Ball (p,s) by A1, TOPREAL9:13; then f .: (Ball (p,s)) c= f .: W by A7, RELAT_1:123; hence f .: (Ball (p,s)) c= V by A5, XBOOLE_1:1; ::_thesis: verum end; assume A8: for p being Point of (TOP-REAL m) for V being open Subset of T st f . p in V holds ex s being real positive number st f .: (Ball (p,s)) c= V ; ::_thesis: f is continuous for p being Point of (TOP-REAL m) for V being Subset of T st f . p in V & V is open holds ex W being Subset of (TOP-REAL m) st ( p in W & W is open & f .: W c= V ) proof let p be Point of (TOP-REAL m); ::_thesis: for V being Subset of T st f . p in V & V is open holds ex W being Subset of (TOP-REAL m) st ( p in W & W is open & f .: W c= V ) let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of (TOP-REAL m) st ( p in W & W is open & f .: W c= V ) ) assume that A9: f . p in V and A10: V is open ; ::_thesis: ex W being Subset of (TOP-REAL m) st ( p in W & W is open & f .: W c= V ) consider s being real positive number such that A11: f .: (Ball (p,s)) c= V by A8, A9, A10; take W = Ball (p,s); ::_thesis: ( p in W & W is open & f .: W c= V ) thus p in W by A1, TOPGEN_5:13; ::_thesis: ( W is open & f .: W c= V ) thus W is open ; ::_thesis: f .: W c= V thus f .: W c= V by A11; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPS_4:20 for m, n being Nat for f being Function of (TOP-REAL m),(TOP-REAL n) holds ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ) proof let m, n be Nat; ::_thesis: for f being Function of (TOP-REAL m),(TOP-REAL n) holds ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ) let f be Function of (TOP-REAL m),(TOP-REAL n); ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ) A1: ( TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) & TopStruct(# the U1 of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) ) by EUCLID:def_8; then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),(TopSpaceMetr (Euclid n)) ; A2: ( m in NAT & n in NAT ) by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ) implies f is continuous ) assume A3: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) let r be real positive number ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) reconsider p1 = p as Point of (Euclid m) by EUCLID:67; reconsider q1 = f . p as Point of (Euclid n) by EUCLID:67; f1 is continuous by A1, A3, YELLOW12:36; then consider s being real positive number such that A4: f1 .: (Ball (p1,s)) c= Ball (q1,r) by Th17; take s = s; ::_thesis: f .: (Ball (p,s)) c= Ball ((f . p),r) ( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = Ball ((f . p),r) ) by A2, TOPREAL9:13; hence f .: (Ball (p,s)) c= Ball ((f . p),r) by A4; ::_thesis: verum end; assume A5: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= Ball ((f . p),r) ; ::_thesis: f is continuous for p being Point of (Euclid m) for q being Point of (Euclid n) for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) proof let p be Point of (Euclid m); ::_thesis: for q being Point of (Euclid n) for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) let q be Point of (Euclid n); ::_thesis: for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) ) assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67; consider s being real positive number such that A7: f .: (Ball (p1,s)) c= Ball ((f . p1),r) by A5; take s ; ::_thesis: f1 .: (Ball (p,s)) c= Ball (q,r) ( Ball (p1,s) = Ball (p,s) & Ball ((f . p1),r) = Ball (q,r) ) by A2, A6, TOPREAL9:13; hence f1 .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum end; then f1 is continuous by Th17; hence f is continuous by A1, YELLOW12:36; ::_thesis: verum end; theorem :: TOPS_4:21 for T being non empty TopSpace for f being Function of T,R^1 holds ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) proof let T be non empty TopSpace; ::_thesis: for f being Function of T,R^1 holds ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) let f be Function of T,R^1; ::_thesis: ( f is continuous iff for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) thus ( f is continuous implies for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) ::_thesis: ( ( for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ) implies f is continuous ) proof assume A1: f is continuous ; ::_thesis: for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) let p be Point of T; ::_thesis: for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) let r be real positive number ; ::_thesis: ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) A2: f . p in ].((f . p) - r),((f . p) + r).[ by TOPREAL6:15; R^1 ].((f . p) - r),((f . p) + r).[ is open ; then ex W being Subset of T st ( p in W & W is open & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A1, A2, JGRAPH_2:10; hence ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; ::_thesis: verum end; assume A3: for p being Point of T for r being real positive number ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) ; ::_thesis: f is continuous for p being Point of T for V being Subset of R^1 st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) proof let p be Point of T; ::_thesis: for V being Subset of R^1 st f . p in V & V is open holds ex W being Subset of T st ( p in W & W is open & f .: W c= V ) let V be Subset of R^1; ::_thesis: ( f . p in V & V is open implies ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) assume A4: f . p in V ; ::_thesis: ( not V is open or ex W being Subset of T st ( p in W & W is open & f .: W c= V ) ) assume V is open ; ::_thesis: ex W being Subset of T st ( p in W & W is open & f .: W c= V ) then consider r being Element of REAL such that A5: r > 0 and A6: ].((f . p) - r),((f . p) + r).[ c= V by A4, FRECHET:8; ex W being open Subset of T st ( p in W & f .: W c= ].((f . p) - r),((f . p) + r).[ ) by A3, A5; hence ex W being Subset of T st ( p in W & W is open & f .: W c= V ) by A6, XBOOLE_1:1; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPS_4:22 for T being non empty TopSpace for f being Function of R^1,T holds ( f is continuous iff for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) proof let T be non empty TopSpace; ::_thesis: for f being Function of R^1,T holds ( f is continuous iff for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) let f be Function of R^1,T; ::_thesis: ( f is continuous iff for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) hereby ::_thesis: ( ( for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V let p be Point of R^1; ::_thesis: for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V let V be open Subset of T; ::_thesis: ( f . p in V implies ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ) assume f . p in V ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= V then consider W being Subset of R^1 such that A2: p in W and A3: W is open and A4: f .: W c= V by A1, JGRAPH_2:10; consider s being Element of REAL such that A5: s > 0 and A6: ].(p - s),(p + s).[ c= W by A2, A3, FRECHET:8; reconsider s = s as real positive number by A5; take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= V f .: ].(p - s),(p + s).[ c= f .: W by A6, RELAT_1:123; hence f .: ].(p - s),(p + s).[ c= V by A4, XBOOLE_1:1; ::_thesis: verum end; assume A7: for p being Point of R^1 for V being open Subset of T st f . p in V holds ex s being real positive number st f .: ].(p - s),(p + s).[ c= V ; ::_thesis: f is continuous for p being Point of R^1 for V being Subset of T st f . p in V & V is open holds ex W being Subset of R^1 st ( p in W & W is open & f .: W c= V ) proof let p be Point of R^1; ::_thesis: for V being Subset of T st f . p in V & V is open holds ex W being Subset of R^1 st ( p in W & W is open & f .: W c= V ) let V be Subset of T; ::_thesis: ( f . p in V & V is open implies ex W being Subset of R^1 st ( p in W & W is open & f .: W c= V ) ) assume that A8: f . p in V and A9: V is open ; ::_thesis: ex W being Subset of R^1 st ( p in W & W is open & f .: W c= V ) consider s being real positive number such that A10: f .: ].(p - s),(p + s).[ c= V by A7, A8, A9; take W = R^1 ].(p - s),(p + s).[; ::_thesis: ( p in W & W is open & f .: W c= V ) thus p in W by TOPREAL6:15; ::_thesis: ( W is open & f .: W c= V ) thus W is open ; ::_thesis: f .: W c= V thus f .: W c= V by A10; ::_thesis: verum end; hence f is continuous by JGRAPH_2:10; ::_thesis: verum end; theorem :: TOPS_4:23 for f being Function of R^1,R^1 holds ( f is continuous iff for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) proof let f be Function of R^1,R^1; ::_thesis: ( f is continuous iff for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) hereby ::_thesis: ( ( for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous ) assume A1: f is continuous ; ::_thesis: for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ let r be real positive number ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ reconsider p1 = p, q1 = f . p as Point of RealSpace ; consider s being real positive number such that A2: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17; take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ( p1 in REAL & q1 in REAL & r in REAL & s in REAL ) by XREAL_0:def_1; then ( Ball (p1,s) = ].(p1 - s),(p1 + s).[ & Ball (q1,r) = ].(q1 - r),(q1 + r).[ ) by FRECHET:7; hence f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ by A2; ::_thesis: verum end; assume A3: for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ ; ::_thesis: f is continuous for p, q being Point of RealSpace for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) proof let p, q be Point of RealSpace; ::_thesis: for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) assume A4: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) consider s being real positive number such that A5: f .: ].(p - s),(p + s).[ c= ].((f . p) - r),((f . p) + r).[ by A3; take s ; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r) ( p in REAL & q in REAL & r in REAL & s in REAL ) by XREAL_0:def_1; then ( Ball (p,s) = ].(p - s),(p + s).[ & Ball (q,r) = ].(q - r),(q + r).[ ) by FRECHET:7; hence f .: (Ball (p,s)) c= Ball (q,r) by A5, A4; ::_thesis: verum end; hence f is continuous by Th17; ::_thesis: verum end; theorem :: TOPS_4:24 for m being Nat for f being Function of (TOP-REAL m),R^1 holds ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) proof let m be Nat; ::_thesis: for f being Function of (TOP-REAL m),R^1 holds ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) let f be Function of (TOP-REAL m),R^1; ::_thesis: ( f is continuous iff for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider f1 = f as Function of (TopSpaceMetr (Euclid m)),R^1 ; A2: m in NAT by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ) implies f is continuous ) assume A3: f is continuous ; ::_thesis: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ let p be Point of (TOP-REAL m); ::_thesis: for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ let r be real positive number ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ reconsider p1 = p as Point of (Euclid m) by EUCLID:67; reconsider q1 = f . p as Point of RealSpace ; f1 is continuous by A1, A3, YELLOW12:36; then consider s being real positive number such that A4: f .: (Ball (p1,s)) c= Ball (q1,r) by A1, Th17; take s = s; ::_thesis: f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ( q1 in REAL & r in REAL ) by XREAL_0:def_1; then ( Ball (p1,s) = Ball (p,s) & Ball (q1,r) = ].((f . p) - r),((f . p) + r).[ ) by A2, FRECHET:7, TOPREAL9:13; hence f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ by A4; ::_thesis: verum end; assume A5: for p being Point of (TOP-REAL m) for r being real positive number ex s being real positive number st f .: (Ball (p,s)) c= ].((f . p) - r),((f . p) + r).[ ; ::_thesis: f is continuous for p being Point of (Euclid m) for q being Point of RealSpace for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) proof let p be Point of (Euclid m); ::_thesis: for q being Point of RealSpace for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) let q be Point of RealSpace; ::_thesis: for r being real positive number st q = f1 . p holds ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) let r be real positive number ; ::_thesis: ( q = f1 . p implies ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) ) assume A6: q = f1 . p ; ::_thesis: ex s being real positive number st f1 .: (Ball (p,s)) c= Ball (q,r) reconsider p1 = p as Point of (TOP-REAL m) by EUCLID:67; consider s being real positive number such that A7: f .: (Ball (p1,s)) c= ].((f . p) - r),((f . p) + r).[ by A5; take s ; ::_thesis: f1 .: (Ball (p,s)) c= Ball (q,r) ( q in REAL & r in REAL ) by XREAL_0:def_1; then ( Ball (p1,s) = Ball (p,s) & ].((f . p) - r),((f . p) + r).[ = Ball (q,r) ) by A2, A6, FRECHET:7, TOPREAL9:13; hence f1 .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum end; then f1 is continuous by Th17; hence f is continuous by A1, YELLOW12:36; ::_thesis: verum end; theorem :: TOPS_4:25 for m being Nat for f being Function of R^1,(TOP-REAL m) holds ( f is continuous iff for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ) proof let m be Nat; ::_thesis: for f being Function of R^1,(TOP-REAL m) holds ( f is continuous iff for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ) let f be Function of R^1,(TOP-REAL m); ::_thesis: ( f is continuous iff for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ) A1: TopStruct(# the U1 of (TOP-REAL m), the topology of (TOP-REAL m) #) = TopSpaceMetr (Euclid m) by EUCLID:def_8; then reconsider f1 = f as Function of R^1,(TopSpaceMetr (Euclid m)) ; A2: m in NAT by ORDINAL1:def_12; hereby ::_thesis: ( ( for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ) implies f is continuous ) assume A3: f is continuous ; ::_thesis: for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) let p be Point of R^1; ::_thesis: for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) let r be real positive number ; ::_thesis: ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) reconsider p1 = p as Point of RealSpace ; reconsider q1 = f . p as Point of (Euclid m) by EUCLID:67; f1 is continuous by A1, A3, YELLOW12:36; then consider s being real positive number such that A4: f1 .: (Ball (p1,s)) c= Ball (q1,r) by Th17; take s = s; ::_thesis: f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ( p in REAL & s in REAL ) by XREAL_0:def_1; then ( Ball (p1,s) = ].(p - s),(p + s).[ & Ball (q1,r) = Ball ((f . p),r) ) by A2, FRECHET:7, TOPREAL9:13; hence f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) by A4; ::_thesis: verum end; assume A5: for p being Point of R^1 for r being real positive number ex s being real positive number st f .: ].(p - s),(p + s).[ c= Ball ((f . p),r) ; ::_thesis: f is continuous for p being Point of RealSpace for q being Point of (Euclid m) for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) proof let p be Point of RealSpace; ::_thesis: for q being Point of (Euclid m) for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let q be Point of (Euclid m); ::_thesis: for r being real positive number st q = f . p holds ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) let r be real positive number ; ::_thesis: ( q = f . p implies ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) ) assume A6: q = f . p ; ::_thesis: ex s being real positive number st f .: (Ball (p,s)) c= Ball (q,r) reconsider p1 = p as Point of R^1 ; consider s being real positive number such that A7: f .: ].(p - s),(p + s).[ c= Ball ((f . p1),r) by A5; take s ; ::_thesis: f .: (Ball (p,s)) c= Ball (q,r) ( p in REAL & s in REAL ) by XREAL_0:def_1; then ( ].(p - s),(p + s).[ = Ball (p,s) & Ball ((f . p1),r) = Ball (q,r) ) by A2, A6, FRECHET:7, TOPREAL9:13; hence f .: (Ball (p,s)) c= Ball (q,r) by A7; ::_thesis: verum end; then f1 is continuous by A1, Th17; hence f is continuous by A1, YELLOW12:36; ::_thesis: verum end;