:: YELLOW12 semantic presentation

registration

let X be empty set ;
cluster union X -> empty ;
coherence by ZFMISC_1:2;

end;

Lm1: now

let S, T, x1, x2 be set ; :: thesis:
assume A1: ( x1 in S & x2 in T ) ; :: thesis:
A2: dom <:(pr2 S,T),(pr1 S,T):> = (dom (pr2 S,T)) /\ (dom (pr1 S,T)) by FUNCT_3:def 8
.= (dom (pr2 S,T)) /\ [:S,T:] by FUNCT_3:def 5
.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 6
.= [:S,T:] ;
[x1,x2] in [:S,T:] by A1, ZFMISC_1:106;
hence <:(pr2 S,T),(pr1 S,T):> . [x1,x2] = [((pr2 S,T) . [x1,x2]),((pr1 S,T) . [x1,x2])] by A2, FUNCT_3:def 8
.= [x2,((pr1 S,T) . [x1,x2])] by A1, FUNCT_3:def 6
.= [x2,x1] by A1, FUNCT_3:def 5 ;
:: thesis:

end;

theorem :: YELLOW12:1

for X, A being set holds (delta X) .: A c= [:A,A:]

proof end;

theorem Th2: :: YELLOW12:2

for X, A being set holds (delta X) " [:A,A:] c= A

proof end;

theorem :: YELLOW12:3

for X being set
for A being Subset of X holds (delta X) " [:A,A:] = A

proof end;

theorem Th4: :: YELLOW12:4

for X, Y being set holds
( dom <:(pr2 X,Y),(pr1 X,Y):> = [:X,Y:] & rng <:(pr2 X,Y),(pr1 X,Y):> = [:Y,X:] )

proof end;

theorem Th5: :: YELLOW12:5

for X, Y, A, B being set holds <:(pr2 X,Y),(pr1 X,Y):> .: [:A,B:] c= [:B,A:]

proof end;

theorem :: YELLOW12:6

for X, Y being set
for A being Subset of X
for B being Subset of Y holds <:(pr2 X,Y),(pr1 X,Y):> .: [:A,B:] = [:B,A:]

proof end;

theorem Th7: :: YELLOW12:7

for X, Y being set holds <:(pr2 X,Y),(pr1 X,Y):> is one-to-one

proof end;

registration

let X, Y be set ;
cluster <:(pr2 X,Y),(pr1 X,Y):> -> one-to-one ;
coherence by Th7;

end;

theorem Th8: :: YELLOW12:8

for X, Y being set holds <:(pr2 X,Y),(pr1 X,Y):> " = <:(pr2 Y,X),(pr1 Y,X):>

proof end;

theorem Th9: :: YELLOW12:9

for L1 being Semilattice
for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = x1 & y = y1 holds
x "/\" y = x1 "/\" y1

proof end;

theorem Th10: :: YELLOW12:10

for L1 being sup-Semilattice
for L2 being non empty RelStr
for x, y being Element of L1
for x1, y1 being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = x1 & y = y1 holds
x "\/" y = x1 "\/" y1

proof end;

theorem Th11: :: YELLOW12:11

for L1 being Semilattice
for L2 being non empty RelStr
for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "/\" Y = X1 "/\" Y1

proof end;

theorem :: YELLOW12:12

for L1 being sup-Semilattice
for L2 being non empty RelStr
for X, Y being Subset of L1
for X1, Y1 being Subset of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & X = X1 & Y = Y1 holds
X "\/" Y = X1 "\/" Y1

proof end;

theorem Th13: :: YELLOW12:13

for L1 being non empty reflexive antisymmetric up-complete RelStr
for L2 being non empty reflexive RelStr
for x being Element of L1
for y being Element of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & x = y holds
( waybelow x = waybelow y & wayabove x = wayabove y )

proof end;

theorem :: YELLOW12:14

for L1 being meet-continuous Semilattice
for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
L2 is meet-continuous

proof end;

theorem :: YELLOW12:15

for L1 being non empty reflexive antisymmetric continuous RelStr
for L2 being non empty reflexive RelStr st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) holds
L2 is continuous

proof end;

theorem :: YELLOW12:16

for L1, L2 being RelStr
for A being Subset of L1
for J being Subset of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & A = J holds
subrelstr A = subrelstr J

