:: by Grzegorz Bancerek

::

:: Received November 7, 2005

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

theorem Th1: :: TOPGEN_5:1

for f, g being Function st f tolerates g holds

for A being set holds (f +* g) " A = (f " A) \/ (g " A)

for A being set holds (f +* g) " A = (f " A) \/ (g " A)

proof end;

theorem :: TOPGEN_5:2

theorem Th3: :: TOPGEN_5:3

for x, a being set

for f being Function st a in dom f holds

(commute (x .--> f)) . a = x .--> (f . a)

for f being Function st a in dom f holds

(commute (x .--> f)) . a = x .--> (f . a)

proof end;

theorem :: TOPGEN_5:4

for b being set

for f being Function holds

( b in dom (commute f) iff ex a being set ex g being Function st

( a in dom f & g = f . a & b in dom g ) )

for f being Function holds

( b in dom (commute f) iff ex a being set ex g being Function st

( a in dom f & g = f . a & b in dom g ) )

proof end;

theorem Th5: :: TOPGEN_5:5

for a, b being set

for f being Function holds

( a in dom ((commute f) . b) iff ex g being Function st

( a in dom f & g = f . a & b in dom g ) )

for f being Function holds

( a in dom ((commute f) . b) iff ex g being Function st

( a in dom f & g = f . a & b in dom g ) )

proof end;

theorem Th6: :: TOPGEN_5:6

for a, b being set

for f, g being Function st a in dom f & g = f . a & b in dom g holds

((commute f) . b) . a = g . b

for f, g being Function st a in dom f & g = f . a & b in dom g holds

((commute f) . b) . a = g . b

proof end;

theorem Th7: :: TOPGEN_5:7

for a being set

for f, g, h being Function st h = f \/ g holds

(commute h) . a = ((commute f) . a) \/ ((commute g) . a)

for f, g, h being Function st h = f \/ g holds

(commute h) . a = ((commute f) . a) \/ ((commute g) . a)

proof end;

theorem Th8: :: TOPGEN_5:8

for X, Y being set holds

( product <*X,Y*>,[:X,Y:] are_equipotent & card (product <*X,Y*>) = (card X) *` (card Y) )

( product <*X,Y*>,[:X,Y:] are_equipotent & card (product <*X,Y*>) = (card X) *` (card Y) )

proof end;

scheme :: TOPGEN_5:sch 1

SCH1{ P_{1}[ object ], F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( object ) -> set , F_{5}( object ) -> set } :

SCH1{ P

ex f being Function of F_{3}(),F_{2}() st

for a being Element of F_{1}() st a in F_{3}() holds

( ( P_{1}[a] implies f . a = F_{4}(a) ) & ( P_{1}[a] implies f . a = F_{5}(a) ) )

providedfor a being Element of F

( ( P

A1:
F_{3}() c= F_{1}()
and

A2: for a being Element of F_{1}() st a in F_{3}() holds

( ( P_{1}[a] implies F_{4}(a) in F_{2}() ) & ( P_{1}[a] implies F_{5}(a) in F_{2}() ) )

A2: for a being Element of F

( ( P

proof end;

scheme :: TOPGEN_5:sch 2

SCH2{ P_{1}[ object ], P_{2}[ object ], F_{1}() -> non empty set , F_{2}() -> non empty set , F_{3}() -> non empty set , F_{4}( object ) -> object , F_{5}( object ) -> object , F_{6}( object ) -> object } :

SCH2{ P

ex f being Function of F_{3}(),F_{2}() st

for a being Element of F_{1}() st a in F_{3}() holds

( ( P_{1}[a] implies f . a = F_{4}(a) ) & ( P_{1}[a] & P_{2}[a] implies f . a = F_{5}(a) ) & ( P_{1}[a] & P_{2}[a] implies f . a = F_{6}(a) ) )

providedfor a being Element of F

( ( P

A1:
F_{3}() c= F_{1}()
and

A2: for a being Element of F_{1}() st a in F_{3}() holds

( ( P_{1}[a] implies F_{4}(a) in F_{2}() ) & ( P_{1}[a] & P_{2}[a] implies F_{5}(a) in F_{2}() ) & ( P_{1}[a] & P_{2}[a] implies F_{6}(a) in F_{2}() ) )

A2: for a being Element of F

( ( P

proof end;

theorem Th10: :: TOPGEN_5:10

for X being TopSpace

for Y being non empty TopSpace

for A, B being closed Subset of X

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | B),Y st f tolerates g holds

f +* g is continuous Function of (X | (A \/ B)),Y

for Y being non empty TopSpace

for A, B being closed Subset of X

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | B),Y st f tolerates g holds

f +* g is continuous Function of (X | (A \/ B)),Y

proof end;

theorem Th11: :: TOPGEN_5:11

for X being TopSpace

for Y being non empty TopSpace

for A, B being closed Subset of X st A misses B holds

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y

for Y being non empty TopSpace

for A, B being closed Subset of X st A misses B holds

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | B),Y holds f +* g is continuous Function of (X | (A \/ B)),Y

proof end;

theorem Th12: :: TOPGEN_5:12

for X being TopSpace

for Y being non empty TopSpace

for A being open closed Subset of X

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y

for Y being non empty TopSpace

for A being open closed Subset of X

for f being continuous Function of (X | A),Y

for g being continuous Function of (X | (A `)),Y holds f +* g is continuous Function of X,Y

proof end;

theorem Th13: :: TOPGEN_5:13

for n being Element of NAT

for a being Point of (TOP-REAL n)

for r being positive Real holds a in Ball (a,r)

for a being Point of (TOP-REAL n)

for r being positive Real holds a in Ball (a,r)

proof end;

definition

{ |[x,0]| where x is Real : verum } is Subset of (TOP-REAL 2)

{ |[x,y]| where x, y is Real : y >= 0 } is Subset of (TOP-REAL 2)
end;

func y=0-line -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 1

{ |[x,0]| where x is Real : verum } ;

coherence { |[x,0]| where x is Real : verum } ;

{ |[x,0]| where x is Real : verum } is Subset of (TOP-REAL 2)

proof end;

func y>=0-plane -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 2

{ |[x,y]| where x, y is Real : y >= 0 } ;

coherence { |[x,y]| where x, y is Real : y >= 0 } ;

{ |[x,y]| where x, y is Real : y >= 0 } is Subset of (TOP-REAL 2)

proof end;

:: deftheorem defines y>=0-plane TOPGEN_5:def 2 :

y>=0-plane = { |[x,y]| where x, y is Real : y >= 0 } ;

y>=0-plane = { |[x,y]| where x, y is Real : y >= 0 } ;

theorem :: TOPGEN_5:17

for a, b being set holds

( <*a,b*> in y>=0-plane iff ( a in REAL & ex y being Real st

( b = y & y >= 0 ) ) )

( <*a,b*> in y>=0-plane iff ( a in REAL & ex y being Real st

( b = y & y >= 0 ) ) )

proof end;

registration
end;

theorem Th22: :: TOPGEN_5:22

for n being Element of NAT

for a, b being Element of (TOP-REAL n)

for r1, r2 being positive Real st |.(a - b).| <= r1 - r2 holds

Ball (b,r2) c= Ball (a,r1)

for a, b being Element of (TOP-REAL n)

for r1, r2 being positive Real st |.(a - b).| <= r1 - r2 holds

Ball (b,r2) c= Ball (a,r1)

proof end;

theorem Th23: :: TOPGEN_5:23

for a being Real

for r1, r2 being positive Real st r1 <= r2 holds

Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2)

for r1, r2 being positive Real st r1 <= r2 holds

Ball (|[a,r1]|,r1) c= Ball (|[a,r2]|,r2)

proof end;

theorem Th24: :: TOPGEN_5:24

for T1, T2 being non empty TopSpace

for B1 being Neighborhood_System of T1

for B2 being Neighborhood_System of T2 st B1 = B2 holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

for B1 being Neighborhood_System of T1

for B2 being Neighborhood_System of T2 st B1 = B2 holds

TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #)

proof end;

definition

ex b_{1} being non empty strict TopSpace st

( the carrier of b_{1} = y>=0-plane & ex B being Neighborhood_System of b_{1} st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) )

for b_{1}, b_{2} being non empty strict TopSpace st the carrier of b_{1} = y>=0-plane & ex B being Neighborhood_System of b_{1} st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) & the carrier of b_{2} = y>=0-plane & ex B being Neighborhood_System of b_{2} st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) holds

b_{1} = b_{2}
end;

func Niemytzki-plane -> non empty strict TopSpace means :Def3: :: TOPGEN_5:def 3

( the carrier of it = y>=0-plane & ex B being Neighborhood_System of it st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) );

existence ( the carrier of it = y>=0-plane & ex B being Neighborhood_System of it st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) );

ex b

( the carrier of b

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) )

proof end;

uniqueness for b

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) & the carrier of b

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) holds

b

proof end;

:: deftheorem Def3 defines Niemytzki-plane TOPGEN_5:def 3 :

for b_{1} being non empty strict TopSpace holds

( b_{1} = Niemytzki-plane iff ( the carrier of b_{1} = y>=0-plane & ex B being Neighborhood_System of b_{1} st

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) ) );

for b

( b

( ( for x being Real holds B . |[x,0]| = { ((Ball (|[x,r]|,r)) \/ {|[x,0]|}) where r is Real : r > 0 } ) & ( for x, y being Real st y > 0 holds

B . |[x,y]| = { ((Ball (|[x,y]|,r)) /\ y>=0-plane) where r is Real : r > 0 } ) ) ) );

Lm1: the carrier of Niemytzki-plane = y>=0-plane

by Def3;

theorem Th27: :: TOPGEN_5:27

for x being Real

for r being positive Real holds (Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane

for r being positive Real holds (Ball (|[x,r]|,r)) \/ {|[x,0]|} is open Subset of Niemytzki-plane

proof end;

theorem Th28: :: TOPGEN_5:28

for x being Real

for y, r being positive Real holds (Ball (|[x,y]|,r)) /\ y>=0-plane is open Subset of Niemytzki-plane

for y, r being positive Real holds (Ball (|[x,y]|,r)) /\ y>=0-plane is open Subset of Niemytzki-plane

proof end;

theorem Th29: :: TOPGEN_5:29

for x, y being Real

for r being positive Real st r <= y holds

Ball (|[x,y]|,r) is open Subset of Niemytzki-plane

for r being positive Real st r <= y holds

Ball (|[x,y]|,r) is open Subset of Niemytzki-plane

proof end;

theorem Th30: :: TOPGEN_5:30

for p being Point of Niemytzki-plane

for r being positive Real ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st

( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds

|.(b - a).| < r ) )

for r being positive Real ex a being Point of (TOP-REAL 2) ex U being open Subset of Niemytzki-plane st

( p in U & a in U & ( for b being Point of (TOP-REAL 2) st b in U holds

|.(b - a).| < r ) )

proof end;

theorem Th31: :: TOPGEN_5:31

for x, y being Real

for r being positive Real ex w, v being Rational st

( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )

for r being positive Real ex w, v being Rational st

( |[w,v]| in Ball (|[x,y]|,r) & |[w,v]| <> |[x,y]| )

proof end;

theorem Th32: :: TOPGEN_5:32

for A being Subset of Niemytzki-plane st A = (y>=0-plane \ y=0-line) /\ (product <*RAT,RAT*>) holds

for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

proof end;

theorem Th33: :: TOPGEN_5:33

for A being Subset of Niemytzki-plane st A = y>=0-plane \ y=0-line holds

for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

for x being set holds Cl (A \ {x}) = [#] Niemytzki-plane

proof end;

:: deftheorem defines Tychonoff TOPGEN_5:def 4 :

for T being TopSpace holds

( T is Tychonoff iff for A being closed Subset of T

for a being Point of T st a in A ` holds

ex f being continuous Function of T,I[01] st

( f . a = 0 & f .: A c= {1} ) );

for T being TopSpace holds

( T is Tychonoff iff for A being closed Subset of T

for a being Point of T st a in A ` holds

ex f being continuous Function of T,I[01] st

( f . a = 0 & f .: A c= {1} ) );

registration

coherence

for b_{1} being TopSpace st b_{1} is Tychonoff holds

b_{1} is regular

for b_{1} being non empty TopSpace st b_{1} is T_4 holds

b_{1} is Tychonoff

end;
for b

b

proof end;

coherence for b

b

proof end;

theorem :: TOPGEN_5:48

for X being T_1 TopSpace st X is Tychonoff holds

for B being prebasis of X

for x being Point of X

for V being Subset of X st x in V & V in B holds

ex f being continuous Function of X,I[01] st

( f . x = 0 & f .: (V `) c= {1} )

for B being prebasis of X

for x being Point of X

for V being Subset of X st x in V & V in B holds

ex f being continuous Function of X,I[01] st

( f . x = 0 & f .: (V `) c= {1} )

proof end;

theorem Th49: :: TOPGEN_5:49

for X being TopSpace

for R being non empty SubSpace of R^1

for f, g being continuous Function of X,R

for A being Subset of X st ( for x being Point of X holds

( x in A iff f . x <= g . x ) ) holds

A is closed

for R being non empty SubSpace of R^1

for f, g being continuous Function of X,R

for A being Subset of X st ( for x being Point of X holds

( x in A iff f . x <= g . x ) ) holds

A is closed

proof end;

theorem Th50: :: TOPGEN_5:50

for X being TopSpace

for R being non empty SubSpace of R^1

for f, g being continuous Function of X,R ex h being continuous Function of X,R st

for x being Point of X holds h . x = max ((f . x),(g . x))

for R being non empty SubSpace of R^1

for f, g being continuous Function of X,R ex h being continuous Function of X,R st

for x being Point of X holds h . x = max ((f . x),(g . x))

proof end;

theorem Th51: :: TOPGEN_5:51

for X being non empty TopSpace

for R being non empty SubSpace of R^1

for A being non empty finite set

for F being ManySortedFunction of A st ( for a being set st a in A holds

F . a is continuous Function of X,R ) holds

ex f being continuous Function of X,R st

for x being Point of X

for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds

f . x = max S

for R being non empty SubSpace of R^1

for A being non empty finite set

for F being ManySortedFunction of A st ( for a being set st a in A holds

F . a is continuous Function of X,R ) holds

ex f being continuous Function of X,R st

for x being Point of X

for S being non empty finite Subset of REAL st S = rng ((commute F) . x) holds

f . x = max S

proof end;

theorem Th52: :: TOPGEN_5:52

for X being non empty T_1 TopSpace

for B being prebasis of X st ( for x being Point of X

for V being Subset of X st x in V & V in B holds

ex f being continuous Function of X,I[01] st

( f . x = 0 & f .: (V `) c= {1} ) ) holds

X is Tychonoff

for B being prebasis of X st ( for x being Point of X

for V being Subset of X st x in V & V in B holds

ex f being continuous Function of X,I[01] st

( f . x = 0 & f .: (V `) c= {1} ) ) holds

X is Tychonoff

proof end;

::<DESC name="1.4.4. Przyk/lad funkcji ci/ag/lej ze strza/lce w [0,1]" monograph="topology"/>

theorem Th58: :: TOPGEN_5:58

for x being Real

for w being Rational ex f being continuous Function of Sorgenfrey-line,I[01] st

for a being Point of Sorgenfrey-line holds

( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )

for w being Rational ex f being continuous Function of Sorgenfrey-line,I[01] st

for a being Point of Sorgenfrey-line holds

( ( a in [.x,w.[ implies f . a = 0 ) & ( not a in [.x,w.[ implies f . a = 1 ) )

proof end;

::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>

definition

let x be Real;

let r be positive Real;

ex b_{1} being Function of Niemytzki-plane,I[01] st

( b_{1} . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b_{1} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies b_{1} . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )

for b_{1}, b_{2} being Function of Niemytzki-plane,I[01] st b_{1} . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b_{1} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies b_{1} . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) & b_{2} . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b_{2} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies b_{2} . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) holds

b_{1} = b_{2}

end;
let r be positive Real;

func + (x,r) -> Function of Niemytzki-plane,I[01] means :Def5: :: TOPGEN_5:def 5

( it . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) );

existence ( it . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies it . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) );

ex b

( b

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b

proof end;

uniqueness for b

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b

b

proof end;

:: deftheorem Def5 defines + TOPGEN_5:def 5 :

for x being Real

for r being positive Real

for b_{3} being Function of Niemytzki-plane,I[01] holds

( b_{3} = + (x,r) iff ( b_{3} . |[x,0]| = 0 & ( for a being Real

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b_{3} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,r]|,r) implies b_{3} . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) ) );

for x being Real

for r being positive Real

for b

( b

for b being non negative Real holds

( ( ( a <> x or b <> 0 ) & not |[a,b]| in Ball (|[x,r]|,r) implies b

theorem Th60: :: TOPGEN_5:60

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds

for x being Real

for r being positive Real st (+ (x,r)) . p = 0 holds

p = |[x,0]|

for x being Real

for r being positive Real st (+ (x,r)) . p = 0 holds

p = |[x,0]|

proof end;

theorem Th62: :: TOPGEN_5:62

for p being Point of (TOP-REAL 2)

for x being Real

for a, r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds

(+ (x,r)) . p = a

for x being Real

for a, r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| = r * a & p `2 <> 0 holds

(+ (x,r)) . p = a

proof end;

theorem Th63: :: TOPGEN_5:63

for p being Point of (TOP-REAL 2)

for x, a being Real

for r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds

(+ (x,r)) . p < a

for x, a being Real

for r being positive Real st a <= 1 & |.(p - |[x,(r * a)]|).| < r * a holds

(+ (x,r)) . p < a

proof end;

theorem Th64: :: TOPGEN_5:64

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds

for x, a being Real

for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds

(+ (x,r)) . p > a

for x, a being Real

for r being positive Real st 0 <= a & a < 1 & |.(p - |[x,(r * a)]|).| > r * a holds

(+ (x,r)) . p > a

proof end;

theorem Th65: :: TOPGEN_5:65

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds

for x, a, b being Real

for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds

ex r1 being positive Real st

( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )

for x, a, b being Real

for r being positive Real st 0 <= a & b <= 1 & (+ (x,r)) . p in ].a,b.[ holds

ex r1 being positive Real st

( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,b.[ )

proof end;

theorem Th66: :: TOPGEN_5:66

for x being Real

for a, r being positive Real holds Ball (|[x,(r * a)]|,(r * a)) c= (+ (x,r)) " ].0,a.[

for a, r being positive Real holds Ball (|[x,(r * a)]|,(r * a)) c= (+ (x,r)) " ].0,a.[

proof end;

theorem Th67: :: TOPGEN_5:67

for x being Real

for a, r being positive Real holds (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[

for a, r being positive Real holds (Ball (|[x,(r * a)]|,(r * a))) \/ {|[x,0]|} c= (+ (x,r)) " [.0,a.[

proof end;

theorem Th68: :: TOPGEN_5:68

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds

for x, a being Real

for r being positive Real st 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 holds

p in Ball (|[x,(r * a)]|,(r * a))

for x, a being Real

for r being positive Real st 0 < (+ (x,r)) . p & (+ (x,r)) . p < a & a <= 1 holds

p in Ball (|[x,(r * a)]|,(r * a))

proof end;

theorem Th69: :: TOPGEN_5:69

for p being Point of (TOP-REAL 2) st p `2 > 0 holds

for x, a being Real

for r being positive Real st 0 <= a & a < (+ (x,r)) . p holds

ex r1 being positive Real st

( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )

for x, a being Real

for r being positive Real st 0 <= a & a < (+ (x,r)) . p holds

ex r1 being positive Real st

( r1 <= p `2 & Ball (p,r1) c= (+ (x,r)) " ].a,1.] )

proof end;

theorem Th70: :: TOPGEN_5:70

for p being Point of (TOP-REAL 2) st p `2 = 0 holds

for x being Real

for r being positive Real st (+ (x,r)) . p = 1 holds

ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}

for x being Real

for r being positive Real st (+ (x,r)) . p = 1 holds

ex r1 being positive Real st (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,r)) " {1}

proof end;

theorem Th71: :: TOPGEN_5:71

for T being non empty TopSpace

for S being SubSpace of T

for B being Basis of T holds { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S

for S being SubSpace of T

for B being Basis of T holds { (A /\ ([#] S)) where A is Subset of T : ( A in B & A meets [#] S ) } is Basis of S

proof end;

theorem Th73: :: TOPGEN_5:73

for T being TopSpace

for U, V being Subset of T

for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds

B is Basis of T

for U, V being Subset of T

for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds

B is Basis of T

proof end;

theorem Th74: :: TOPGEN_5:74

( { [.0,a.[ where a is Real : ( 0 < a & a <= 1 ) } \/ { ].a,1.] where a is Real : ( 0 <= a & a < 1 ) } ) \/ { ].a,b.[ where a, b is Real : ( 0 <= a & a < b & b <= 1 ) } is Basis of I[01]

proof end;

theorem Th75: :: TOPGEN_5:75

for T being non empty TopSpace

for f being Function of T,I[01] holds

( f is continuous iff for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds

( f " [.0,b.[ is open & f " ].a,1.] is open ) )

for f being Function of T,I[01] holds

( f is continuous iff for a, b being Real st 0 <= a & a < 1 & 0 < b & b <= 1 holds

( f " [.0,b.[ is open & f " ].a,1.] is open ) )

proof end;

theorem Th76: :: TOPGEN_5:76

for U being Subset of Niemytzki-plane

for x being Real

for r being positive Real st U = (Ball (|[x,r]|,r)) \/ {|[x,0]|} holds

ex f being continuous Function of Niemytzki-plane,I[01] st

( f . |[x,0]| = 0 & ( for a, b being Real holds

( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0]|} implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )

for x being Real

for r being positive Real st U = (Ball (|[x,r]|,r)) \/ {|[x,0]|} holds

ex f being continuous Function of Niemytzki-plane,I[01] st

( f . |[x,0]| = 0 & ( for a, b being Real holds

( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U \ {|[x,0]|} implies f . |[a,b]| = (|.(|[x,0]| - |[a,b]|).| ^2) / ((2 * r) * b) ) ) ) )

proof end;

::<DESC name="1.4.5. Przyk/lad funkcji ci/ag/lej z p/laszczyzny Niemytzkiego w R^1" monograph="topology"/>

definition

let x, y be Real;

let r be positive Real;

ex b_{1} being Function of Niemytzki-plane,I[01] st

for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b_{1} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies b_{1} . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) )

for b_{1}, b_{2} being Function of Niemytzki-plane,I[01] st ( for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b_{1} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies b_{1} . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) & ( for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b_{2} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies b_{2} . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) holds

b_{1} = b_{2}

end;
let r be positive Real;

func + (x,y,r) -> Function of Niemytzki-plane,I[01] means :Def6: :: TOPGEN_5:def 6

for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies it . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) );

existence for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies it . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies it . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) );

ex b

for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b

proof end;

uniqueness for b

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b

b

proof end;

:: deftheorem Def6 defines + TOPGEN_5:def 6 :

for x, y being Real

for r being positive Real

for b_{4} being Function of Niemytzki-plane,I[01] holds

( b_{4} = + (x,y,r) iff for a being Real

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b_{4} . |[a,b]| = 1 ) & ( |[a,b]| in Ball (|[x,y]|,r) implies b_{4} . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) );

for x, y being Real

for r being positive Real

for b

( b

for b being non negative Real holds

( ( not |[a,b]| in Ball (|[x,y]|,r) implies b

theorem Th77: :: TOPGEN_5:77

for p being Point of (TOP-REAL 2) st p `2 >= 0 holds

for x being Real

for y being non negative Real

for r being positive Real holds

( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )

for x being Real

for y being non negative Real

for r being positive Real holds

( (+ (x,y,r)) . p = 0 iff p = |[x,y]| )

proof end;

theorem Th78: :: TOPGEN_5:78

for x being Real

for y being non negative Real

for r, a being positive Real st a <= 1 holds

(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane

for y being non negative Real

for r, a being positive Real st a <= 1 holds

(+ (x,y,r)) " [.0,a.[ = (Ball (|[x,y]|,(r * a))) /\ y>=0-plane

proof end;

theorem Th79: :: TOPGEN_5:79

for p being Point of (TOP-REAL 2) st p `2 > 0 holds

for x being Real

for a being non negative Real

for y, r being positive Real st (+ (x,y,r)) . p > a holds

( |.(|[x,y]| - p).| > r * a & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] )

for x being Real

for a being non negative Real

for y, r being positive Real st (+ (x,y,r)) . p > a holds

( |.(|[x,y]| - p).| > r * a & (Ball (p,(|.(|[x,y]| - p).| - (r * a)))) /\ y>=0-plane c= (+ (x,y,r)) " ].a,1.] )

proof end;

theorem Th80: :: TOPGEN_5:80

for p being Point of (TOP-REAL 2) st p `2 = 0 holds

for x being Real

for a being non negative Real

for y, r being positive Real st (+ (x,y,r)) . p > a holds

( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st

( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )

for x being Real

for a being non negative Real

for y, r being positive Real st (+ (x,y,r)) . p > a holds

( |.(|[x,y]| - p).| > r * a & ex r1 being positive Real st

( r1 = (|.(|[x,y]| - p).| - (r * a)) / 2 & (Ball (|[(p `1),r1]|,r1)) \/ {p} c= (+ (x,y,r)) " ].a,1.] ) )

proof end;

registration
end;

theorem Th81: :: TOPGEN_5:81

for U being Subset of Niemytzki-plane

for x, y being Real

for r being positive Real st y > 0 & U = (Ball (|[x,y]|,r)) /\ y>=0-plane holds

ex f being continuous Function of Niemytzki-plane,I[01] st

( f . |[x,y]| = 0 & ( for a, b being Real holds

( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )

for x, y being Real

for r being positive Real st y > 0 & U = (Ball (|[x,y]|,r)) /\ y>=0-plane holds

ex f being continuous Function of Niemytzki-plane,I[01] st

( f . |[x,y]| = 0 & ( for a, b being Real holds

( ( |[a,b]| in U ` implies f . |[a,b]| = 1 ) & ( |[a,b]| in U implies f . |[a,b]| = |.(|[x,y]| - |[a,b]|).| / r ) ) ) )

proof end;