:: TOPGEN_5 semantic presentation

theorem Th1: :: TOPGEN_5:1

for b₁, b₂ being Function st b₁ tolerates b₂ holds
for b₃ being set holds (b₁ +* b₂) " b₃ = (b₁ " b₃) \/ (b₂ " b₃)

proof end;

theorem Th2: :: TOPGEN_5:2

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
for b₃ being set holds (b₁ +* b₂) " b₃ = (b₁ " b₃) \/ (b₂ " b₃)

proof end;

registration

let c₁ be set ;
let c₂ be real-membered set ;
cluster -> real-yielding Relation of a₁,a₂;
coherence

proof end;

end;

theorem Th3: :: TOPGEN_5:3

for b₁, b₂ being set
for b₃ being Function st b₂ in dom b₃ holds
(commute (b₁ .--> b₃)) . b₂ = b₁ .--> (b₃ . b₂)

proof end;

theorem Th4: :: TOPGEN_5:4

for b₁ being set
for b₂ being Function holds
( b₁ in dom (commute b₂) iff ex b₃ being set ex b₄ being Function st
( b₃ in dom b₂ & b₄ = b₂ . b₃ & b₁ in dom b₄ ) )

proof end;

theorem Th5: :: TOPGEN_5:5

for b₁, b₂ being set
for b₃ being Function holds
( b₁ in dom ((commute b₃) . b₂) iff ex b₄ being Function st
( b₁ in dom b₃ & b₄ = b₃ . b₁ & b₂ in dom b₄ ) )

proof end;

theorem Th6: :: TOPGEN_5:6

for b₁, b₂ being set
for b₃, b₄ being Function st b₁ in dom b₃ & b₄ = b₃ . b₁ & b₂ in dom b₄ holds
((commute b₃) . b₂) . b₁ = b₄ . b₂

proof end;

theorem Th7: :: TOPGEN_5:7

for b₁ being set
for b₂, b₃, b₄ being Function st b₄ = b₂ \/ b₃ holds
(commute b₄) . b₁ = ((commute b₂) . b₁) \/ ((commute b₃) . b₁)

proof end;

registration

cluster finite -> finite bounded Element of bool REAL ;
coherence

proof end;

end;

theorem Th8: :: TOPGEN_5:8

for b₁, b₂, b₃, b₄ being real number st b₁ < b₂ & b₃ <= b₄ holds
].b₁,b₃.[ /\ [.b₂,b₄.] = [.b₂,b₃.[

proof end;

theorem Th9: :: TOPGEN_5:9

for b₁, b₂, b₃, b₄ being real number st b₁ >= b₂ & b₃ > b₄ holds
].b₁,b₃.[ /\ [.b₂,b₄.] = ].b₁,b₄.]

proof end;

theorem Th10: :: TOPGEN_5:10

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ holds
[.b₁,b₃.[ \/ ].b₂,b₄.] = [.b₁,b₄.]

proof end;

theorem Th11: :: TOPGEN_5:11

for b₁, b₂, b₃, b₄ being real number st b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ holds
[.b₁,b₃.[ /\ ].b₂,b₄.] = ].b₂,b₃.[

proof end;

theorem Th12: :: TOPGEN_5:12

for b₁, b₂ being set holds
( product <*b₁,b₂*>,[:b₁,b₂:] are_equipotent & Card (product <*b₁,b₂*>) = (Card b₁) *` (Card b₂) )

proof end;

scheme :: TOPGEN_5:sch 1
s1{ P₁[ set ], F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set ) -> set , F₅( set ) -> set } :

ex b₁ being Function of F₃(),F₂() st
for b₂ being Element of F₁() st b₂ in F₃() holds
( ( P₁[b₂] implies b₁ . b₂ = F₄(b₂) ) & ( P₁[b₂] implies b₁ . b₂ = F₅(b₂) ) )

provided

E11: F₃() c= F₁() and
E12: for b₁ being Element of F₁() st b₁ in F₃() holds
( ( P₁[b₁] implies F₄(b₁) in F₂() ) & ( P₁[b₁] implies F₅(b₁) in F₂() ) )

proof end;

scheme :: TOPGEN_5:sch 2
s2{ P₁[ set ], P₂[ set ], F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set ) -> set , F₅( set ) -> set , F₆( set ) -> set } :

ex b₁ being Function of F₃(),F₂() st
for b₂ being Element of F₁() st b₂ in F₃() holds
( ( P₁[b₂] implies b₁ . b₂ = F₄(b₂) ) & ( P₁[b₂] & P₂[b₂] implies b₁ . b₂ = F₅(b₂) ) & ( P₁[b₂] & P₂[b₂] implies b₁ . b₂ = F₆(b₂) ) )

provided

E11: F₃() c= F₁() and
E12: for b₁ being Element of F₁() st b₁ in F₃() holds
( ( P₁[b₁] implies F₄(b₁) in F₂() ) & ( P₁[b₁] & P₂[b₁] implies F₅(b₁) in F₂() ) & ( P₁[b₁] & P₂[b₁] implies F₆(b₁) in F₂() ) )

proof end;

theorem Th13: :: TOPGEN_5:13

for b₁, b₂ being real number holds |.|[b₁,b₂]|.| ^2 = (b₁ ^2 ) + (b₂ ^2 )

proof end;

theorem Th14: :: TOPGEN_5:14

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃, b₄ being closed Subset of b₁
for b₅ being continuous Function of (b₁ | b₃),b₂
for b₆ being continuous Function of (b₁ | b₄),b₂ st b₅ tolerates b₆ holds
b₅ +* b₆ is continuous Function of (b₁ | (b₃ \/ b₄)),b₂

proof end;

theorem Th15: :: TOPGEN_5:15

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃, b₄ being closed Subset of b₁ st b₃ misses b₄ holds
for b₅ being continuous Function of (b₁ | b₃),b₂
for b₆ being continuous Function of (b₁ | b₄),b₂ holds b₅ +* b₆ is continuous Function of (b₁ | (b₃ \/ b₄)),b₂

proof end;

theorem Th16: :: TOPGEN_5:16

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being open closed Subset of b₁
for b₄ being continuous Function of (b₁ | b₃),b₂
for b₅ being continuous Function of (b₁ | (b₃ ` )),b₂ holds b₄ +* b₅ is continuous Function of b₁,b₂