proof end;

theorem :: YELLOW12:17

for L1, L2 being non empty RelStr
for A being SubRelStr of L1
for J being SubRelStr of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & RelStr(# the carrier of A,the InternalRel of A #) = RelStr(# the carrier of J,the InternalRel of J #) & A is meet-inheriting holds
J is meet-inheriting

proof end;

theorem :: YELLOW12:18

proof end;

theorem :: YELLOW12:19

for L1 being non empty reflexive antisymmetric up-complete RelStr
for L2 being non empty reflexive RelStr
for X being Subset of L1
for Y being Subset of L2 st RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) & X = Y & X has_the_property_(S) holds
Y has_the_property_(S)

proof end;

theorem :: YELLOW12:20

proof end;

theorem :: YELLOW12:21

for N being antisymmetric with_infima RelStr
for D, E being Subset of N
for X being upper Subset of N st D misses X holds
D "/\" E misses X

proof end;

theorem :: YELLOW12:22

for R being non empty reflexive RelStr holds id the carrier of R c= the InternalRel of R /\ the InternalRel of (R ~ )

proof end;

theorem :: YELLOW12:23

for R being antisymmetric RelStr holds the InternalRel of R /\ the InternalRel of (R ~ ) c= id the carrier of R

proof end;

theorem Th24: :: YELLOW12:24

for R being upper-bounded Semilattice
for X being Subset of [:R,R:] st ex_inf_of (inf_op R) .: X,R holds
inf_op R preserves_inf_of X

proof end;

registration

let R be complete Semilattice;
cluster inf_op R -> infs-preserving ;
coherence

proof end;

end;

theorem Th25: :: YELLOW12:25

for R being lower-bounded sup-Semilattice
for X being Subset of [:R,R:] st ex_sup_of (sup_op R) .: X,R holds
sup_op R preserves_sup_of X

proof end;

registration

let R be complete sup-Semilattice;
cluster sup_op R -> sups-preserving ;
coherence

proof end;

end;

theorem :: YELLOW12:26

for N being Semilattice
for A being Subset of N st subrelstr A is meet-inheriting holds
A is filtered

proof end;

theorem :: YELLOW12:27

for N being sup-Semilattice
for A being Subset of N st subrelstr A is join-inheriting holds
A is directed

proof end;

theorem :: YELLOW12:28

for N being transitive RelStr
for A, J being Subset of N st A is_coarser_than uparrow J holds
uparrow A c= uparrow J

proof end;

theorem :: YELLOW12:29

for N being transitive RelStr
for A, J being Subset of N st A is_finer_than downarrow J holds
downarrow A c= downarrow J

proof end;

theorem :: YELLOW12:30

for N being non empty reflexive RelStr
for x being Element of N
for X being Subset of N st x in X holds
uparrow x c= uparrow X

proof end;

theorem :: YELLOW12:31

for N being non empty reflexive RelStr
for x being Element of N
for X being Subset of N st x in X holds
downarrow x c= downarrow X

proof end;

registration

