:: by Artur Korni{\l}owicz

::

:: Received April 18, 1998

:: Copyright (c) 1998-2021 Association of Mizar Users

registration
end;

Lm1: now :: thesis: for S, T, x1, x2 being set st x1 in S & x2 in T holds

<:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]

<:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]

let S, T, x1, x2 be set ; :: thesis: ( x1 in S & x2 in T implies <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1] )

assume A1: ( x1 in S & x2 in T ) ; :: thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]

A2: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def 7

.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def 4

.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5

.= [:S,T:] ;

[x1,x2] in [:S,T:] by A1, ZFMISC_1:87;

hence <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def 7

.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def 5

.= [x2,x1] by A1, FUNCT_3:def 4 ;

:: thesis: verum

end;
assume A1: ( x1 in S & x2 in T ) ; :: thesis: <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [x2,x1]

A2: dom <:(pr2 (S,T)),(pr1 (S,T)):> = (dom (pr2 (S,T))) /\ (dom (pr1 (S,T))) by FUNCT_3:def 7

.= (dom (pr2 (S,T))) /\ [:S,T:] by FUNCT_3:def 4

.= [:S,T:] /\ [:S,T:] by FUNCT_3:def 5

.= [:S,T:] ;

[x1,x2] in [:S,T:] by A1, ZFMISC_1:87;

hence <:(pr2 (S,T)),(pr1 (S,T)):> . (x1,x2) = [((pr2 (S,T)) . (x1,x2)),((pr1 (S,T)) . (x1,x2))] by A2, FUNCT_3:def 7

.= [x2,((pr1 (S,T)) . (x1,x2))] by A1, FUNCT_3:def 5

.= [x2,x1] by A1, FUNCT_3:def 4 ;

:: thesis: verum

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:] )

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

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:]

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 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

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

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

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

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 )

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

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

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

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

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

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 join-inheriting holds

J is join-inheriting

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 join-inheriting holds

J is join-inheriting

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 is property(S) holds

Y is property(S)

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 is property(S) holds

Y is property(S)

proof end;

theorem :: YELLOW12:20

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 is directly_closed holds

Y is directly_closed

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 is directly_closed holds

Y is directly_closed

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

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;

definition

let L be non empty RelStr ;

let f be Function of [:L,L:],L;

let a, b be Element of L;

:: original: .

redefine func f . (a,b) -> Element of L;

coherence

f . (a,b) is Element of L

end;
let f be Function of [:L,L:],L;

let a, b be Element of L;

:: original: .

redefine func f . (a,b) -> Element of L;

coherence

f . (a,b) is Element of L

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

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;

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

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
end;

theorem :: YELLOW12:26

for N being Semilattice

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

A is filtered

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

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

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

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

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

for x being Element of N

for X being Subset of N st x in X holds

downarrow x c= downarrow X

proof 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

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

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;

registration
end;

registration

let T be non empty TopSpace;

let x be Point of T;

coherence

for b_{1} being Basis of x holds not b_{1} is empty
by Th35;

end;
let x be Point of T;

coherence

for b

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

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 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 R, S, T 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:]

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 being_homeomorphism

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 being_homeomorphism

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 ) )

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 )

( 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
end;

registration

let S be non empty TopStruct ;

let T be TopStruct ;

existence

ex b_{1} being Refinement of S,T st

( b_{1} is strict & not b_{1} is empty )

ex b_{1} being Refinement of T,S st

( b_{1} is strict & not b_{1} is empty )

end;
let T be TopStruct ;

existence

ex b

( b

proof end;

existence ex b

( b

proof 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 )

( 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

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 )

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:]

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;