:: YELLOW14 semantic presentation

theorem Th1: :: YELLOW14:1

bool 1 = {0,1} by CARD_5:1, ZFMISC_1:30;

theorem Th2: :: YELLOW14:2

for b₁ being set
for b₂ being Subset of b₁ holds rng ((id b₁) | b₂) = b₂

proof end;

theorem Th3: :: YELLOW14:3

for b₁ being Function
for b₂, b₃ being set holds (b₁ +* (b₂ .--> b₃)) . b₂ = b₃

proof end;

registration

cluster empty strict RelStr ;
existence

proof end;

end;

theorem Th4: :: YELLOW14:4

for b₁ being empty 1-sorted
for b₂ being 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ holds
b₂ is empty

proof end;

theorem Th5: :: YELLOW14:5

for b₁ being 1-sorted
for b₂ being empty 1-sorted
for b₃ being Function of b₁,b₂ st dom b₃ = [#] b₁ holds
b₁ is empty

proof end;

theorem Th6: :: YELLOW14:6

for b₁ being non empty 1-sorted
for b₂ being 1-sorted
for b₃ being Function of b₁,b₂ st dom b₃ = [#] b₁ holds
not b₂ is empty

proof end;

theorem Th7: :: YELLOW14:7

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ holds
not b₁ is empty

proof end;

definition

let c₁ be non empty reflexive RelStr ;
let c₂ be non empty RelStr ;
let c₃ be Function of c₁,c₂;
redefine attr a₃ is directed-sups-preserving means :: YELLOW14:def 1
for b₁ being non empty directed Subset of a₁ holds a₃ preserves_sup_of b₁;
compatibility

proof end;

end;

:: deftheorem Def1 defines directed-sups-preserving YELLOW14:def 1 :

definition

let c₁ be 1-sorted ;
let c₂ be NetStr of c₁;
attr a₂ is Function-yielding means :Def2: :: YELLOW14:def 2
the mapping of a₂ is Function-yielding;

end;

:: deftheorem Def2 defines Function-yielding YELLOW14:def 2 :

registration

cluster strict non empty constituted-Functions 1-sorted ;
existence

proof end;

end;

registration

cluster non empty strict constituted-Functions RelStr ;
existence

proof end;

end;

registration

let c₁ be constituted-Functions 1-sorted ;
cluster -> Function-yielding NetStr of a₁;
coherence

proof end;

end;

registration

let c₁ be constituted-Functions 1-sorted ;
cluster strict Function-yielding NetStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty constituted-Functions 1-sorted ;
cluster non empty strict Function-yielding NetStr of a₁;
existence

proof end;

end;

registration

let c₁ be constituted-Functions 1-sorted ;
let c₂ be Function-yielding NetStr of c₁;
cluster the mapping of a₂ -> Function-yielding ;
coherence by Def2;

end;

registration

let c₁ be non empty constituted-Functions 1-sorted ;
cluster strict Function-yielding NetStr of a₁;
existence

proof end;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
cluster rng the mapping of a₂ -> non empty ;
coherence ;

end;

registration

let c₁ be non empty 1-sorted ;
let c₂ be non empty NetStr of c₁;
cluster rng (netmap a₂,a₁) -> non empty ;
coherence ;

end;

theorem Th8: :: YELLOW14:8

for b₁, b₂, b₃ being non empty RelStr
for b₄ being Function of b₂,b₃
for b₅, b₆ being Function of b₁,b₂ st b₅ <= b₆ & b₄ is monotone holds
b₄ * b₅ <= b₄ * b₆

proof end;

theorem Th9: :: YELLOW14:9

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

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty RelStr ;
let c₃ be Element of (c₂ |^ c₁);
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

theorem Th10: :: YELLOW14:10

for b₁, b₂ being RelStr
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
b₃ is onto

proof end;

registration

let c₁, c₂ be RelStr ;
cluster isomorphic -> onto Relation of the carrier of a₁,the carrier of a₂;
coherence by Th10;

end;

theorem Th11: :: YELLOW14:11

for b₁, b₂ being non empty RelStr
for b₃ being Function of b₁,b₂ st b₃ is isomorphic holds
b₃ /" is isomorphic

proof end;

theorem Th12: :: YELLOW14:12

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is with_infima holds
b₂ is with_infima

proof end;

theorem Th13: :: YELLOW14:13

for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic & b₁ is with_suprema holds
b₂ is with_suprema

proof end;

theorem Th14: :: YELLOW14:14

for b₁ being RelStr st b₁ is empty holds
b₁ is bounded

proof end;

registration

cluster empty -> bounded RelStr ;
coherence by Th14;

end;

theorem Th15: :: YELLOW14:15

for b₁, b₂ being RelStr st b₁,b₂ are_isomorphic & b₁ is lower-bounded holds
b₂ is lower-bounded

proof end;

theorem Th16: :: YELLOW14:16

for b₁, b₂ being RelStr st b₁,b₂ are_isomorphic & b₁ is upper-bounded holds
b₂ is upper-bounded

proof end;

theorem Th17: :: YELLOW14:17

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ st b₄ is isomorphic & ex_sup_of b₃,b₁ holds
ex_sup_of b₄ .: b₃,b₂

proof end;

theorem Th18: :: YELLOW14:18

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Function of b₁,b₂ st b₄ is isomorphic & ex_inf_of b₃,b₁ holds
ex_inf_of b₄ .: b₃,b₂

proof end;

theorem Th19: :: YELLOW14:19

for b₁, b₂ being TopStruct st ( b₁,b₂ are_homeomorphic or ex b₃ being Function of b₁,b₂ st
( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ ) ) holds
( b₁ is empty iff b₂ is empty )

proof end;

theorem Th20: :: YELLOW14:20

for b₁ being non empty TopSpace holds b₁, TopStruct(# the carrier of b₁,the topology of b₁ #) are_homeomorphic

proof end;

registration

let c₁ be non empty reflexive Scott TopRelStr ;
cluster open -> upper inaccessible Element of bool the carrier of a₁;
coherence by WAYBEL11:def 4;
cluster upper inaccessible -> open Element of bool the carrier of a₁;
coherence by WAYBEL11:def 4;

end;

theorem Th21: :: YELLOW14:21

for b₁ being TopStruct
for b₂, b₃ being Point of b₁
for b₄, b₅ being Subset of b₁ st b₄ = {b₂} & Cl b₄ c= Cl b₅ holds
b₂ in Cl b₅

proof end;

theorem Th22: :: YELLOW14:22

for b₁ being TopStruct
for b₂, b₃ being Point of b₁
for b₄, b₅ being Subset of b₁ st b₄ = {b₃} & b₂ in Cl b₄ & b₅ is open & b₂ in b₅ holds
b₃ in b₅

proof end;

theorem Th23: :: YELLOW14:23

for b₁ being TopStruct
for b₂, b₃ being Point of b₁
for b₄, b₅ being Subset of b₁ st b₄ = {b₂} & b₅ = {b₃} & ( for b₆ being Subset of b₁ st b₆ is open & b₂ in b₆ holds
b₃ in b₆ ) holds
Cl b₄ c= Cl b₅

proof end;

theorem Th24: :: YELLOW14:24

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

proof end;

theorem Th25: :: YELLOW14:25

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being Subset of b₁
for b₆ being Subset of b₂ st b₃ = b₄ & b₅ = b₆ & TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ is_dense_point_of b₅ holds
b₄ is_dense_point_of b₆

proof end;

theorem Th26: :: YELLOW14:26

for b₁, b₂ being TopStruct
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ & TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₃ is compact holds
b₄ is compact

proof end;

theorem Th27: :: YELLOW14:27

for b₁, b₂ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is sober holds
b₂ is sober

proof end;

theorem Th28: :: YELLOW14:28

for b₁, b₂ being non empty TopSpace st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is locally-compact holds
b₂ is locally-compact

proof end;

theorem Th29: :: YELLOW14:29

for b₁, b₂ being TopStruct st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & b₁ is compact holds
b₂ is compact

proof end;

definition

let c₁ be non empty set ;
let c₂ be non empty TopSpace;
let c₃ be Point of (product (c₁ --> c₂));
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> Element of a₂;
coherence

proof end;

end;

theorem Th30: :: YELLOW14:30

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁
for b₃, b₄ being Point of (product b₂) holds
( b₃ in Cl {b₄} iff for b₅ being Element of b₁ holds b₃ . b₅ in Cl {(b₄ . b₅)} )

proof end;

theorem Th31: :: YELLOW14:31

for b₁ being non empty set
for b₂ being non empty TopSpace
for b₃, b₄ being Point of (product (b₁ --> b₂)) holds
( b₃ in Cl {b₄} iff for b₅ being Element of b₁ holds b₃ . b₅ in Cl {(b₄ . b₅)} )

proof end;

theorem Th32: :: YELLOW14:32

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non-Empty TopSpace-yielding ManySortedSet of b₁
for b₄ being Point of (product b₃) holds pi (Cl {b₄}),b₂ = Cl {(b₄ . b₂)}

proof end;

theorem Th33: :: YELLOW14:33

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty TopSpace
for b₄ being Point of (product (b₁ --> b₃)) holds pi (Cl {b₄}),b₂ = Cl {(b₄ . b₂)}

proof end;

theorem Th34: :: YELLOW14:34

for b₁, b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂
for b₄ being Function of b₂,b₁ st b₃ = id b₁ & b₄ = id b₁ & b₃ is continuous & b₄ is continuous holds
TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #)

proof end;

theorem Th35: :: YELLOW14:35

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

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
cluster incl a₂ -> continuous ;
coherence by TMAP_1:98;

end;

theorem Th36: :: YELLOW14:36

for b₁ being non empty TopSpace
for b₂ being Function of b₁,b₁ st b₂ * b₂ = b₂ holds
(corestr b₂) * (incl (Image b₂)) = id (Image b₂)

proof end;

theorem Th37: :: YELLOW14:37

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁ holds corestr (incl b₂) is_homeomorphism

proof end;

theorem Th38: :: YELLOW14:38

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds b₂ . b₃ is T_0 TopSpace ) holds
product b₂ is T_0

proof end;

registration

let c₁ be non empty set ;
let c₂ be non empty T_0 TopSpace;
cluster product (a₁ --> a₂) -> T_0 ;
coherence

proof end;

end;

theorem Th39: :: YELLOW14:39

for b₁ being non empty set
for b₂ being non-Empty TopSpace-yielding ManySortedSet of b₁ st ( for b₃ being Element of b₁ holds
( b₂ . b₃ is being_T1 & b₂ . b₃ is TopSpace-like ) ) holds
product b₂ is_T1

proof end;

registration

let c₁ be non empty set ;
let c₂ be non empty being_T1 TopSpace;
cluster product (a₁ --> a₂) -> being_T1 ;
coherence

proof end;

end;