let T be non empty TopStruct ;
cluster TopStruct(# the carrier of T,the topology of T #) -> non empty ;
coherence by STRUCT_0:def 1;

end;

registration

let T be TopSpace;
cluster TopStruct(# the carrier of T,the topology of T #) -> TopSpace-like ;
coherence

proof end;

end;

theorem Th32: :: YELLOW12:32

for S, T being TopStruct
for B being Basis of S st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is Basis of T

proof end;

theorem Th33: :: YELLOW12:33

for S, T being TopStruct
for B being prebasis of S st TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is prebasis of T

proof end;

theorem Th34: :: YELLOW12:34

for T being non empty TopSpace
for J being Basis of T holds not J is empty

proof end;

registration

let T be non empty TopSpace;
cluster -> non empty Basis of T;
coherence by Th34;

end;

theorem Th35: :: YELLOW12:35

for T being non empty TopSpace
for x being Point of T
for J being Basis of x holds not J is empty

proof end;

registration

let T be non empty TopSpace;
let x be Point of T;
cluster -> non empty Basis of x;
coherence by Th35;

end;

theorem :: YELLOW12:36

for S1, T1, S2, T2 being TopSpace
for f being Function of S1,S2
for g being Function of T1,T2 st TopStruct(# the carrier of S1,the topology of S1 #) = TopStruct(# the carrier of T1,the topology of T1 #) & TopStruct(# the carrier of S2,the topology of S2 #) = TopStruct(# the carrier of T2,the topology of T2 #) & f = g & f is continuous holds
g is continuous

proof end;

theorem Th37: :: YELLOW12:37

for T being non empty TopSpace holds id the carrier of T = { p where p is Point of [:T,T:] : (pr1 the carrier of T,the carrier of T) . p = (pr2 the carrier of T,the carrier of T) . p }

proof end;

theorem Th38: :: YELLOW12:38

for T being non empty TopSpace holds delta the carrier of T is continuous Function of T,[:T,T:]

proof end;

theorem Th39: :: YELLOW12:39

for S, T being non empty TopSpace holds pr1 the carrier of S,the carrier of T is continuous Function of [:S,T:],S

proof end;

theorem Th40: :: YELLOW12:40

for S, T being non empty TopSpace holds pr2 the carrier of S,the carrier of T is continuous Function of [:S,T:],T

proof end;

theorem Th41: :: YELLOW12:41

for T, S, R being non empty TopSpace
for f being continuous Function of T,S
for g being continuous Function of T,R holds <:f,g:> is continuous Function of T,[:S,R:]

proof end;

theorem Th42: :: YELLOW12:42

for S, T being non empty TopSpace holds <:(pr2 the carrier of S,the carrier of T),(pr1 the carrier of S,the carrier of T):> is continuous Function of [:S,T:],[:T,S:]

proof end;

theorem Th43: :: YELLOW12:43

for S, T being non empty TopSpace
for f being Function of [:S,T:],[:T,S:] st f = <:(pr2 the carrier of S,the carrier of T),(pr1 the carrier of S,the carrier of T):> holds
f is_homeomorphism

proof end;

theorem :: YELLOW12:44

for S, T being non empty TopSpace holds [:S,T:],[:T,S:] are_homeomorphic

proof end;

theorem Th45: :: YELLOW12:45

for S being non empty TopSpace
for T being non empty Hausdorff TopSpace
for f, g being continuous Function of S,T holds
( ( for X being Subset of S st X = { p where p is Point of S : f . p <> g . p } holds
X is open ) & ( for X being Subset of S st X = { p where p is Point of S : f . p = g . p } holds
X is closed ) )

proof end;

theorem :: YELLOW12:46

for T being non empty TopSpace holds
( T is Hausdorff iff for A being Subset of [:T,T:] st A = id the carrier of T holds
A is closed )

proof end;

registration

let S, T be TopStruct ;
cluster strict Refinement of S,T;
existence

proof end;

end;

registration

let S be non empty TopStruct ;
let T be TopStruct ;
cluster non empty strict Refinement of S,T;
existence

proof end;

cluster non empty strict Refinement of T,S;
existence

proof end;

end;

theorem :: YELLOW12:47

for R, S, T being TopStruct holds
( R is Refinement of S,T iff TopStruct(# the carrier of R,the topology of R #) is Refinement of S,T )

proof end;

theorem Th48: :: YELLOW12:48

for S1, S2, T1, T2 being non empty TopSpace
for R being Refinement of [:S1,T1:],[:S2,T2:] st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
{ ([:U1,V1:] /\ [:U2,V2:]) where U1 is Subset of S1, U2 is Subset of S2, V1 is Subset of T1, V2 is Subset of T2 : ( U1 is open & U2 is open & V1 is open & V2 is open ) } is Basis of R

proof end;

theorem Th49: :: YELLOW12:49

for S1, S2, T1, T2 being non empty TopSpace
for R being Refinement of [:S1,T1:],[:S2,T2:]
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
( the carrier of [:R1,R2:] = the carrier of R & the topology of [:R1,R2:] = the topology of R )

proof end;

theorem :: YELLOW12:50

for S1, S2, T1, T2 being non empty TopSpace
for R1 being Refinement of S1,S2
for R2 being Refinement of T1,T2 st the carrier of S1 = the carrier of S2 & the carrier of T1 = the carrier of T2 holds
[:R1,R2:] is Refinement of [:S1,T1:],[:S2,T2:]

proof end;