:: Some Properties of Isomorphism between Relational Structures. On the Product of Topological Spaces
:: by Jaros{\l}aw Gryko and Artur Korni{\l}owicz
::
:: Received June 22, 1999
:: Copyright (c) 1999-2012 Association of Mizar Users


begin

theorem :: YELLOW14:1
bool 1 = {0,1} by CARD_1:49, ZFMISC_1:24;

theorem Th2: :: YELLOW14:2
for X being set
for Y being Subset of X holds rng ((id X) | Y) = Y
proofend;

theorem :: YELLOW14:3
for S being empty 1-sorted
for T being 1-sorted
for f being Function of S,T st rng f = [#] T holds
T is empty ;

theorem :: YELLOW14:4
for S being 1-sorted
for T being empty 1-sorted
for f being Function of S,T st dom f = [#] S holds
S is empty ;

theorem :: YELLOW14:5
for S being non empty 1-sorted
for T being 1-sorted
for f being Function of S,T st dom f = [#] S holds
not T is empty ;

theorem :: YELLOW14:6
for S being 1-sorted
for T being non empty 1-sorted
for f being Function of S,T st rng f = [#] T holds
not S is empty ;

definition
let S be non empty reflexive RelStr ;
let T be non empty RelStr ;
let f be Function of S,T;
redefine attr f is directed-sups-preserving  means :: YELLOW14:def 1
 for X being non empty directed Subset of S holds f preserves_sup_of X;
compatibility
 ( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X )
proofend;
end;

:: deftheorem  defines directed-sups-preserving YELLOW14:def_1_:_
 for S being non empty reflexive RelStr
for T being non empty RelStr
for f being Function of S,T holds
( f is directed-sups-preserving iff for X being non empty directed Subset of S holds f preserves_sup_of X );

definition
let R be 1-sorted ;
let N be NetStr over R;
attrN is Function-yielding  means :Def2: :: YELLOW14:def 2
 the mapping of N is Function-yielding ;
end;

:: deftheorem Def2 defines Function-yielding YELLOW14:def_2_:_
 for R being 1-sorted
for N being NetStr over R holds
( N is Function-yielding iff the mapping of N is Function-yielding );

registration
cluster non empty constituted-Functions for 1-sorted ;
existence
 ex b1 being 1-sorted st
( not b1 is empty & b1 is constituted-Functions )
proofend;
end;

registration
cluster non empty strict constituted-Functions for RelStr ;
existence
 ex b1 being RelStr st
( b1 is strict & not b1 is empty & b1 is constituted-Functions )
proofend;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster  ->  Function-yielding for NetStr over R;
coherence
 for b1 being NetStr over R holds b1 is Function-yielding
proofend;
end;

registration
let R be constituted-Functions 1-sorted ;
cluster strict Function-yielding for NetStr over R;
existence
 ex b1 being NetStr over R st
( b1 is strict & b1 is Function-yielding )
proofend;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster non empty strict Function-yielding for NetStr over R;
existence
 ex b1 being NetStr over R st
( b1 is strict & not b1 is empty & b1 is Function-yielding )
proofend;
end;

registration
let R be constituted-Functions 1-sorted ;
let N be Function-yielding NetStr over R;
cluster the mapping of N ->  Function-yielding ;
coherence
 the mapping of N is Function-yielding by Def2;
end;

registration
let R be non empty constituted-Functions 1-sorted ;
cluster non empty transitive strict directed Function-yielding for NetStr over R;
existence
 ex b1 being net of R st
( b1 is strict & b1 is Function-yielding )
proofend;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
cluster rng the mapping of N ->  non empty ;
coherence
 not rng the mapping of N is empty ;
end;

registration
let S be non empty 1-sorted ;
let N be non empty NetStr over S;
cluster rng (netmap (N,S)) ->  non empty ;
coherence
 not rng (netmap (N,S)) is empty ;
end;

theorem :: YELLOW14:7
for A, B, C being non empty RelStr
for f being Function of B,C
for g, h being Function of A,B st g <= h &amp; f is monotone holds
f * g <= f * h
proofend;

theorem :: YELLOW14:8
for S being non empty TopSpace
for T being non empty TopSpace-like TopRelStr
for f, g being Function of S,T
for x, y being Element of (ContMaps (S,T)) st x = f &amp; y = g holds
( x <= y iff f <= g )
proofend;

definition
let I be non empty set ;
let R be non empty RelStr ;
let f be Element of (R |^ I);
let i be Element of I;
:: original:.
redefine funcf . i ->  Element of R;
coherence
 f . i is Element of R
proofend;
end;

begin

theorem Th9: :: YELLOW14:9
for S, T being RelStr
for f being Function of S,T st f is isomorphic holds
f is onto
proofend;

registration
let S, T be RelStr ;
cluster Function-like quasi_total isomorphic  ->  onto for Element of K6(K7( the carrier of S, the carrier of T));
coherence
 for b1 being Function of S,T st b1 is isomorphic holds
b1 is onto by Th9;
end;

theorem Th10: :: YELLOW14:10
for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
f /" is isomorphic
proofend;

theorem :: YELLOW14:11
for S, T being non empty RelStr st S,T are_isomorphic &amp; S is with_infima holds
T is with_infima
proofend;

theorem :: YELLOW14:12
for S, T being non empty RelStr st S,T are_isomorphic &amp; S is with_suprema holds
T is with_suprema
proofend;

theorem Th13: :: YELLOW14:13
for L being RelStr st L is empty holds
L is bounded
proofend;

registration
cluster empty  ->  bounded for RelStr ;
coherence
 for b1 being RelStr st b1 is empty holds
b1 is bounded by Th13;
end;

theorem :: YELLOW14:14
for S, T being RelStr st S,T are_isomorphic &amp; S is lower-bounded holds
T is lower-bounded
proofend;

theorem :: YELLOW14:15
for S, T being RelStr st S,T are_isomorphic &amp; S is upper-bounded holds
T is upper-bounded
proofend;

theorem :: YELLOW14:16
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic &amp; ex_sup_of A,S holds
ex_sup_of f .: A,T
proofend;

theorem :: YELLOW14:17
for S, T being non empty RelStr
for A being Subset of S
for f being Function of S,T st f is isomorphic &amp; ex_inf_of A,S holds
ex_inf_of f .: A,T
proofend;

begin

theorem :: YELLOW14:18
for S, T being TopStruct st ( S,T are_homeomorphic or ex f being Function of S,T st
( dom f = [#] S &amp; rng f = [#] T ) ) holds
( S is empty iff T is empty )
proofend;

theorem :: YELLOW14:19
for T being non empty TopSpace holds T, TopStruct(# the carrier of T, the topology of T #) are_homeomorphic
proofend;

registration
let T be non empty reflexive Scott TopRelStr ;
cluster open  ->  upper inaccessible for Element of K6( the carrier of T);
coherence
 for b1 being Subset of T st b1 is open holds
( b1 is inaccessible &amp; b1 is upper ) by WAYBEL11:def_4;
cluster upper inaccessible  ->  open for Element of K6( the carrier of T);
coherence
 for b1 being Subset of T st b1 is inaccessible &amp; b1 is upper holds
b1 is open by WAYBEL11:def_4;
end;

theorem :: YELLOW14:20
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} &amp; Cl X c= Cl Y holds
x in Cl Y
proofend;

theorem :: YELLOW14:21
for T being TopStruct
for x, y being Point of T
for Y, V being Subset of T st Y = {y} &amp; x in Cl Y &amp; V is open &amp; x in V holds
y in V
proofend;

theorem :: YELLOW14:22
for T being TopStruct
for x, y being Point of T
for X, Y being Subset of T st X = {x} &amp; Y = {y} &amp; ( for V being Subset of T st V is open &amp; x in V holds
y in V ) holds
Cl X c= Cl Y
proofend;

theorem Th23: :: YELLOW14:23
for S, T being non empty TopSpace
for A being irreducible Subset of S
for B being Subset of T st A = B &amp; TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is irreducible
proofend;

theorem Th24: :: YELLOW14:24
for S, T being non empty TopSpace
for a being Point of S
for b being Point of T
for A being Subset of S
for B being Subset of T st a = b &amp; A = B &amp; TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; a is_dense_point_of A holds
b is_dense_point_of B
proofend;

theorem Th25: :: YELLOW14:25
for S, T being TopStruct
for A being Subset of S
for B being Subset of T st A = B &amp; TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; A is compact holds
B is compact
proofend;

theorem :: YELLOW14:26
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; S is sober holds
T is sober
proofend;

theorem :: YELLOW14:27
for S, T being non empty TopSpace st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; S is locally-compact holds
T is locally-compact
proofend;

theorem :: YELLOW14:28
for S, T being TopStruct st TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) &amp; S is compact holds
T is compact
proofend;

definition
let I be non empty set ;
let T be non empty TopSpace;
let x be Point of (product (I --> T));
let i be Element of I;
:: original:.
redefine funcx . i ->  Element of T;
coherence
 x . i is Element of T
proofend;
end;

theorem Th29: :: YELLOW14:29
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proofend;

theorem :: YELLOW14:30
for M being non empty set
for T being non empty TopSpace
for x, y being Point of (product (M --> T)) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
proofend;

theorem Th31: :: YELLOW14:31
for M being non empty set
for i being Element of M
for J being non-Empty TopStruct-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}
proofend;

theorem :: YELLOW14:32
for M being non empty set
for i being Element of M
for T being non empty TopSpace
for x being Point of (product (M --> T)) holds pi ((Cl {x}),i) = Cl {(x . i)}
proofend;

theorem :: YELLOW14:33
for X, Y being non empty TopStruct
for f being Function of X,Y
for g being Function of Y,X st f = id X &amp; g = id X &amp; f is continuous &amp; g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
proofend;

theorem :: YELLOW14:34
for X, Y being non empty TopSpace
for f being Function of X,Y st corestr f is continuous holds
f is continuous
proofend;

registration
let X be non empty TopSpace;
let Y be non empty SubSpace of X;
cluster incl Y ->  continuous ;
coherence
 incl Y is continuous by TMAP_1:87;
end;

theorem :: YELLOW14:35
for T being non empty TopSpace
for f being Function of T,T st f * f = f holds
(corestr f) * (incl (Image f)) = id (Image f)
proofend;

theorem :: YELLOW14:36
for Y being non empty TopSpace
for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism
proofend;

theorem Th37: :: YELLOW14:37
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds J . i is T_0 TopSpace ) holds
product J is T_0
proofend;

registration
let I be non empty set ;
let T be non empty T_0 TopSpace;
cluster product (I --> T) ->  T_0 ;
coherence
 product (I --> T) is T_0
proofend;
end;

theorem Th38: :: YELLOW14:38
for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds
( J . i is T_1 &amp; J . i is TopSpace-like ) ) holds
product J is T_1
proofend;

registration
let I be non empty set ;
let T be non empty T_1 TopSpace;
cluster product (I --> T) ->  T_1 ;
coherence
 product (I --> T) is T_1
proofend;
end;