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

begin

theorem :: YELLOW14:1

bool 1 = {0,1} by CARD_1:87, ZFMISC_1:30;

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

canceled;

theorem :: YELLOW14:4

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

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

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

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 )

proof end;

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 of 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 of R holds
( N is Function-yielding iff the mapping of N is Function-yielding );

registration

cluster non empty constituted-Functions 1-sorted ;
existence
ex b₁ being 1-sorted st
( not b₁ is empty & b₁ is constituted-Functions )

proof end;

end;

registration

cluster non empty strict constituted-Functions RelStr ;
existence
ex b₁ being RelStr st
( b₁ is strict & not b₁ is empty & b₁ is constituted-Functions )

proof end;

end;

registration

let R be constituted-Functions 1-sorted ;
cluster -> Function-yielding NetStr of R;
coherence
for b₁ being NetStr of R holds b₁ is Function-yielding

proof end;

end;

registration

let R be constituted-Functions 1-sorted ;
cluster strict Function-yielding NetStr of R;
existence
ex b₁ being NetStr of R st
( b₁ is strict & b₁ is Function-yielding )

proof end;

end;

registration

let R be non empty constituted-Functions 1-sorted ;
cluster non empty strict Function-yielding NetStr of R;
existence
ex b₁ being NetStr of R st
( b₁ is strict & not b₁ is empty & b₁ is Function-yielding )

proof end;

end;

registration

let R be constituted-Functions 1-sorted ;
let N be Function-yielding NetStr of 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 NetStr of R;
existence
ex b₁ being net of R st
( b₁ is strict & b₁ is Function-yielding )

proof end;

end;

registration

let S be non empty 1-sorted ;
let N be non empty NetStr of S;
cluster proj2 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 of S;
cluster proj2 (netmap (N,S)) -> non empty ;
coherence
not rng (netmap (N,S)) is empty ;

end;

theorem :: YELLOW14:8

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

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;

begin

theorem Th10: :: YELLOW14:10

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 Element of bool [: the carrier of S, the carrier of T:];
coherence
for b₁ being Function of S,T st b₁ is isomorphic holds
b₁ is onto by Th10;

end;

theorem Th11: :: YELLOW14:11

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

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

for S, T being non empty RelStr st S,T are_isomorphic & S is with_suprema holds
T is with_suprema

proof end;

theorem Th14: :: YELLOW14:14

for L being RelStr st L is empty holds
L is bounded

proof end;

registration

cluster empty -> bounded RelStr ;
coherence
for b₁ being RelStr st b₁ is empty holds
b₁ is bounded by Th14;

end;

theorem :: YELLOW14:15

for S, T being RelStr st S,T are_isomorphic & S is lower-bounded holds
T is lower-bounded

proof end;

theorem :: YELLOW14:16

for S, T being RelStr st S,T are_isomorphic & S is upper-bounded holds
T is upper-bounded

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_sup_of A,S holds
ex_sup_of f .: A,T

proof end;

theorem :: YELLOW14:18

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;

begin

theorem :: YELLOW14:19

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

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 Element of bool the carrier of T;
coherence
for b₁ being Subset of T st b₁ is open holds
( b₁ is inaccessible_by_directed_joins & b₁ is upper ) by WAYBEL11:def 4;
cluster upper inaccessible -> open Element of bool the carrier of T;
coherence
for b₁ being Subset of T st b₁ is inaccessible_by_directed_joins & b₁ is upper holds
b₁ is open by WAYBEL11:def 4;

end;

theorem :: YELLOW14:21

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

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

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 Th24: :: YELLOW14:24

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 Th25: :: YELLOW14:25

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 Th26: :: YELLOW14:26

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: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 sober holds
T is sober

proof end;

theorem :: YELLOW14:28

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

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 Th30: :: YELLOW14:30

for M being non empty set
for J being non-Empty TopSpace-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:31

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 Th32: :: YELLOW14:32

for M being non empty set
for i being Element of M
for J being non-Empty TopSpace-yielding ManySortedSet of M
for x being Point of (product J) holds pi ((Cl {x}),i) = Cl {(x . i)}

proof end;

theorem :: YELLOW14:33

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

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

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:98;

end;

theorem :: YELLOW14:36

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

for Y being non empty TopSpace
for W being non empty SubSpace of Y holds corestr (incl W) is being_homeomorphism

proof end;

theorem Th38: :: YELLOW14:38

for M being non empty set
for J being non-Empty TopSpace-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 Th39: :: YELLOW14:39

for M being non empty set
for J being non-Empty TopSpace-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;