:: WAYBEL26 semantic presentation

notation

let c₁ be set ;
let c₂ be RelStr-yielding ManySortedSet of c₁;
synonym c₁ -POS_prod c₂ for product c₂;

end;

registration

let c₁ be set ;
let c₂ be RelStr-yielding non-Empty ManySortedSet of c₁;
cluster a₁ -POS_prod a₂ -> constituted-Functions ;
coherence ;

end;

notation

let c₁ be set ;
let c₂ be non-Empty TopSpace-yielding ManySortedSet of c₁;
synonym c₁ -TOP_prod c₂ for product c₂;

end;

definition

let c₁, c₂ be non empty TopSpace;
func oContMaps c₁,c₂ -> non empty strict RelStr equals :: WAYBEL26:def 1
ContMaps a₁,(Omega a₂);
coherence ;

end;

:: deftheorem Def1 defines oContMaps WAYBEL26:def 1 :

registration

let c₁, c₂ be non empty TopSpace;
cluster oContMaps a₁,a₂ -> non empty strict reflexive transitive constituted-Functions ;
coherence ;

end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty T_0 TopSpace;
cluster oContMaps a₁,a₂ -> non empty strict reflexive transitive antisymmetric constituted-Functions ;
coherence ;

end;

theorem Th1: :: WAYBEL26:1

for b₁, b₂ being non empty TopSpace
for b₃ being set holds
( b₃ is Element of (oContMaps b₁,b₂) iff b₃ is continuous Function of b₁,(Omega b₂) )

proof end;

theorem Th2: :: WAYBEL26:2

for b₁, b₂ being non empty TopSpace
for b₃ being set holds
( b₃ is Element of (oContMaps b₁,b₂) iff b₃ is continuous Function of b₁,b₂ )

proof end;

theorem Th3: :: WAYBEL26:3

for b₁, b₂ being non empty TopSpace
for b₃, b₄ being Element of (oContMaps b₁,b₂)
for b₅, b₆ being Function of b₁,(Omega b₂) st b₃ = b₅ & b₄ = b₆ holds
( b₃ <= b₄ iff b₅ <= b₆ )

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Point of c₁;
let c₄ be Subset of (oContMaps c₁,c₂);
redefine func pi as pi c₄,c₃ -> Subset of (Omega a₂);
coherence

proof end;

end;

registration

let c₁, c₂ be non empty TopSpace;
let c₃ be set ;
let c₄ be non empty Subset of (oContMaps c₁,c₂);
cluster pi a₄,a₃ -> non empty ;
coherence

proof end;

end;

theorem Th4: :: WAYBEL26:4

Omega Sierpinski_Space is TopAugmentation of BoolePoset 1

proof end;

theorem Th5: :: WAYBEL26:5

for b₁ being non empty TopSpace ex b₂ being Function of (InclPoset the topology of b₁),(oContMaps b₁,Sierpinski_Space ) st
( b₂ is isomorphic & ( for b₃ being open Subset of b₁ holds b₂ . b₃ = chi b₃,the carrier of b₁ ) )

proof end;

theorem Th6: :: WAYBEL26:6

for b₁ being non empty TopSpace holds InclPoset the topology of b₁, oContMaps b₁,Sierpinski_Space are_isomorphic

proof end;

definition

let c₁, c₂, c₃ be non empty TopSpace;
let c₄ be continuous Function of c₂,c₃;
func oContMaps c₁,c₄ -> Function of (oContMaps a₁,a₂),(oContMaps a₁,a₃) means :Def2: :: WAYBEL26:def 2
for b₁ being continuous Function of a₁,a₂ holds a₅ . b₁ = a₄ * b₁;
uniqueness

proof end;

existence

proof end;

func oContMaps c₄,c₁ -> Function of (oContMaps a₃,a₁),(oContMaps a₂,a₁) means :Def3: :: WAYBEL26:def 3
for b₁ being continuous Function of a₃,a₁ holds a₅ . b₁ = b₁ * a₄;
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def2 defines oContMaps WAYBEL26:def 2 :

:: deftheorem Def3 defines oContMaps WAYBEL26:def 3 :