proof end;

theorem Th17: :: TOPGEN_5:17

for b₁ being Nat
for b₂ being Point of (TOP-REAL b₁)
for b₃ being real positive number holds b₂ in Ball b₂,b₃

proof end;

definition

func y=0-line -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 1
{ |[b₁,0]| where B is Element of REAL : verum } ;
coherence

proof end;

func y>=0-plane -> Subset of (TOP-REAL 2) equals :: TOPGEN_5:def 2
{ |[b₁,b₂]| where B is Element of REAL , B is Element of REAL : b₂ >= 0 } ;
coherence

proof end;

end;

:: deftheorem Def1 defines y=0-line TOPGEN_5:def 1 :

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

theorem Th18: :: TOPGEN_5:18

for b₁, b₂ being set holds
( <*b₁,b₂*> in y=0-line iff ( b₁ in REAL & b₂ = 0 ) )

proof end;

theorem Th19: :: TOPGEN_5:19

for b₁, b₂ being real number holds
( |[b₁,b₂]| in y=0-line iff b₂ = 0 )

proof end;

theorem Th20: :: TOPGEN_5:20

Card y=0-line = continuum

proof end;

theorem Th21: :: TOPGEN_5:21

for b₁, b₂ being set holds
( <*b₁,b₂*> in y>=0-plane iff ( b₁ in REAL & ex b₃ being Element of REAL st
( b₂ = b₃ & b₃ >= 0 ) ) )

proof end;

theorem Th22: :: TOPGEN_5:22

for b₁, b₂ being real number holds
( |[b₁,b₂]| in y>=0-plane iff b₂ >= 0 )

proof end;

registration

cluster y=0-line -> non empty ;
coherence by Th19;
cluster y>=0-plane -> non empty ;
coherence by Th22;

end;

theorem Th23: :: TOPGEN_5:23

y=0-line c= y>=0-plane

proof end;

theorem Th24: :: TOPGEN_5:24

for b₁, b₂, b₃ being real number st b₃ > 0 holds
( Ball |[b₁,b₂]|,b₃ c= y>=0-plane iff b₃ <= b₂ )

proof end;

theorem Th25: :: TOPGEN_5:25

