:: YELLOW12 semantic presentation

registration

let c₁ be empty set ;
cluster union a₁ -> empty ;
coherence by ZFMISC_1:2;

end;

E1: now

let c₁, c₂, c₃, c₄ be set ;
assume E2: ( c₃ in c₁ & c₄ in c₂ ) ;
E3: dom <:(pr2 c₁,c₂),(pr1 c₁,c₂):> = (dom (pr2 c₁,c₂)) /\ (dom (pr1 c₁,c₂)) by FUNCT_3:def 8
.= (dom (pr2 c₁,c₂)) /\ [:c₁,c₂:] by FUNCT_3:def 5
.= [:c₁,c₂:] /\ [:c₁,c₂:] by FUNCT_3:def 6
.= [:c₁,c₂:] ;
[c₃,c₄] in [:c₁,c₂:] by E2, ZFMISC_1:106;
hence <:(pr2 c₁,c₂),(pr1 c₁,c₂):> . [c₃,c₄] = [((pr2 c₁,c₂) . [c₃,c₄]),((pr1 c₁,c₂) . [c₃,c₄])] by E3, FUNCT_3:def 8
.= [c₄,((pr1 c₁,c₂) . [c₃,c₄])] by E2, FUNCT_3:def 6
.= [c₄,c₃] by E2, FUNCT_3:def 5 ;

end;

theorem Th1: :: YELLOW12:1

for b₁, b₂ being set holds (delta b₁) .: b₂ c= [:b₂,b₂:]

proof end;

theorem Th2: :: YELLOW12:2

for b₁, b₂ being set holds (delta b₁) " [:b₂,b₂:] c= b₂

proof end;

theorem Th3: :: YELLOW12:3

for b₁ being set
for b₂ being Subset of b₁ holds (delta b₁) " [:b₂,b₂:] = b₂

proof end;

theorem Th4: :: YELLOW12:4

for b₁, b₂ being set holds
( dom <:(pr2 b₁,b₂),(pr1 b₁,b₂):> = [:b₁,b₂:] & rng <:(pr2 b₁,b₂),(pr1 b₁,b₂):> = [:b₂,b₁:] )

proof end;

theorem Th5: :: YELLOW12:5

for b₁, b₂, b₃, b₄ being set holds <:(pr2 b₁,b₂),(pr1 b₁,b₂):> .: [:b₃,b₄:] c= [:b₄,b₃:]

proof end;

theorem Th6: :: YELLOW12:6

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds <:(pr2 b₁,b₂),(pr1 b₁,b₂):> .: [:b₃,b₄:] = [:b₄,b₃:]

proof end;

theorem Th7: :: YELLOW12:7

for b₁, b₂ being set holds <:(pr2 b₁,b₂),(pr1 b₁,b₂):> is one-to-one

proof end;

registration

let c₁, c₂ be set ;
cluster <:(pr2 a₁,a₂),(pr1 a₁,a₂):> -> one-to-one ;
coherence by Th7;

end;

theorem Th8: :: YELLOW12:8

for b₁, b₂ being set holds <:(pr2 b₁,b₂),(pr1 b₁,b₂):> " = <:(pr2 b₂,b₁),(pr1 b₂,b₁):>

proof end;

theorem Th9: :: YELLOW12:9

for b₁ being Semilattice
for b₂ being non empty RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₅ & b₄ = b₆ holds
b₃ "/\" b₄ = b₅ "/\" b₆

proof end;

theorem Th10: :: YELLOW12:10

for b₁ being sup-Semilattice
for b₂ being non empty RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₅ & b₄ = b₆ holds
b₃ "\/" b₄ = b₅ "\/" b₆

proof end;

theorem Th11: :: YELLOW12:11

for b₁ being Semilattice
for b₂ being non empty RelStr
for b₃, b₄ being Subset of b₁
for b₅, b₆ being Subset of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₅ & b₄ = b₆ holds
b₃ "/\" b₄ = b₅ "/\" b₆

proof end;

theorem Th12: :: YELLOW12:12

for b₁ being sup-Semilattice
for b₂ being non empty RelStr
for b₃, b₄ being Subset of b₁
for b₅, b₆ being Subset of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₅ & b₄ = b₆ holds
b₃ "\/" b₄ = b₅ "\/" b₆

proof end;

theorem Th13: :: YELLOW12:13

for b₁ being non empty reflexive antisymmetric up-complete RelStr
for b₂ being non empty reflexive RelStr
for b₃ being Element of b₁
for b₄ being Element of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₄ holds
( waybelow b₃ = waybelow b₄ & wayabove b₃ = wayabove b₄ )