theorem Th7: :: WAYBEL26:7

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace holds oContMaps b₁,b₂ is directed-sups-inheriting SubRelStr of (Omega b₂) |^ the carrier of b₁ by WAYBEL25:43;

theorem Th8: :: WAYBEL26:8

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace holds oContMaps b₁,b₂ is up-complete

proof end;

theorem Th9: :: WAYBEL26:9

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₂,b₃ holds oContMaps b₁,b₄ is monotone

proof end;

theorem Th10: :: WAYBEL26:10

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₂,b₂ st b₃ is idempotent holds
oContMaps b₁,b₃ is idempotent

proof end;

theorem Th11: :: WAYBEL26:11

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₂,b₃ holds oContMaps b₄,b₁ is monotone

proof end;

theorem Th12: :: WAYBEL26:12

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₂,b₂ st b₃ is idempotent holds
oContMaps b₃,b₁ is idempotent

proof end;

theorem Th13: :: WAYBEL26:13

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₂,b₃
for b₅ being Element of b₁
for b₆ being Subset of (oContMaps b₁,b₂) holds pi ((oContMaps b₁,b₄) .: b₆),b₅ = b₄ .: (pi b₆,b₅)

proof end;

theorem Th14: :: WAYBEL26:14

for b₁ being non empty TopSpace
for b₂, b₃ being monotone-convergence T_0-TopSpace
for b₄ being continuous Function of b₂,b₃ holds oContMaps b₁,b₄ is directed-sups-preserving

proof end;

theorem Th15: :: WAYBEL26:15

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₂,b₃
for b₅ being Element of b₂
for b₆ being Subset of (oContMaps b₃,b₁) holds pi ((oContMaps b₄,b₁) .: b₆),b₅ = pi b₆,(b₄ . b₅)

proof end;

theorem Th16: :: WAYBEL26:16

for b₁, b₂ being non empty TopSpace
for b₃ being monotone-convergence T_0-TopSpace
for b₄ being continuous Function of b₁,b₂ holds oContMaps b₄,b₃ is directed-sups-preserving

proof end;

theorem Th17: :: WAYBEL26:17

for b₁, b₂ being non empty TopSpace
for b₃ being non empty SubSpace of b₂ holds oContMaps b₁,b₃ is full SubRelStr of oContMaps b₁,b₂

proof end;

theorem Th18: :: WAYBEL26:18

for b₁ being monotone-convergence T_0-TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
Omega b₂ is directed-sups-inheriting SubRelStr of Omega b₁

proof end;

Lemma20: for b₁ being monotone-convergence T_0-TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being continuous Function of b₁,b₂ st b₃ is_a_retraction holds
b₂ is monotone-convergence

proof end;

theorem Th19: :: WAYBEL26:19

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace
for b₃ being non empty SubSpace of b₂
for b₄ being continuous Function of b₂,b₃ st b₄ is_a_retraction holds
oContMaps b₁,b₄ is_a_retraction_of oContMaps b₁,b₂, oContMaps b₁,b₃

proof end;

theorem Th20: :: WAYBEL26:20

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace
for b₃ being non empty SubSpace of b₂ st b₃ is_a_retract_of b₂ holds
oContMaps b₁,b₃ is_a_retract_of oContMaps b₁,b₂

proof end;

theorem Th21: :: WAYBEL26:21

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₂,b₃ st b₄ is_homeomorphism holds
oContMaps b₁,b₄ is isomorphic

proof end;

theorem Th22: :: WAYBEL26:22

for b₁, b₂, b₃ being non empty TopSpace st b₂,b₃ are_homeomorphic holds
oContMaps b₁,b₂, oContMaps b₁,b₃ are_isomorphic

proof end;

theorem Th23: :: WAYBEL26:23

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace
for b₃ being non empty SubSpace of b₂ st b₃ is_a_retract_of b₂ & oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous holds
( oContMaps b₁,b₃ is complete & oContMaps b₁,b₃ is continuous )

proof end;

theorem Th24: :: WAYBEL26:24