for b₁, b₂, b₃ being real number st b₃ > 0 & b₂ >= 0 holds
( Ball |[b₁,b₂]|,b₃ misses y=0-line iff b₃ <= b₂ )

proof end;

theorem Th26: :: TOPGEN_5:26

for b₁ being Nat
for b₂, b₃ being Element of (TOP-REAL b₁)
for b₄, b₅ being real positive number st |.(b₂ - b₃).| <= b₄ - b₅ holds
Ball b₃,b₅ c= Ball b₂,b₄

proof end;

theorem Th27: :: TOPGEN_5:27

for b₁ being real number
for b₂, b₃ being real positive number st b₂ <= b₃ holds
Ball |[b₁,b₂]|,b₂ c= Ball |[b₁,b₃]|,b₃

proof end;

theorem Th28: :: TOPGEN_5:28

for b₁, b₂ being non empty TopSpace
for b₃ being Neighborhood_System of b₁
for b₄ being Neighborhood_System of b₂ st b₃ = b₄ holds
TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #)

proof end;

definition

func Niemytzki-plane -> non empty strict TopSpace means :Def3: :: TOPGEN_5:def 3
( the carrier of a₁ = y>=0-plane & ex b₁ being Neighborhood_System of a₁ st
( ( for b₂ being Element of REAL holds b₁ . |[b₂,0]| = { ((Ball |[b₂,b₃]|,b₃) \/ {|[b₂,0]|}) where B is Element of REAL : b₃ > 0 } ) & ( for b₂, b₃ being Element of REAL st b₃ > 0 holds
b₁ . |[b₂,b₃]| = { ((Ball |[b₂,b₃]|,b₄) /\ y>=0-plane ) where B is Element of REAL : b₄ > 0 } ) ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th29: :: TOPGEN_5:29

y>=0-plane \ y=0-line is open Subset of Niemytzki-plane

proof end;

Lemma27: the carrier of Niemytzki-plane = y>=0-plane
by Def3;

theorem Th30: :: TOPGEN_5:30

y=0-line is closed Subset of Niemytzki-plane

proof end;

theorem Th31: :: TOPGEN_5:31

for b₁ being real number
for b₂ being real positive number holds (Ball |[b₁,b₂]|,b₂) \/ {|[b₁,0]|} is open Subset of Niemytzki-plane

proof end;

theorem Th32: :: TOPGEN_5:32

for b₁ being real number
for b₂, b₃ being real positive number holds (Ball |[b₁,b₂]|,b₃) /\ y>=0-plane is open Subset of Niemytzki-plane

proof end;

theorem Th33: :: TOPGEN_5:33

for b₁, b₂ being real number
for b₃ being real positive number st b₃ <= b₂ holds
Ball |[b₁,b₂]|,b₃ is open Subset of Niemytzki-plane

proof end;

theorem Th34: :: TOPGEN_5:34

for b₁ being Point of Niemytzki-plane
for b₂ being real positive number ex b₃ being Point of (TOP-REAL 2)ex b₄ being open Subset of Niemytzki-plane st
( b₁ in b₄ & b₃ in b₄ & ( for b₅ being Point of (TOP-REAL 2) st b₅ in b₄ holds
|.(b₅ - b₃).| < b₂ ) )

proof end;

theorem Th35: :: TOPGEN_5:35

for b₁, b₂ being real number
for b₃ being real positive number ex b₄, b₅ being rational number st
( |[b₄,b₅]| in Ball |[b₁,b₂]|,b₃ & |[b₄,b₅]| <> |[b₁,b₂]| )

proof end;

theorem Th36: :: TOPGEN_5:36

for b₁ being Subset of Niemytzki-plane st b₁ = (y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) holds
for b₂ being set holds Cl (b₁ \ {b₂}) = [#] Niemytzki-plane

proof end;

theorem Th37: :: TOPGEN_5:37

for b₁ being Subset of Niemytzki-plane st b₁ = y>=0-plane \ y=0-line holds
for b₂ being set holds Cl (b₁ \ {b₂}) = [#] Niemytzki-plane

proof end;

theorem Th38: :: TOPGEN_5:38

for b₁ being Subset of Niemytzki-plane st b₁ = y>=0-plane \ y=0-line holds
Cl b₁ = [#] Niemytzki-plane

proof end;

theorem Th39: :: TOPGEN_5:39

for b₁ being Subset of Niemytzki-plane st b₁ = y=0-line holds
( Cl b₁ = b₁ & Int b₁ = {} )

proof end;

theorem Th40: :: TOPGEN_5:40

(y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) is dense Subset of Niemytzki-plane

proof end;

theorem Th41: :: TOPGEN_5:41

(y>=0-plane \ y=0-line ) /\ (product <*RAT ,RAT *>) is dense-in-itself Subset of Niemytzki-plane

proof end;

theorem Th42: :: TOPGEN_5:42

y>=0-plane \ y=0-line is dense Subset of Niemytzki-plane

proof end;

theorem Th43: :: TOPGEN_5:43

y>=0-plane \ y=0-line is dense-in-itself Subset of Niemytzki-plane

proof end;

theorem Th44: :: TOPGEN_5:44

y=0-line is nowhere_dense Subset of Niemytzki-plane

proof end;

theorem Th45: :: TOPGEN_5:45

for b₁ being Subset of Niemytzki-plane st b₁ = y=0-line holds
Der b₁ is empty

proof end;

theorem Th46: :: TOPGEN_5:46

for b₁ being Subset of y=0-line holds b₁ is closed Subset of Niemytzki-plane

proof end;

theorem Th47: :: TOPGEN_5:47

RAT is dense Subset of Sorgenfrey-line

proof end;

theorem Th48: :: TOPGEN_5:48

Sorgenfrey-line is separable

proof end;

theorem Th49: :: TOPGEN_5:49

Niemytzki-plane is separable

proof end;

theorem Th50: :: TOPGEN_5:50

Niemytzki-plane is_T1

proof end;

theorem Th51: :: TOPGEN_5:51

not Niemytzki-plane is being_T4

proof end;

definition

let c₁ be TopSpace;
attr a₁ is Tychonoff means :Def4: :: TOPGEN_5:def 4
( a₁ is_T1 & ( for b₁ being closed Subset of a₁
for b₂ being Point of a₁ st b₂ in b₁ ` holds
ex b₃ being continuous Function of a₁,I[01] st
( b₃ . b₂ = 0 & b₃ .: b₁ c= {1} ) ) );

end;

:: deftheorem Def4 defines Tychonoff TOPGEN_5:def 4 :

registration

cluster Tychonoff -> being_T1 being_T3 TopStruct ;
coherence

proof end;

cluster non empty being_T1 being_T4 -> non empty Tychonoff TopStruct ;
coherence

proof end;

end;

theorem Th52: :: TOPGEN_5:52

for b₁ being being_T1 TopSpace st b₁ is Tychonoff holds
for b₂ being prebasis of b₁
for b₃ being Point of b₁
for b₄ being Subset of b₁ st b₃ in b₄ & b₄ in b₂ holds
ex b₅ being continuous Function of b₁,I[01] st
( b₅ . b₃ = 0 & b₅ .: (b₄ ` ) c= {1} )

proof end;

registration

let c₁ be set ;
let c₂ be non empty real-membered set ;
cluster -> real-yielding Relation of a₁,a₂;
coherence ;

end;

theorem Th53: :: TOPGEN_5:53

for b₁ being TopSpace
for b₂ being non empty SubSpace of R^1
for b₃, b₄ being continuous Function of b₁,b₂
for b₅ being Subset of b₁ st ( for b₆ being Point of b₁ holds
( b₆ in b₅ iff b₃ . b₆ <= b₄ . b₆ ) ) holds
b₅ is closed

proof end;

theorem Th54: :: TOPGEN_5:54

for b₁ being TopSpace
for b₂ being non empty SubSpace of R^1
for b₃, b₄ being continuous Function of b₁,b₂ ex b₅ being continuous Function of b₁,b₂ st
for b₆ being Point of b₁ holds b₅ . b₆ = max (b₃ . b₆),(b₄ . b₆)

proof end;

theorem Th55: :: TOPGEN_5:55

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of R^1
for b₃ being non empty finite set
for b₄ being ManySortedFunction of b₃ st ( for b₅ being set st b₅ in b₃ holds
b₄ . b₅ is continuous Function of b₁,b₂ ) holds
ex b₅ being continuous Function of b₁,b₂ st
for b₆ being Point of b₁
for b₇ being non empty finite Subset of REAL st b₇ = rng ((commute b₄) . b₆) holds
b₅ . b₆ = max b₇

proof end;

theorem Th56: :: TOPGEN_5:56

for b₁ being non empty being_T1 TopSpace
for b₂ being prebasis of b₁ st ( for b₃ being Point of b₁
for b₄ being Subset of b₁ st b₃ in b₄ & b₄ in b₂ holds
ex b₅ being continuous Function of b₁,I[01] st
( b₅ . b₃ = 0 & b₅ .: (b₄ ` ) c= {1} ) ) holds
b₁ is Tychonoff

proof end;

theorem Th57: :: TOPGEN_5:57

Sorgenfrey-line is_T1

proof end;

theorem Th58: :: TOPGEN_5:58

for b₁ being real number holds left_open_halfline b₁ is closed Subset of Sorgenfrey-line

proof end;

theorem Th59: :: TOPGEN_5:59

for b₁ being real number holds left_closed_halfline b₁ is closed Subset of Sorgenfrey-line

proof end;

theorem Th60: :: TOPGEN_5:60

for b₁ being real number holds right_closed_halfline b₁ is closed Subset of Sorgenfrey-line

proof end;

theorem Th61: :: TOPGEN_5:61

for b₁, b₂ being real number holds [.b₁,b₂.[ is closed Subset of Sorgenfrey-line

proof end;

theorem Th62: :: TOPGEN_5:62

for b₁ being real number
for b₂ being rational number st b₁ < b₂ holds
ex b₃ being continuous Function of Sorgenfrey-line ,I[01] st
for b₄ being Point of Sorgenfrey-line holds
( ( b₄ in [.b₁,b₂.[ implies b₃ . b₄ = 0 ) & ( not b₄ in [.b₁,b₂.[ implies b₃ . b₄ = 1 ) )

proof end;

theorem Th63: :: TOPGEN_5:63

Sorgenfrey-line is Tychonoff

proof end;

definition

let c₁ be real number ;
let c₂ be real positive number ;
func + c₁,c₂ -> Function of Niemytzki-plane ,I[01] means :Def5: :: TOPGEN_5:def 5
( a₃ . |[a₁,0]| = 0 & ( for b₁ being real number
for b₂ being real non negative number holds
( ( ( b₁ <> a₁ or b₂ <> 0 ) & not |[b₁,b₂]| in Ball |[a₁,a₂]|,a₂ implies a₃ . |[b₁,b₂]| = 1 ) & ( |[b₁,b₂]| in Ball |[a₁,a₂]|,a₂ implies a₃ . |[b₁,b₂]| = (|.(|[a₁,0]| - |[b₁,b₂]|).| ^2 ) / ((2 * a₂) * b₂) ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines + TOPGEN_5:def 5 :

theorem Th64: :: TOPGEN_5:64

for b₁ being Point of (TOP-REAL 2) st b₁ `2 >= 0 holds
for b₂ being real number
for b₃ being real positive number st (+ b₂,b₃) . b₁ = 0 holds
b₁ = |[b₂,0]|

proof end;

theorem Th65: :: TOPGEN_5:65

for b₁, b₂ being real number
for b₃ being real positive number st b₁ <> b₂ holds
(+ b₁,b₃) . |[b₂,0]| = 1

proof end;

theorem Th66: :: TOPGEN_5:66

for b₁ being Point of (TOP-REAL 2)
for b₂ being real number
for b₃, b₄ being real positive number st b₃ <= 1 & |.(b₁ - |[b₂,(b₄ * b₃)]|).| = b₄ * b₃ & b₁ `2 <> 0 holds
(+ b₂,b₄) . b₁ = b₃

proof end;

theorem Th67: :: TOPGEN_5:67

for b₁ being Point of (TOP-REAL 2)
for b₂, b₃ being real number
for b₄ being real positive number st 0 <= b₃ & b₃ <= 1 & |.(b₁ - |[b₂,(b₄ * b₃)]|).| < b₄ * b₃ holds
(+ b₂,b₄) . b₁ < b₃

proof end;

theorem Th68: :: TOPGEN_5:68

for b₁ being Point of (TOP-REAL 2) st b₁ `2 >= 0 holds
for b₂, b₃ being real number
for b₄ being real positive number st 0 <= b₃ & b₃ < 1 & |.(b₁ - |[b₂,(b₄ * b₃)]|).| > b₄ * b₃ holds
(+ b₂,b₄) . b₁ > b₃

proof end;

theorem Th69: :: TOPGEN_5:69

for b₁ being Point of (TOP-REAL 2) st b₁ `2 >= 0 holds
for b₂, b₃, b₄ being real number
for b₅ being real positive number st 0 <= b₃ & b₄ <= 1 & (+ b₂,b₅) . b₁ in ].b₃,b₄.[ holds
ex b₆ being real positive number st
( b₆ <= b₁ `2 & Ball b₁,b₆ c= (+ b₂,b₅) " ].b₃,b₄.[ )

proof end;

theorem Th70: :: TOPGEN_5:70

for b₁ being real number
for b₂, b₃ being real positive number holds Ball |[b₁,(b₃ * b₂)]|,(b₃ * b₂) c= (+ b₁,b₃) " ].0,b₂.[

proof end;

theorem Th71: :: TOPGEN_5:71

for b₁ being real number
for b₂, b₃ being real positive number holds (Ball |[b₁,(b₃ * b₂)]|,(b₃ * b₂)) \/ {|[b₁,0]|} c= (+ b₁,b₃) " [.0,b₂.[

proof end;

theorem Th72: :: TOPGEN_5:72

for b₁ being Point of (TOP-REAL 2) st b₁ `2 >= 0 holds
for b₂, b₃ being real number
for b₄ being real positive number st 0 < (+ b₂,b₄) . b₁ & (+ b₂,b₄) . b₁ < b₃ & b₃ <= 1 holds
b₁ in Ball |[b₂,(b₄ * b₃)]|,(b₄ * b₃)

proof end;

theorem Th73: :: TOPGEN_5:73

for b₁ being Point of (TOP-REAL 2) st b₁ `2 > 0 holds
for b₂, b₃ being real number
for b₄ being real positive number st 0 <= b₃ & b₃ < (+ b₂,b₄) . b₁ holds
ex b₅ being real positive number st
( b₅ <= b₁ `2 & Ball b₁,b₅ c= (+ b₂,b₄) " ].b₃,1.] )

proof end;

theorem Th74: :: TOPGEN_5:74

for b₁ being Point of (TOP-REAL 2) st b₁ `2 = 0 holds
for b₂ being real number
for b₃ being real positive number st (+ b₂,b₃) . b₁ = 1 holds
ex b₄ being real positive number st (Ball |[(b₁ `1 ),b₄]|,b₄) \/ {b₁} c= (+ b₂,b₃) " {1}

proof end;

theorem Th75: :: TOPGEN_5:75

for b₁ being non empty TopSpace
for b₂ being SubSpace of b₁
for b₃ being Basis of b₁ holds { (b₄ /\ ([#] b₂)) where B is Subset of b₁ : ( b₄ in b₃ & b₄ meets [#] b₂ ) } is Basis of b₂

proof end;

theorem Th76: :: TOPGEN_5:76

{ ].b₁,b₂.[ where B is Real, B is Real : b₁ < b₂ } is Basis of R^1

proof end;

theorem Th77: :: TOPGEN_5:77

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being set st b₂ in b₄ & b₃ in b₄ & b₄ \/ {(b₂ \/ b₃)} is Basis of b₁ holds
b₄ is Basis of b₁

proof end;

theorem Th78: :: TOPGEN_5:78

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

proof end;

theorem Th79: :: TOPGEN_5:79

for b₁ being non empty TopSpace
for b₂ being Function of b₁,I[01] holds
( b₂ is continuous iff for b₃, b₄ being real number st 0 <= b₃ & b₃ < 1 & 0 < b₄ & b₄ <= 1 holds
( b₂ " [.0,b₄.[ is open & b₂ " ].b₃,1.] is open ) )

proof end;

registration

let c₁ be real number ;
let c₂ be real positive number ;
cluster + a₁,a₂ -> continuous real-yielding ;
coherence

proof end;

end;

theorem Th80: :: TOPGEN_5:80

for b₁ being Subset of Niemytzki-plane
for b₂ being Element of REAL
for b₃ being real positive number st b₁ = (Ball |[b₂,b₃]|,b₃) \/ {|[b₂,0]|} holds
ex b₄ being continuous Function of Niemytzki-plane ,I[01] st
( b₄ . |[b₂,0]| = 0 & ( for b₅, b₆ being real number holds
( ( |[b₅,b₆]| in b₁ ` implies b₄ . |[b₅,b₆]| = 1 ) & ( |[b₅,b₆]| in b₁ \ {|[b₂,0]|} implies b₄ . |[b₅,b₆]| = (|.(|[b₂,0]| - |[b₅,b₆]|).| ^2 ) / ((2 * b₃) * b₆) ) ) ) )

proof end;

definition

let c₁, c₂ be real number ;
let c₃ be real positive number ;
func + c₁,c₂,c₃ -> Function of Niemytzki-plane ,I[01] means :Def6: :: TOPGEN_5:def 6
for b₁ being real number
for b₂ being real non negative number holds
( ( not |[b₁,b₂]| in Ball |[a₁,a₂]|,a₃ implies a₄ . |[b₁,b₂]| = 1 ) & ( |[b₁,b₂]| in Ball |[a₁,a₂]|,a₃ implies a₄ . |[b₁,b₂]| = |.(|[a₁,a₂]| - |[b₁,b₂]|).| / a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines + TOPGEN_5:def 6 :

theorem Th81: :: TOPGEN_5:81

for b₁ being Point of (TOP-REAL 2) st b₁ `2 >= 0 holds
for b₂ being real number
for b₃ being real non negative number
for b₄ being real positive number holds
( (+ b₂,b₃,b₄) . b₁ = 0 iff b₁ = |[b₂,b₃]| )

proof end;

theorem Th82: :: TOPGEN_5:82

for b₁ being real number
for b₂ being real non negative number
for b₃, b₄ being real positive number st b₄ <= 1 holds
(+ b₁,b₂,b₃) " [.0,b₄.[ = (Ball |[b₁,b₂]|,(b₃ * b₄)) /\ y>=0-plane

proof end;

theorem Th83: :: TOPGEN_5:83

for b₁ being Point of (TOP-REAL 2) st b₁ `2 > 0 holds
for b₂ being real number
for b₃ being real non negative number
for b₄, b₅ being real positive number st (+ b₂,b₄,b₅) . b₁ > b₃ holds
( |.(|[b₂,b₄]| - b₁).| > b₅ * b₃ & (Ball b₁,(|.(|[b₂,b₄]| - b₁).| - (b₅ * b₃))) /\ y>=0-plane c= (+ b₂,b₄,b₅) " ].b₃,1.] )

proof end;

theorem Th84: :: TOPGEN_5:84

for b₁ being Point of (TOP-REAL 2) st b₁ `2 = 0 holds
for b₂ being real number
for b₃ being real non negative number
for b₄, b₅ being real positive number st (+ b₂,b₄,b₅) . b₁ > b₃ holds
( |.(|[b₂,b₄]| - b₁).| > b₅ * b₃ & ex b₆ being real positive number st
( b₆ = (|.(|[b₂,b₄]| - b₁).| - (b₅ * b₃)) / 2 & (Ball |[(b₁ `1 ),b₆]|,b₆) \/ {b₁} c= (+ b₂,b₄,b₅) " ].b₃,1.] ) )

proof end;

registration

let c₁ be real number ;
let c₂, c₃ be real positive number ;
cluster + a₁,a₂,a₃ -> continuous real-yielding ;
coherence

proof end;

end;

theorem Th85: :: TOPGEN_5:85

for b₁ being Subset of Niemytzki-plane
for b₂, b₃ being Element of REAL
for b₄ being real positive number st b₃ > 0 & b₁ = (Ball |[b₂,b₃]|,b₄) /\ y>=0-plane holds
ex b₅ being continuous Function of Niemytzki-plane ,I[01] st
( b₅ . |[b₂,b₃]| = 0 & ( for b₆, b₇ being real number holds
( ( |[b₆,b₇]| in b₁ ` implies b₅ . |[b₆,b₇]| = 1 ) & ( |[b₆,b₇]| in b₁ implies b₅ . |[b₆,b₇]| = |.(|[b₂,b₃]| - |[b₆,b₇]|).| / b₄ ) ) ) )

proof end;

theorem Th86: :: TOPGEN_5:86

Niemytzki-plane is_T1

proof end;

theorem Th87: :: TOPGEN_5:87

Niemytzki-plane is Tychonoff

proof end;