Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Adam Grabowski
- Received June 22, 1999
- MML identifier: WAYBEL24
- [
Mizar article,
MML identifier index
]
environ
vocabulary WAYBEL_0, WAYBEL11, WAYBEL_9, WAYBEL17, LATTICES, ORDINAL2,
PRE_TOPC, YELLOW_1, ORDERS_1, RELAT_2, SEQM_3, FUNCT_1, RELAT_1,
FUNCOP_1, LATTICE3, BOOLE, GROUP_1, BHSP_3, YELLOW_0, FUNCT_2, BORSUK_1,
FUNCT_5, MCART_1, QUANTAL1, CAT_1, MONOID_0, WAYBEL_3, PBOOLE, CARD_3,
FUNCT_4, WAYBEL24;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
FUNCT_2, FUNCT_5, SEQM_3, MONOID_0, CARD_3, FUNCOP_1, BORSUK_1, PRE_TOPC,
ORDERS_1, LATTICE3, PBOOLE, FUNCT_7, YELLOW_0, ORDERS_3, WAYBEL_0,
YELLOW_1, YELLOW_2, WAYBEL_3, WAYBEL_9, WAYBEL11, WAYBEL17, YELLOW_3;
constructors FUNCT_7, SEQM_3, ORDERS_3, WAYBEL_3, WAYBEL_5, WAYBEL_1,
WAYBEL17, MONOID_0, BORSUK_1;
clusters STRUCT_0, WAYBEL_0, WAYBEL_3, RELSET_1, YELLOW_1, LATTICE3, BORSUK_2,
WAYBEL10, WAYBEL11, WAYBEL17, YELLOW_3, YELLOW_0, MONOID_0, SUBSET_1,
FUNCT_2, XBOOLE_0;
requirements SUBSET, BOOLE;
begin :: Preliminaries
theorem :: WAYBEL24:1
for S, T being up-complete Scott TopLattice
for M being Subset of SCMaps (S,T) holds
"\/" (M, SCMaps (S,T)) is continuous map of S, T;
definition let S be non empty RelStr,
T be non empty reflexive RelStr;
cluster constant -> monotone map of S, T;
end;
definition let S be non empty RelStr,
T be reflexive non empty RelStr,
a be Element of T;
cluster S --> a -> monotone;
end;
theorem :: WAYBEL24:2
for S being non empty RelStr,
T being lower-bounded antisymmetric reflexive non empty RelStr holds
Bottom MonMaps(S, T) = S --> Bottom T;
theorem :: WAYBEL24:3
for S being non empty RelStr,
T being upper-bounded antisymmetric reflexive non empty RelStr holds
Top MonMaps(S, T) = S --> Top T;
theorem :: WAYBEL24:4
for S, T being complete LATTICE,
f being monotone map of S, T holds
for x being Element of S holds f.x = sup (f.:downarrow x);
theorem :: WAYBEL24:5
for S, T being complete lower-bounded LATTICE,
f being monotone map of S, T holds
( for x being Element of S holds
f.x = "\/"({ f.w where w is Element of S : w <= x },T) );
theorem :: WAYBEL24:6
for S being RelStr, T being non empty RelStr,
F being Subset of (T |^ the carrier of S) holds sup F is map of S, T;
begin :: On the Scott continuity of maps
definition let X1, X2, Y be non empty RelStr;
let f be map of [:X1, X2:], Y;
let x be Element of X1;
func Proj (f, x) -> map of X2, Y equals
:: WAYBEL24:def 1
(curry f).x;
end;
reserve X1, X2, Y for non empty RelStr,
f for map of [:X1, X2:], Y,
x for Element of X1,
y for Element of X2;
theorem :: WAYBEL24:7
for y being Element of X2 holds
(Proj (f, x)). y = f. [x, y];
definition let X1, X2, Y be non empty RelStr;
let f be map of [:X1, X2:], Y;
let y be Element of X2;
func Proj (f, y) -> map of X1, Y equals
:: WAYBEL24:def 2
(curry' f).y;
end;
theorem :: WAYBEL24:8
for x being Element of X1 holds
(Proj (f, y)). x = f. [x, y];
theorem :: WAYBEL24:9
for R, S, T being non empty RelStr,
f being map of [:R,S:], T,
a being Element of R,
b being Element of S holds
Proj (f, a). b = Proj (f, b). a;
definition
let S be non empty RelStr, T be non empty reflexive RelStr;
cluster antitone map of S, T;
end;
theorem :: WAYBEL24:10
for R, S, T being non empty reflexive RelStr,
f being map of [:R,S:], T,
a being Element of R,
b being Element of S st
f is monotone holds Proj (f, a) is monotone & Proj (f, b) is monotone;
theorem :: WAYBEL24:11
for R, S, T being non empty reflexive RelStr,
f being map of [:R,S:], T,
a being Element of R,
b being Element of S st
f is antitone holds Proj (f, a) is antitone & Proj (f, b) is antitone;
definition let R, S, T be non empty reflexive RelStr;
let f be monotone map of [:R, S:], T;
let a be Element of R;
cluster Proj (f, a) -> monotone;
end;
definition let R, S, T be non empty reflexive RelStr;
let f be monotone map of [:R, S:], T;
let b be Element of S;
cluster Proj (f, b) -> monotone;
end;
definition let R, S, T be non empty reflexive RelStr;
let f be antitone map of [:R, S:], T;
let a be Element of R;
cluster Proj (f, a) -> antitone;
end;
definition let R, S, T be non empty reflexive RelStr;
let f be antitone map of [:R, S:], T;
let b be Element of S;
cluster Proj (f, b) -> antitone;
end;
theorem :: WAYBEL24:12
for R, S, T being LATTICE,
f being map of [:R,S:], T st
( for a being Element of R, b being Element of S holds
Proj (f, a) is monotone & Proj (f, b) is monotone)
holds f is monotone;
theorem :: WAYBEL24:13
for R, S, T being LATTICE,
f being map of [:R,S:], T st
( for a being Element of R, b being Element of S holds
Proj (f, a) is antitone & Proj (f, b) is antitone)
holds f is antitone;
theorem :: WAYBEL24:14
for R, S, T being LATTICE,
f being map of [:R,S:], T,
b being Element of S,
X being Subset of R holds
Proj (f, b).:X = f.:[:X, {b}:];
theorem :: WAYBEL24:15
for R, S, T being LATTICE,
f being map of [:R,S:], T,
b being Element of R,
X being Subset of S holds
Proj (f, b).:X = f.:[:{b}, X:];
theorem :: WAYBEL24:16 :: Lemma 2.9 p. 116 (1) => (2)
for R, S, T being LATTICE,
f being map of [:R,S:], T,
a being Element of R,
b being Element of S st
f is directed-sups-preserving holds
Proj (f, a) is directed-sups-preserving &
Proj (f, b) is directed-sups-preserving;
theorem :: WAYBEL24:17
for R, S, T being LATTICE,
f being monotone map of [:R, S:], T,
a being Element of R, b being Element of S,
X being directed Subset of [:R, S:] st
ex_sup_of f.:X, T & a in proj1 X & b in proj2 X holds
f. [a, b] <= sup (f.:X);
theorem :: WAYBEL24:18 :: Lemma 2.9 p. 116 (2) => (1)
for R, S, T being complete LATTICE,
f being map of [:R, S:], T st
( for a being Element of R, b being Element of S holds
Proj (f, a) is directed-sups-preserving &
Proj (f, b) is directed-sups-preserving ) holds
f is directed-sups-preserving;
theorem :: WAYBEL24:19
for S being non empty 1-sorted,
T being non empty RelStr,
f be set holds
f is Element of (T |^ the carrier of S) iff f is map of S, T;
begin :: The poset of continuous maps
definition let S be TopStruct,
T be non empty TopRelStr;
func ContMaps (S, T) -> strict RelStr means
:: WAYBEL24:def 3
it is full SubRelStr of T |^ the carrier of S &
for x being set holds
x in the carrier of it iff
ex f being map of S, T st x = f & f is continuous;
end;
definition let S be non empty TopSpace,
T be non empty TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> non empty;
end;
definition let S be non empty TopSpace,
T be non empty TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> constituted-Functions;
end;
theorem :: WAYBEL24:20
for S being non empty TopSpace,
T being non empty reflexive TopSpace-like TopRelStr,
x, y being Element of ContMaps (S, T) holds
x <= y iff for i being Element of S holds
[x.i, y.i] in the InternalRel of T;
theorem :: WAYBEL24:21
for S being non empty TopSpace,
T being non empty reflexive TopSpace-like TopRelStr,
x being set holds
x is continuous map of S, T iff x is Element of ContMaps (S, T);
definition let S be non empty TopSpace,
T be non empty reflexive TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> reflexive;
end;
definition let S be non empty TopSpace,
T be non empty transitive TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> transitive;
end;
definition let S be non empty TopSpace,
T be non empty antisymmetric TopSpace-like TopRelStr;
cluster ContMaps (S, T) -> antisymmetric;
end;
definition let S be non empty 1-sorted,
T be non empty TopSpace-like TopRelStr;
cluster T |^ the carrier of S -> constituted-Functions;
end;
theorem :: WAYBEL24:22
for S being non empty 1-sorted,
T being complete LATTICE
for f, g, h being map of S, T,
i being Element of S st h = "\/" ({f, g}, T |^ the carrier of S) holds
h.i = sup {f.i, g.i};
theorem :: WAYBEL24:23
for I being non empty set
for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
st for i being Element of I holds J.i is complete LATTICE
for X being Subset of product J, i being Element of I holds
(inf X).i = inf pi(X,i);
theorem :: WAYBEL24:24
for S being non empty 1-sorted,
T being complete LATTICE
for f, g, h being map of S, T,
i being Element of S st h = "/\" ({f, g}, T |^ the carrier of S) holds
h.i = inf {f.i, g.i};
definition let S be non empty 1-sorted, T be LATTICE;
cluster -> Function-like Relation-like Element of (T |^ the carrier of S);
end;
definition let S, T be TopLattice;
cluster -> Function-like Relation-like Element of ContMaps (S, T);
end;
theorem :: WAYBEL24:25
for S being non empty RelStr,
T being complete LATTICE
for F being non empty Subset of (T |^ the carrier of S),
i being Element of S holds
(sup F).i = "\/" ({ f.i where f is Element of (T |^ the carrier of S) :
f in F }, T );
theorem :: WAYBEL24:26
for S, T being complete TopLattice
for F being non empty Subset of ContMaps (S, T),
i being Element of S holds
"\/" (F, (T |^ the carrier of S)).i =
"\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T );
reserve S for non empty RelStr, T for complete LATTICE;
theorem :: WAYBEL24:27
for F being non empty Subset of (T |^ the carrier of S),
D being non empty Subset of S holds
(sup F).:D =
{ "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T )
where i is Element of S : i in D };
theorem :: WAYBEL24:28
for S, T being complete Scott TopLattice,
F being non empty Subset of ContMaps (S, T),
D being non empty Subset of S holds
("\/" (F, (T |^ the carrier of S))).:D =
{ "\/" ({ f.i where f is Element of (T |^ the carrier of S) : f in F }, T )
where i is Element of S : i in D };
scheme FraenkelF'RSS{ B() -> non empty RelStr, F(set) -> set, G(set) -> set,
P[set] } :
{ F(v1) where v1 is Element of B() : P[v1] }
= { G(v2) where v2 is Element of B() : P[v2] }
provided
for v being Element of B() st P[v] holds F(v) = G(v);
theorem :: WAYBEL24:29
for S, T being complete Scott TopLattice,
F being non empty Subset of ContMaps (S, T) holds
"\/" (F, (T |^ the carrier of S)) is monotone map of S, T;
theorem :: WAYBEL24:30
for S, T being complete Scott TopLattice,
F being non empty Subset of ContMaps (S, T),
D being directed non empty Subset of S holds
"\/"({ "\/"({g.i where i is Element of S : i in D }, T )
where g is Element of (T |^ the carrier of S) : g in F }, T ) =
"\/"({ "\/"
({g'.i' where g' is Element of (T |^ the carrier of S) : g' in F },
T ) where i' is Element of S : i' in D }, T);
theorem :: WAYBEL24:31
for S, T being complete Scott TopLattice,
F being non empty Subset of ContMaps (S, T),
D being directed non empty Subset of S holds
"\/" (("\/"(F, (T |^ the carrier of S))).:D, T) =
"\/" (F, (T |^ the carrier of S)).sup D;
theorem :: WAYBEL24:32
for S, T being complete Scott TopLattice,
F being non empty Subset of ContMaps (S, T) holds
"\/"(F, (T |^ the carrier of S)) in the carrier of ContMaps (S, T);
theorem :: WAYBEL24:33
for S being non empty RelStr,
T being lower-bounded antisymmetric non empty RelStr holds
Bottom (T |^ the carrier of S) = S --> Bottom T;
theorem :: WAYBEL24:34
for S being non empty RelStr,
T being upper-bounded antisymmetric non empty RelStr holds
Top (T |^ the carrier of S) = S --> Top T;
definition let S be non empty reflexive RelStr,
T be complete LATTICE,
a be Element of T;
cluster S --> a -> directed-sups-preserving;
end;
theorem :: WAYBEL24:35 :: Lemma 2.4, p. 115
for S, T being complete Scott TopLattice holds
ContMaps (S, T) is sups-inheriting SubRelStr of (T |^ the carrier of S);
definition let S, T be complete Scott TopLattice;
cluster ContMaps (S, T) -> complete;
end;
theorem :: WAYBEL24:36
for S, T being non empty Scott complete TopLattice holds
Bottom ContMaps (S, T) = S --> Bottom T;
theorem :: WAYBEL24:37
for S, T being non empty Scott complete TopLattice holds
Top ContMaps (S, T) = S --> Top T;
theorem :: WAYBEL24:38
for S, T being Scott complete TopLattice holds
SCMaps (S, T) = ContMaps (S, T);
Back to top