for b₁ being non empty TopSpace
for b₂, b₃ being monotone-convergence T_0-TopSpace st b₂ is_Retract_of b₃ & oContMaps b₁,b₃ is complete & oContMaps b₁,b₃ is continuous holds
( oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous )

proof end;

theorem Th25: :: WAYBEL26:25

for b₁ being non trivial T_0-TopSpace st not b₁ is_T1 holds
Sierpinski_Space is_Retract_of b₁

proof end;

theorem Th26: :: WAYBEL26:26

for b₁ being non empty TopSpace
for b₂ being non trivial T_0-TopSpace st oContMaps b₁,b₂ is with_suprema holds
not b₂ is_T1

proof end;

registration

cluster Sierpinski_Space -> non trivial monotone-convergence ;
coherence

proof end;

end;

registration

cluster non trivial injective monotone-convergence TopStruct ;
existence

proof end;

end;

theorem Th27: :: WAYBEL26:27

for b₁ being non empty TopSpace
for b₂ being non trivial monotone-convergence T_0-TopSpace st oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous holds
InclPoset the topology of b₁ is continuous

proof end;

theorem Th28: :: WAYBEL26:28

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being monotone-convergence T_0-TopSpace ex b₄ being directed-sups-preserving projection Function of (oContMaps b₁,b₃),(oContMaps b₁,b₃) st
( ( for b₅ being continuous Function of b₁,b₃ holds b₄ . b₅ = b₁ --> (b₅ . b₂) ) & ex b₅ being continuous Function of b₁,b₁ st
( b₅ = b₁ --> b₂ & b₄ = oContMaps b₅,b₃ ) )

proof end;

theorem Th29: :: WAYBEL26:29

for b₁ being non empty TopSpace
for b₂ being monotone-convergence T_0-TopSpace st oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous holds
( Omega b₂ is complete & Omega b₂ is continuous )

proof end;

theorem Th30: :: WAYBEL26:30

for b₁ being non empty 1-sorted
for b₂ being non empty set
for b₃ being non-Empty TopSpace-yielding ManySortedSet of b₂
for b₄ being Function of b₁,(b₂ -TOP_prod b₃)
for b₅ being Element of b₂ holds (commute b₄) . b₅ = (proj b₃,b₅) * b₄

proof end;

theorem Th31: :: WAYBEL26:31

for b₁ being 1-sorted
for b₂ being set holds Carrier (b₂ --> b₁) = b₂ --> the carrier of b₁

proof end;

theorem Th32: :: WAYBEL26:32

for b₁, b₂ being non empty TopSpace
for b₃ being non empty set
for b₄ being continuous Function of b₁,(b₃ -TOP_prod (b₃ --> b₂)) holds commute b₄ is Function of b₃,the carrier of (oContMaps b₁,b₂)

proof end;

theorem Th33: :: WAYBEL26:33

for b₁, b₂ being non empty TopSpace holds the carrier of (oContMaps b₁,b₂) c= Funcs the carrier of b₁,the carrier of b₂

proof end;

theorem Th34: :: WAYBEL26:34

for b₁, b₂ being non empty TopSpace
for b₃ being non empty set
for b₄ being Function of b₃,the carrier of (oContMaps b₁,b₂) holds commute b₄ is continuous Function of b₁,(b₃ -TOP_prod (b₃ --> b₂))

proof end;

theorem Th35: :: WAYBEL26:35

for b₁ being non empty TopSpace
for b₂ being non empty set ex b₃ being Function of (oContMaps b₁,(b₂ -TOP_prod (b₂ --> Sierpinski_Space ))),(b₂ -POS_prod (b₂ --> (oContMaps b₁,Sierpinski_Space ))) st
( b₃ is isomorphic & ( for b₄ being continuous Function of b₁,(b₂ -TOP_prod (b₂ --> Sierpinski_Space )) holds b₃ . b₄ = commute b₄ ) )

proof end;

theorem Th36: :: WAYBEL26:36

for b₁ being non empty TopSpace
for b₂ being non empty set holds oContMaps b₁,(b₂ -TOP_prod (b₂ --> Sierpinski_Space )),b₂ -POS_prod (b₂ --> (oContMaps b₁,Sierpinski_Space )) are_isomorphic

