:: 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-2021 Association of Mizar Users


theorem :: YELLOW14:1
bool {0} = {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
proof end;

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 ) ;
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;
attr N 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 )
proof end;
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 )
proof end;
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
proof end;
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 )
proof end;
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 )
proof end;
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 )
proof end;
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 & f is monotone holds
f * g <= f * h
proof end;

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 & y = g holds
( x <= y iff f <= g )
proof end;

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 func f . i -> Element of R;
coherence
f . i is Element of R
proof end;
end;

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

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

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

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

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

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 & S is lower-bounded holds
T is lower-bounded
proof end;

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

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 & ex_sup_of A,S holds
ex_sup_of f .: A,T
proof end;

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 & ex_inf_of A,S holds
ex_inf_of f .: A,T
proof end;

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 & rng f = [#] T ) ) holds
( S is empty iff T is empty )
proof end;

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

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 & 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 & 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} & Cl X c= Cl Y holds
x in Cl Y
proof end;

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

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

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 & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) holds
B is irreducible
proof end;

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 & A = B & TopStruct(# the carrier of S, the topology of S #) = TopStruct(# the carrier of T, the topology of T #) & a is_dense_point_of A holds
b is_dense_point_of B
proof end;

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

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 #) & S is sober holds
T is sober
proof end;

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 #) & S is locally-compact holds
T is locally-compact
proof end;

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 #) & S is compact holds
T is compact
proof end;

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 func x . i -> Element of T;
coherence
x . i is Element of T
proof end;
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)} )
proof end;

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)} )
proof end;

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)}
proof end;

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)}
proof end;

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 & g = id X & f is continuous & g is continuous holds
TopStruct(# the carrier of X, the topology of X #) = TopStruct(# the carrier of Y, the topology of Y #)
proof end;

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

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

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

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

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
proof end;
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 & J . i is TopSpace-like ) ) holds
product J is T_1
proof end;

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