proof end;

theorem Th14: :: YELLOW12:14

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

proof end;

theorem Th15: :: YELLOW12:15

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

proof end;

theorem Th16: :: YELLOW12:16

for b₁, b₂ being RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₄ holds
subrelstr b₃ = subrelstr b₄

proof end;

theorem Th17: :: YELLOW12:17

for b₁, b₂ being non empty RelStr
for b₃ being SubRelStr of b₁
for b₄ being SubRelStr of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & RelStr(# the carrier of b₃,the InternalRel of b₃ #) = RelStr(# the carrier of b₄,the InternalRel of b₄ #) & b₃ is meet-inheriting holds
b₄ is meet-inheriting

proof end;

theorem Th18: :: YELLOW12:18

proof end;

theorem Th19: :: YELLOW12:19

for b₁ being non empty reflexive antisymmetric up-complete RelStr
for b₂ being non empty reflexive RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₄ & b₃ has_the_property_(S) holds
b₄ has_the_property_(S)

proof end;

theorem Th20: :: YELLOW12:20

for b₁ being non empty reflexive antisymmetric up-complete RelStr
for b₂ being non empty reflexive RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st RelStr(# the carrier of b₁,the InternalRel of b₁ #) = RelStr(# the carrier of b₂,the InternalRel of b₂ #) & b₃ = b₄ & b₃ is closed_under_directed_sups holds
b₄ is closed_under_directed_sups

proof end;

theorem Th21: :: YELLOW12:21

for b₁ being antisymmetric with_infima RelStr
for b₂, b₃ being Subset of b₁
for b₄ being upper Subset of b₁ st b₂ misses b₄ holds
b₂ "/\" b₃ misses b₄

proof end;

theorem Th22: :: YELLOW12:22

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

proof end;

theorem Th23: :: YELLOW12:23

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

proof end;

theorem Th24: :: YELLOW12:24

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

proof end;

registration

let c₁ be complete Semilattice;
cluster inf_op a₁ -> infs-preserving ;
coherence

proof end;

end;

theorem Th25: :: YELLOW12:25

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

proof end;

registration

let c₁ be complete sup-Semilattice;
cluster sup_op a₁ -> sups-preserving ;
coherence

proof end;

end;

theorem Th26: :: YELLOW12:26

for b₁ being Semilattice
for b₂ being Subset of b₁ st subrelstr b₂ is meet-inheriting holds
b₂ is filtered

proof end;

theorem Th27: :: YELLOW12:27

for b₁ being sup-Semilattice
for b₂ being Subset of b₁ st subrelstr b₂ is join-inheriting holds
b₂ is directed

proof end;

theorem Th28: :: YELLOW12:28

for b₁ being transitive RelStr
for b₂, b₃ being Subset of b₁ st b₂ is_coarser_than uparrow b₃ holds
uparrow b₂ c= uparrow b₃

proof end;

theorem Th29: :: YELLOW12:29

for b₁ being transitive RelStr
for b₂, b₃ being Subset of b₁ st b₂ is_finer_than downarrow b₃ holds
downarrow b₂ c= downarrow b₃

proof end;

theorem Th30: :: YELLOW12:30

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₂ in b₃ holds
uparrow b₂ c= uparrow b₃

proof end;

theorem Th31: :: YELLOW12:31

for b₁ being non empty reflexive RelStr
for b₂ being Element of b₁
for b₃ being Subset of b₁ st b₂ in b₃ holds
downarrow b₂ c= downarrow b₃

proof end;

registration

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

end;

registration

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

proof end;

end;

theorem Th32: :: YELLOW12:32

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

proof end;

theorem Th33: :: YELLOW12:33

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

proof end;

theorem Th34: :: YELLOW12:34

for b₁ being non empty TopSpace
for b₂ being Basis of b₁ holds not b₂ is empty

proof end;

registration

let c₁ be non empty TopSpace;
cluster -> non empty Basis of a₁;
coherence by Th34;

end;

theorem Th35: :: YELLOW12:35

for b₁ being non empty TopSpace
for b₂ being Point of b₁
for b₃ being Basis of b₂ holds not b₃ is empty

proof end;

registration

let c₁ be non empty TopSpace;
let c₂ be Point of c₁;
cluster -> non empty Basis of a₂;
coherence by Th35;

end;

theorem Th36: :: YELLOW12:36

for b₁, b₂, b₃, b₄ being TopSpace
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st TopStruct(# the carrier of b₁,the topology of b₁ #) = TopStruct(# the carrier of b₂,the topology of b₂ #) & TopStruct(# the carrier of b₃,the topology of b₃ #) = TopStruct(# the carrier of b₄,the topology of b₄ #) & b₅ = b₆ & b₅ is continuous holds
b₆ is continuous

proof end;

theorem Th37: :: YELLOW12:37

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

proof end;

theorem Th38: :: YELLOW12:38

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

proof end;

theorem Th39: :: YELLOW12:39

for b₁, b₂ being non empty TopSpace holds pr1 the carrier of b₁,the carrier of b₂ is continuous Function of [:b₁,b₂:],b₁

proof end;

theorem Th40: :: YELLOW12:40

for b₁, b₂ being non empty TopSpace holds pr2 the carrier of b₁,the carrier of b₂ is continuous Function of [:b₁,b₂:],b₂

proof end;

theorem Th41: :: YELLOW12:41

for b₁, b₂, b₃ being non empty TopSpace
for b₄ being continuous Function of b₁,b₂
for b₅ being continuous Function of b₁,b₃ holds <:b₄,b₅:> is continuous Function of b₁,[:b₂,b₃:]

proof end;

theorem Th42: :: YELLOW12:42

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

proof end;

theorem Th43: :: YELLOW12:43

for b₁, b₂ being non empty TopSpace
for b₃ being Function of [:b₁,b₂:],[:b₂,b₁:] st b₃ = <:(pr2 the carrier of b₁,the carrier of b₂),(pr1 the carrier of b₁,the carrier of b₂):> holds
b₃ is_homeomorphism

proof end;

theorem Th44: :: YELLOW12:44

for b₁, b₂ being non empty TopSpace holds [:b₁,b₂:],[:b₂,b₁:] are_homeomorphic

proof end;

theorem Th45: :: YELLOW12:45

for b₁ being non empty TopSpace
for b₂ being non empty Hausdorff TopSpace
for b₃, b₄ being continuous Function of b₁,b₂ holds
( ( for b₅ being Subset of b₁ st b₅ = { b₆ where B is Point of b₁ : b₃ . b₆ <> b₄ . b₆ } holds
b₅ is open ) & ( for b₅ being Subset of b₁ st b₅ = { b₆ where B is Point of b₁ : b₃ . b₆ = b₄ . b₆ } holds
b₅ is closed ) )

proof end;

theorem Th46: :: YELLOW12:46

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

proof end;

registration

let c₁, c₂ be TopStruct ;
cluster strict Refinement of a₁,a₂;
existence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
let c₂ be TopStruct ;
cluster non empty strict Refinement of a₁,a₂;
existence

proof end;

cluster non empty strict Refinement of a₂,a₁;
existence

proof end;

end;

theorem Th47: :: YELLOW12:47

for b₁, b₂, b₃ being TopStruct holds
( b₁ is Refinement of b₂,b₃ iff TopStruct(# the carrier of b₁,the topology of b₁ #) is Refinement of b₂,b₃ )

proof end;

theorem Th48: :: YELLOW12:48

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Refinement of [:b₁,b₃:],[:b₂,b₄:] st the carrier of b₁ = the carrier of b₂ & the carrier of b₃ = the carrier of b₄ holds
{ ([:b₆,b₈:] /\ [:b₇,b₉:]) where B is Subset of b₁, B is Subset of b₂, B is Subset of b₃, B is Subset of b₄ : ( b₆ is open & b₇ is open & b₈ is open & b₉ is open ) } is Basis of b₅

proof end;

theorem Th49: :: YELLOW12:49

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Refinement of [:b₁,b₃:],[:b₂,b₄:]
for b₆ being Refinement of b₁,b₂
for b₇ being Refinement of b₃,b₄ st the carrier of b₁ = the carrier of b₂ & the carrier of b₃ = the carrier of b₄ holds
( the carrier of [:b₆,b₇:] = the carrier of b₅ & the topology of [:b₆,b₇:] = the topology of b₅ )

proof end;

theorem Th50: :: YELLOW12:50

for b₁, b₂, b₃, b₄ being non empty TopSpace
for b₅ being Refinement of b₁,b₂
for b₆ being Refinement of b₃,b₄ st the carrier of b₁ = the carrier of b₂ & the carrier of b₃ = the carrier of b₄ holds
[:b₅,b₆:] is Refinement of [:b₁,b₃:],[:b₂,b₄:]

proof end;