proof end;

theorem Th37: :: WAYBEL26:37

for b₁ being non empty TopSpace st InclPoset the topology of b₁ is continuous holds
for b₂ being injective T_0-TopSpace holds
( oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous )

proof end;

registration

cluster Scott complete non trivial TopRelStr ;
existence

proof end;

end;

theorem Th38: :: WAYBEL26:38

for b₁ being non empty TopSpace
for b₂ being Scott complete non trivial TopLattice holds
( oContMaps b₁,b₂ is complete & oContMaps b₁,b₂ is continuous iff ( InclPoset the topology of b₁ is continuous & b₂ is continuous ) )

proof end;

registration

let c₁ be Function;
cluster Union (disjoin a₁) -> Relation-like ;
coherence

proof end;

end;

definition

let c₁ be Function;
func *graph c₁ -> Relation equals :: WAYBEL26:def 4
(Union (disjoin a₁)) ~ ;
correctness ;

end;

:: deftheorem Def4 defines *graph WAYBEL26:def 4 :

theorem Th39: :: WAYBEL26:39

for b₁, b₂ being set
for b₃ being Function holds
( [b₁,b₂] in *graph b₃ iff ( b₁ in dom b₃ & b₂ in b₃ . b₁ ) )

proof end;

theorem Th40: :: WAYBEL26:40

for b₁ being finite set holds
( proj1 b₁ is finite & proj2 b₁ is finite )

proof end;

theorem Th41: :: WAYBEL26:41

for b₁, b₂ being non empty TopSpace
for b₃ being Scott TopAugmentation of InclPoset the topology of b₂
for b₄ being Function of b₁,b₃ st *graph b₄ is open Subset of [:b₁,b₂:] holds
b₄ is continuous

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
func c₁,c₂ *graph -> Function means :Def5: :: WAYBEL26:def 5
( dom a₃ = a₂ & ( for b₁ being set st b₁ in a₂ holds
a₃ . b₁ = a₁ .: {b₁} ) );
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def5 defines *graph WAYBEL26:def 5 :

theorem Th42: :: WAYBEL26:42

for b₁ being Relation
for b₂ being set st dom b₁ c= b₂ holds
*graph (b₁,b₂ *graph ) = b₁

proof end;

registration

let c₁, c₂ be TopSpace;
cluster -> Relation-like Element of bool the carrier of [:a₁,a₂:];
coherence

proof end;

cluster -> Relation-like Element of the topology of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th43: :: WAYBEL26:43

for b₁, b₂ being non empty TopSpace
for b₃ being open Subset of [:b₁,b₂:]
for b₄ being Point of b₁ holds b₃ .: {b₄} is open Subset of b₂

proof end;

theorem Th44: :: WAYBEL26:44

for b₁, b₂ being non empty TopSpace
for b₃ being Scott TopAugmentation of InclPoset the topology of b₂
for b₄ being open Subset of [:b₁,b₂:] holds b₄,the carrier of b₁ *graph is continuous Function of b₁,b₃

proof end;

theorem Th45: :: WAYBEL26:45

for b₁, b₂ being non empty TopSpace
for b₃ being Scott TopAugmentation of InclPoset the topology of b₂
for b₄, b₅ being open Subset of [:b₁,b₂:] st b₄ c= b₅ holds
for b₆, b₇ being Element of (oContMaps b₁,b₃) st b₆ = b₄,the carrier of b₁ *graph & b₇ = b₅,the carrier of b₁ *graph holds
b₆ <= b₇

proof end;

theorem Th46: :: WAYBEL26:46

for b₁, b₂ being non empty TopSpace
for b₃ being Scott TopAugmentation of InclPoset the topology of b₂ ex b₄ being Function of (InclPoset the topology of [:b₁,b₂:]),(oContMaps b₁,b₃) st
( b₄ is monotone & ( for b₅ being open Subset of [:b₁,b₂:] holds b₄ . b₅ = b₅,the carrier of b₁ *graph ) )

proof end;