:: Moore-Smith Convergence
:: by Andrzej Trybulec
::
:: Received November 12, 1996
:: Copyright (c) 1996-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies CLASSES2, CLASSES1, ORDINAL1, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI,
CARD_3, CARD_1, FUNCT_2, PRALG_1, PBOOLE, SUBSET_1, RLVECT_2, STRUCT_0,
FUNCOP_1, WAYBEL_3, YELLOW_1, ORDERS_2, WAYBEL_0, XXREAL_0, RELAT_2,
ZFMISC_1, CAT_1, YELLOW_0, WELLORD1, PRE_TOPC, RCOMP_1, CONNSP_2,
COMPTS_1, MCART_1, TOPS_1, SEQ_2, ORDINAL2, SETFAM_1, YELLOW_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, MCART_1,
RELAT_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, CARD_1,
CARD_3, FUNCOP_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, STRUCT_0,
TOPS_1, COMPTS_1, CONNSP_2, PRALG_1, ORDERS_2, LATTICE3, PRE_TOPC,
YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, WAYBEL_3;
constructors BINOP_1, CLASSES1, TOLER_1, CLASSES2, REALSET1, TOPS_1, COMPTS_1,
CONNSP_2, LATTICE3, PRALG_1, YELLOW_3, WAYBEL_3, RELSET_1, PBOOLE,
XTUPLE_0, WAYBEL_0;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1,
CARD_1, CLASSES1, CARD_3, CLASSES2, PBOOLE, STRUCT_0, ORDERS_2, PCOMPS_1,
LATTICE3, YELLOW_0, WAYBEL_0, PARTFUN1, YELLOW_1, YELLOW_3, WAYBEL_3,
RELSET_1, TOPS_1, RELAT_1, XTUPLE_0;
requirements BOOLE, SUBSET;
definitions TARSKI, STRUCT_0, WAYBEL_0, PRALG_1, YELLOW_1, YELLOW_0, RELAT_1,
PRE_TOPC, WAYBEL_3;
equalities STRUCT_0, WAYBEL_0, YELLOW_1, BINOP_1, SUBSET_1, WELLORD1;
expansions TARSKI, WAYBEL_0, YELLOW_0, RELAT_1, PRE_TOPC, WAYBEL_3;
theorems CONNSP_2, TOPS_1, FUNCOP_1, WAYBEL_0, PRE_TOPC, ORDERS_2, RELAT_1,
FUNCT_2, ZFMISC_1, FUNCT_1, TARSKI, PBOOLE, YELLOW_1, CARD_3, PRALG_1,
YELLOW_3, RELSET_1, DOMAIN_1, YELLOW_0, CLASSES2, CLASSES1, CARD_2,
FUNCT_6, LATTICE3, SUBSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, PARTFUN1;
schemes PBOOLE, FUNCT_7, SUBSET_1, RELSET_1, DOMAIN_1, MSSUBFAM, FUNCT_2,
XBOOLE_0;
begin :: Preliminaries, classical mathematics
reserve x,y,z,X for set,
T for Universe;
definition
let X;
func the_universe_of X -> set equals
Tarski-Class the_transitive-closure_of X;
correctness;
end;
registration
let X;
cluster the_universe_of X -> epsilon-transitive Tarski;
coherence;
end;
registration
let X;
cluster the_universe_of X -> universal non empty;
coherence;
end;
theorem Th1:
for f being Function st dom f in T & rng f c= T holds product f in T
proof
let f be Function such that
A1: dom f in T and
A2: rng f c= T;
card dom f in card T by A1,CLASSES2:1;
then card rng f in card T by CARD_2:61,ORDINAL1:12;
then rng f in T by A2,CLASSES1:1;
then union rng f in T by CLASSES2:59;
then Union f in T by CARD_3:def 4;
then product f c= Funcs(dom f, Union f) & Funcs(dom f, Union f) in T by A1,
CLASSES2:61,FUNCT_6:1;
hence thesis by CLASSES1:def 1;
end;
begin
begin :: 1-sorted structures
theorem Th2:
for Y be non empty set for J being 1-sorted-yielding
ManySortedSet of Y, i being Element of Y holds (Carrier J).i = the carrier of J
.i
proof
let Y be non empty set;
let J be 1-sorted-yielding ManySortedSet of Y, i be Element of Y;
ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R by
PRALG_1:def 15;
hence thesis;
end;
registration
cluster non empty constant 1-sorted-yielding for Function;
existence
proof
set S = the 1-sorted;
take f = {{}} --> S;
thus f is non empty;
thus f is constant;
let x be object;
assume x in dom(f);
hence thesis by FUNCOP_1:7;
end;
end;
notation
let J be 1-sorted-yielding Function;
synonym J is yielding_non-empty_carriers for J is non-Empty;
end;
definition
let J be 1-sorted-yielding Function;
redefine attr J is yielding_non-empty_carriers means :: redefines yielding_non-empty_carriers (YELLOW_6, synonym) → non-Empty (WAYBEL_3, definition)
:Def2:
for i being set st i in rng J holds i is non empty 1-sorted;
compatibility by PRALG_1:def 11;
end;
registration
let X be set;
let L be 1-sorted;
cluster X --> L -> 1-sorted-yielding;
coherence
proof
let x be object;
set IT = X --> L;
assume x in dom IT;
then IT.x in rng IT by FUNCT_1:def 3;
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be set;
cluster yielding_non-empty_carriers for
1-sorted-yielding ManySortedSet of I;
existence
proof
set R = the non empty 1-sorted;
take I --> R;
let i be set;
assume i in rng(I --> R);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be non empty set;
let J be RelStr-yielding ManySortedSet of I;
cluster the carrier of product J -> functional;
coherence
proof
product Carrier J is functional;
hence thesis by YELLOW_1:def 4;
end;
end;
registration
let I be set;
let J be yielding_non-empty_carriers 1-sorted-yielding ManySortedSet of I;
cluster Carrier J -> non-empty;
coherence
proof
assume {} in rng Carrier J;
then consider i being object such that
A1: i in dom Carrier J and
A2: (Carrier J).i = {} by FUNCT_1:def 3;
A3: i in I by A1;
then consider R being 1-sorted such that
A4: R = J.i and
A5: (Carrier J).i = the carrier of R by PRALG_1:def 15;
A6: R is empty by A2,A5;
i in dom J by A3,PARTFUN1:def 2;
then R in rng J by A4,FUNCT_1:def 3;
hence contradiction by A6,Def2;
end;
end;
begin :: Preliminaries to Relational Structures
registration
let T be non empty RelStr, A be lower Subset of T;
cluster A` -> upper;
coherence
proof
let x,y be Element of T such that
A1: x in A` and
A2: x <= y;
not x in A by A1,XBOOLE_0:def 5;
then not y in A by A2,WAYBEL_0:def 19;
hence thesis by XBOOLE_0:def 5;
end;
end;
registration
let T be non empty RelStr, A be upper Subset of T;
cluster A` -> lower;
coherence
proof
let x,y be Element of T such that
A1: x in A` and
A2: y <= x;
not x in A by A1,XBOOLE_0:def 5;
then not y in A by A2,WAYBEL_0:def 20;
hence thesis by XBOOLE_0:def 5;
end;
end;
definition
let N be non empty RelStr;
redefine attr N is directed means :: redefines directed (WAYBEL_0, definition)
:Def3:
for x,y being Element of N ex z being Element of N st x <= z & y <= z;
compatibility
proof
hereby
assume
A1: N is directed;
let x,y be Element of N;
[#]N is directed by A1;
then ex z being Element of N st z in [#]N & x <= z & y <= z;
hence ex z being Element of N st x <= z & y <= z;
end;
assume
A2: for x,y being Element of N ex z being Element of N st x <= z & y <= z;
let x,y be Element of N such that
x in [#]N and
y in [#]N;
consider z being Element of N such that
A3: x <= z & y <= z by A2;
take z;
thus z in [#]N;
thus thesis by A3;
end;
end;
registration
let X be set;
cluster BoolePoset X -> directed;
coherence;
end;
registration
cluster non empty directed transitive strict for RelStr;
existence
proof
take BoolePoset {};
thus thesis;
end;
end;
Lm1: for N being non empty RelStr holds N is directed iff the RelStr of N is
directed
proof
let N be non empty RelStr;
thus N is directed implies the RelStr of N is directed
proof
assume
A1: N is directed;
let x,y be Element of the RelStr of N;
reconsider x9 = x, y9 = y as Element of N;
consider z9 being Element of N such that
A2: x9 <= z9 & y9 <= z9 by A1;
reconsider z = z9 as Element of the RelStr of N;
take z;
[x,z] in the InternalRel of N & [y,z] in the InternalRel of N by A2,
ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
assume
A3: the RelStr of N is directed;
let x,y be Element of N;
reconsider x9 = x, y9 = y as Element of the RelStr of N;
consider z9 being Element of the RelStr of N such that
A4: x9 <= z9 & y9 <= z9 by A3;
reconsider z = z9 as Element of N;
take z;
[x9,z9] in the InternalRel of the RelStr of N & [y9,z9] in the
InternalRel of the RelStr of N by A4,ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
Lm2: for N being non empty RelStr holds N is transitive iff the RelStr of N is
transitive
proof
let N be non empty RelStr;
thus N is transitive implies the RelStr of N is transitive
proof
assume
A1: N is transitive;
let x,y,z be Element of the RelStr of N such that
A2: x <= y and
A3: y <= z;
reconsider x9 = x, y9 = y, z9 = z as Element of N;
[y,z] in the InternalRel of the RelStr of N by A3,ORDERS_2:def 5;
then
A4: y9 <= z9 by ORDERS_2:def 5;
[x,y] in the InternalRel of the RelStr of N by A2,ORDERS_2:def 5;
then x9 <= y9 by ORDERS_2:def 5;
then x9 <= z9 by A1,A4;
then [x9,z9] in the InternalRel of N by ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
assume
A5: the RelStr of N is transitive;
let x,y,z be Element of N such that
A6: x <= y and
A7: y <= z;
reconsider x9 = x, y9 = y, z9 = z as Element of the RelStr of N;
[y9,z9] in the InternalRel of the RelStr of N by A7,ORDERS_2:def 5;
then
A8: y9 <= z9 by ORDERS_2:def 5;
[x9,y9] in the InternalRel of the RelStr of N by A6,ORDERS_2:def 5;
then x9 <= y9 by ORDERS_2:def 5;
then x9 <= z9 by A5,A8;
then [x,z] in the InternalRel of N by ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
registration
let I be set;
cluster yielding_non-empty_carriers for RelStr-yielding ManySortedSet of I;
existence
proof
set R = the non empty RelStr;
take I --> R;
let i be set;
assume i in rng(I --> R);
hence thesis by TARSKI:def 1;
end;
end;
registration
let I be non empty set;
let J be yielding_non-empty_carriers RelStr-yielding ManySortedSet of I;
cluster product J -> non empty;
coherence;
end;
registration
let Y1,Y2 be directed RelStr;
cluster [:Y1,Y2:] -> directed;
coherence
proof
reconsider S2 = [#]Y2 as directed Subset of Y2 by WAYBEL_0:def 6;
reconsider S1 = [#]Y1 as directed Subset of Y1 by WAYBEL_0:def 6;
[:S1,S2:] is directed;
then [#][:Y1,Y2:] is directed by YELLOW_3:def 2;
hence thesis;
end;
end;
theorem Th3:
for R being RelStr holds the carrier of R = the carrier of R~
proof
let R be RelStr;
R~ = RelStr(#the carrier of R, (the InternalRel of R)~#) by LATTICE3:def 5;
hence thesis;
end;
Lm3: for R,S being RelStr, p,q being Element of R, p9,q9 being Element of S st
p = p9 & q = q9 & the RelStr of R = the RelStr of S holds p <= q implies p9 <=
q9
proof
let R,S be RelStr, p,q be Element of R, p9,q9 be Element of S such that
A1: p = p9 & q = q9 & the RelStr of R = the RelStr of S;
assume p <= q;
then [p9,q9] in the InternalRel of S by A1,ORDERS_2:def 5;
hence thesis by ORDERS_2:def 5;
end;
definition
let S be 1-sorted, N be NetStr over S;
attr N is constant means
:Def4:
the mapping of N is constant;
end;
definition
let R be RelStr, T be non empty 1-sorted, p be Element of T;
func ConstantNet(R,p) -> strict NetStr over T means
:Def5:
the RelStr of it
= the RelStr of R & the mapping of it = (the carrier of it) --> p;
existence
proof
reconsider f = (the carrier of R) --> p as Function of R,T;
take NetStr(#the carrier of R, the InternalRel of R,f#);
thus thesis;
end;
correctness;
end;
registration
let R be RelStr, T be non empty 1-sorted, p be Element of T;
cluster ConstantNet(R,p) -> constant;
coherence
proof
(the carrier of ConstantNet(R,p)) --> p is constant;
hence the mapping of ConstantNet(R,p) is constant by Def5;
end;
end;
registration
let R be non empty RelStr, T be non empty 1-sorted, p be Element of T;
cluster ConstantNet(R,p) -> non empty;
coherence
proof
the RelStr of ConstantNet(R,p) = the RelStr of R by Def5;
hence the carrier of ConstantNet(R,p) is non empty;
end;
end;
registration
let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of
T;
cluster ConstantNet(R,p) -> directed;
coherence
proof
the RelStr of ConstantNet(R,p) = the RelStr of R & the RelStr of R is
directed by Def5,Lm1;
hence thesis by Lm1;
end;
end;
registration
let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element
of T;
cluster ConstantNet(R,p) -> transitive;
coherence
proof
the RelStr of ConstantNet(R,p) = the RelStr of R & the RelStr of R is
transitive by Def5,Lm2;
hence thesis by Lm2;
end;
end;
theorem Th4:
for R be RelStr, T be non empty 1-sorted, p be Element of T
holds the carrier of ConstantNet(R,p) = the carrier of R
proof
let R be RelStr, T be non empty 1-sorted, p be Element of T;
the RelStr of ConstantNet(R,p) = the RelStr of R by Def5;
hence thesis;
end;
theorem Th5:
for R be non empty RelStr, T be non empty 1-sorted, p be Element
of T, q be Element of ConstantNet(R,p) holds ConstantNet(R,p).q = p
proof
let R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be
Element of ConstantNet(R,p);
thus ConstantNet(R,p).q = ((the carrier of ConstantNet(R,p)) --> p).q by Def5
.= p;
end;
registration
let T be non empty 1-sorted, N be non empty NetStr over T;
cluster the mapping of N -> non empty;
coherence;
end;
begin :: Substructures of Nets
theorem Th6:
for R being RelStr holds R is full SubRelStr of R
proof
let R be RelStr;
the InternalRel of R c= the InternalRel of R;
then reconsider R9 = R as SubRelStr of R by YELLOW_0:def 13;
the InternalRel of R9 = (the InternalRel of R)|_2 the carrier of R9 by
XBOOLE_1:28;
hence thesis by YELLOW_0:def 14;
end;
theorem Th7:
for R being RelStr, S being SubRelStr of R, T being SubRelStr of
S holds T is SubRelStr of R
proof
let R be RelStr, S be SubRelStr of R, T be SubRelStr of S;
the InternalRel of S c= the InternalRel of R & the InternalRel of T c=
the InternalRel of S by YELLOW_0:def 13;
then
A1: the InternalRel of T c= the InternalRel of R;
the carrier of S c= the carrier of R & the carrier of T c= the carrier
of S by YELLOW_0:def 13;
then the carrier of T c= the carrier of R;
hence thesis by A1,YELLOW_0:def 13;
end;
definition
let S be 1-sorted, N be NetStr over S;
mode SubNetStr of N -> NetStr over S means
:Def6:
it is SubRelStr of N & the
mapping of it = (the mapping of N)|the carrier of it;
existence
proof
take N;
thus N is SubRelStr of N by Th6;
thus the mapping of N = (the mapping of N)|the carrier of N;
end;
end;
theorem
for S being 1-sorted, N being NetStr over S holds N is SubNetStr of N
proof
let S be 1-sorted, N be NetStr over S;
N is SubRelStr of N & the mapping of N = (the mapping of N)|the carrier
of N by Th6;
hence thesis by Def6;
end;
theorem
for Q being 1-sorted, R being NetStr over Q, S being SubNetStr of R, T
being SubNetStr of S holds T is SubNetStr of R
proof
let Q be 1-sorted, R be NetStr over Q, S be SubNetStr of R, T be SubNetStr
of S;
A1: T is SubRelStr of S by Def6;
then
A2: the carrier of T c= the carrier of S by YELLOW_0:def 13;
A3: the mapping of T = (the mapping of S)|the carrier of T by Def6
.= (the mapping of R)|(the carrier of S)|the carrier of T by Def6
.= (the mapping of R)|((the carrier of S) /\ the carrier of T) by
RELAT_1:71
.= (the mapping of R)|the carrier of T by A2,XBOOLE_1:28;
S is SubRelStr of R by Def6;
then T is SubRelStr of R by A1,Th7;
hence thesis by A3,Def6;
end;
Lm4: for S being 1-sorted, R being NetStr over S holds the NetStr of R is
SubNetStr of R
proof
let S be 1-sorted, N be NetStr over S;
the NetStr of N is SubRelStr of N & the mapping of the NetStr of N = (
the mapping of N)|the carrier of the NetStr of N by YELLOW_0:def 13;
hence thesis by Def6;
end;
definition
let S be 1-sorted, N be NetStr over S, M be SubNetStr of N;
attr M is full means
:Def7:
M is full SubRelStr of N;
end;
Lm5: for S being 1-sorted, R being NetStr over S holds the NetStr of R is full
SubRelStr of R
proof
let S be 1-sorted, R be NetStr over S;
reconsider R9 = the NetStr of R as SubRelStr of R by YELLOW_0:def 13;
the InternalRel of R9 = (the InternalRel of R)|_2 the carrier of R9 by
XBOOLE_1:28;
hence thesis by YELLOW_0:def 14;
end;
registration
let S be 1-sorted, N be NetStr over S;
cluster full strict for SubNetStr of N;
existence
proof
reconsider M = the NetStr of N as SubNetStr of N by Lm4;
take M;
thus M is full SubRelStr of N by Lm5;
thus thesis;
end;
end;
registration
let S be 1-sorted, N be non empty NetStr over S;
cluster full non empty strict for SubNetStr of N;
existence
proof
reconsider M = the NetStr of N as SubNetStr of N by Lm4;
take M;
thus M is full SubRelStr of N by Lm5;
thus thesis;
end;
end;
theorem Th10:
for S being 1-sorted, N being NetStr over S, M be SubNetStr of N
holds the carrier of M c= the carrier of N
proof
let S be 1-sorted, N be NetStr over S, M be SubNetStr of N;
M is SubRelStr of N by Def6;
hence thesis by YELLOW_0:def 13;
end;
theorem Th11:
for S being 1-sorted, N being NetStr over S, M be SubNetStr of N
, x,y being Element of N, i,j being Element of M st x = i & y = j & i <= j
holds x <= y
proof
let S be 1-sorted, N be NetStr over S, M be SubNetStr of N, x,y be Element
of N, i,j be Element of M such that
A1: x = i & y = j and
A2: i <= j;
reconsider M as SubRelStr of N by Def6;
reconsider i9 = i, j9 = j as Element of M;
i9 <= j9 by A2;
hence thesis by A1,YELLOW_0:59;
end;
theorem Th12:
for S being 1-sorted, N being non empty NetStr over S, M be non
empty full SubNetStr of N, x,y being Element of N, i,j being Element of M st x
= i & y = j & x <= y holds i <= j
proof
let S be 1-sorted, N be non empty NetStr over S, M be non empty full
SubNetStr of N, x,y be Element of N, i,j be Element of M such that
A1: x = i & y = j & x <= y;
reconsider M as full non empty SubRelStr of N by Def7;
reconsider i9 = i, j9 = j as Element of M;
i9 <= j9 by A1,YELLOW_0:60;
hence thesis;
end;
begin :: More about Nets
registration
let T be non empty 1-sorted;
cluster constant strict for net of T;
existence
proof
set R = the non empty directed transitive RelStr,p = the Element of T;
take ConstantNet(R,p);
thus thesis;
end;
end;
registration
let T be non empty 1-sorted, N be constant NetStr over T;
cluster the mapping of N -> constant;
coherence by Def4;
end;
definition
let T be non empty 1-sorted, N be NetStr over T;
assume
A1: N is constant non empty;
func the_value_of N -> Element of T equals
:Def8:
the_value_of the mapping
of N;
coherence
proof
reconsider M = N as constant non empty NetStr over T by A1;
set f = the mapping of M;
ex x being set st x in dom f & the_value_of f = f.x by FUNCT_1:def 12;
then the_value_of f in rng f by FUNCT_1:def 3;
hence thesis;
end;
end;
theorem Th13:
for R be non empty RelStr, T be non empty 1-sorted, p be Element
of T holds the_value_of (ConstantNet(R,p)) = p
proof
let R be non empty RelStr, T be non empty 1-sorted, p be Element of T;
thus the_value_of (ConstantNet(R,p)) = the_value_of the mapping of
ConstantNet(R,p) by Def8
.= the_value_of ((the carrier of ConstantNet(R,p)) --> p) by Def5
.= p by FUNCOP_1:79;
end;
definition
let T be non empty 1-sorted, N be net of T;
mode subnet of N -> net of T means
:Def9:
ex f being Function of it, N st
the mapping of it = (the mapping of N)*f & for m being Element of N ex n being
Element of it st for p being Element of it st n <= p holds m <= f.p;
existence
proof
take N, id N;
thus the mapping of N = (the mapping of N)*id N by FUNCT_2:17;
let m be Element of N;
take n = m;
let p be Element of N;
assume n <= p;
hence thesis;
end;
end;
theorem
for T being non empty 1-sorted, N be net of T holds N is subnet of N
proof
let T be non empty 1-sorted, N be net of T;
take id N;
thus the mapping of N = (the mapping of N)*id N by FUNCT_2:17;
let m be Element of N;
take n = m;
let p be Element of N;
assume n <= p;
hence thesis;
end;
theorem
for T being non empty 1-sorted, N1,N2,N3 be net of T st N1 is subnet
of N2 & N2 is subnet of N3 holds N1 is subnet of N3
proof
let T be non empty 1-sorted, N1,N2,N3 be net of T;
given f being Function of N1, N2 such that
A1: the mapping of N1 = (the mapping of N2)*f and
A2: for m being Element of N2 ex n being Element of N1 st for p being
Element of N1 st n <= p holds m <= f.p;
given g being Function of N2, N3 such that
A3: the mapping of N2 = (the mapping of N3)*g and
A4: for m being Element of N3 ex n being Element of N2 st for p being
Element of N2 st n <= p holds m <= g.p;
take g*f;
thus the mapping of N1 = (the mapping of N3)*(g*f) by A1,A3,RELAT_1:36;
let m be Element of N3;
consider m1 being Element of N2 such that
A5: for p being Element of N2 st m1 <= p holds m <= g.p by A4;
consider n being Element of N1 such that
A6: for p being Element of N1 st n <= p holds m1 <= f.p by A2;
take n;
let p be Element of N1;
assume n <= p;
then m <= g.(f.p) by A5,A6;
hence thesis by FUNCT_2:15;
end;
theorem Th16:
for T being non empty 1-sorted, N be constant net of T, i being
Element of N holds N.i = the_value_of N
proof
let T be non empty 1-sorted, N be constant net of T, i be Element of N;
dom the mapping of N = the carrier of N by FUNCT_2:def 1;
hence N.i = the_value_of the mapping of N by FUNCT_1:def 12
.= the_value_of N by Def8;
end;
theorem Th17:
for L being non empty 1-sorted, N being net of L, X,Y being set
st N is_eventually_in X & N is_eventually_in Y holds X meets Y
proof
let L be non empty 1-sorted, N be net of L, X,Y be set;
assume N is_eventually_in X;
then consider i1 being Element of N such that
A1: for j being Element of N st i1 <= j holds N.j in X;
assume N is_eventually_in Y;
then consider i2 being Element of N such that
A2: for j being Element of N st i2 <= j holds N.j in Y;
consider i being Element of N such that
A3: i1 <= i and
A4: i2 <= i by Def3;
A5: N.i in Y by A2,A4;
N.i in X by A1,A3;
hence thesis by A5,XBOOLE_0:3;
end;
theorem Th18:
for S being non empty 1-sorted, N being net of S, M being subnet
of N, X st M is_often_in X holds N is_often_in X
proof
let S be non empty 1-sorted, N be net of S, M be subnet of N, X such that
A1: M is_often_in X;
let i be Element of N;
consider f being Function of M, N such that
A2: the mapping of M = (the mapping of N)*f and
A3: for m being Element of N ex n being Element of M st for p being
Element of M st n <= p holds m <= f.p by Def9;
consider n being Element of M such that
A4: for p being Element of M st n <= p holds i <= f.p by A3;
consider m being Element of M such that
A5: n <= m and
A6: M.m in X by A1;
take f.m;
thus i <= f.m by A4,A5;
thus thesis by A2,A6,FUNCT_2:15;
end;
theorem Th19:
for S being non empty 1-sorted, N being net of S, X st N
is_eventually_in X holds N is_often_in X
proof
let S be non empty 1-sorted, N be net of S, X;
given i being Element of N such that
A1: for j being Element of N st i <= j holds N.j in X;
let j be Element of N;
consider z being Element of N such that
A2: i <= z & j <= z by Def3;
take z;
thus thesis by A1,A2;
end;
theorem Th20:
for S being non empty 1-sorted, N being net of S holds N
is_eventually_in the carrier of S
proof
let S be non empty 1-sorted, N be net of S;
set i = the Element of N;
take i;
let j be Element of N;
assume i <= j;
thus thesis;
end;
begin :: The Restriction of a Net
definition
let S be 1-sorted, N be NetStr over S, X;
func N"X -> strict SubNetStr of N means
:Def10:
it is full SubRelStr of N & the carrier of it = (the mapping of N)"X;
existence
proof
set c = (the mapping of N)"X;
reconsider i = (the InternalRel of N)|_2 c as Relation of c,c;
per cases;
suppose
S is non empty;
then reconsider S as non empty 1-sorted;
set c = (the mapping of N)"X;
reconsider m = (the mapping of N)|c as Function of c,S by FUNCT_2:32;
set S = NetStr(#c,i,m#);
A1: i c= the InternalRel of N by XBOOLE_1:17;
then S is SubRelStr of N by YELLOW_0:def 13;
then reconsider S as strict SubNetStr of N by Def6;
take S;
thus thesis by A1,YELLOW_0:def 13,def 14;
end;
suppose
A2: S is empty;
then the mapping of N = {};
then c = {};
then reconsider m = {} as Function of c,S by RELSET_1:12;
set S = NetStr(#c,i,m#);
A3: the mapping of S = (the mapping of N)|the carrier of S by A2;
A4: i c= the InternalRel of N by XBOOLE_1:17;
then S is SubRelStr of N by YELLOW_0:def 13;
then reconsider S as strict SubNetStr of N by A3,Def6;
take S;
thus thesis by A4,YELLOW_0:def 13,def 14;
end;
end;
uniqueness
proof
let it1,it2 be strict SubNetStr of N such that
A5: it1 is full SubRelStr of N and
A6: the carrier of it1 = (the mapping of N)"X and
A7: it2 is full SubRelStr of N and
A8: the carrier of it2 = (the mapping of N)"X;
A9: the mapping of it1 = (the mapping of N)|the carrier of it2 by A6,A8,Def6
.= the mapping of it2 by Def6;
the RelStr of it1 = the RelStr of it2 by A5,A6,A7,A8,YELLOW_0:57;
hence thesis by A9;
end;
end;
registration
let S be 1-sorted, N be transitive NetStr over S, X;
cluster N"X -> transitive full;
coherence
proof
reconsider M = N"X as full SubRelStr of N by Def10;
M is transitive;
hence thesis;
end;
end;
theorem Th21:
for S being non empty 1-sorted, N be net of S, X st N
is_often_in X holds N"X is non empty directed
proof
let S be non empty 1-sorted, N be net of S, X such that
A1: N is_often_in X;
set i = the Element of N;
consider j being Element of N such that
i <= j and
A2: N.j in X by A1;
A3: j in (the mapping of N)"X by A2,FUNCT_2:38;
hence the carrier of N"X is non empty by Def10;
reconsider M = N"X as non empty full SubNetStr of N by A3,Def10;
M is directed
proof
let i,j be Element of M;
the carrier of M c= the carrier of N by Th10;
then reconsider x = i, y = j as Element of N;
consider z being Element of N such that
A4: x <= z & y <= z by Def3;
consider e being Element of N such that
A5: z <= e and
A6: N.e in X by A1;
e in (the mapping of N)"X by A6,FUNCT_2:38;
then reconsider k = e as Element of M by Def10;
take k;
x <= e & y <= e by A4,A5,YELLOW_0:def 2;
hence thesis by Th12;
end;
hence thesis;
end;
theorem Th22:
for S being non empty 1-sorted, N being net of S, X st N
is_often_in X holds N"X is subnet of N
proof
let S be non empty 1-sorted, N be net of S, X;
assume
A1: N is_often_in X;
then reconsider M = N"X as net of S by Th21;
M is subnet of N
proof
set f = id M;
the carrier of M c= the carrier of N by Th10;
then reconsider f as Function of M,N by FUNCT_2:7;
take f;
the mapping of M = (the mapping of N)|the carrier of M by Def6;
hence the mapping of M = (the mapping of N)*f by RELAT_1:65;
let m be Element of N;
consider j being Element of N such that
A2: m <= j and
A3: N.j in X by A1;
j in (the mapping of N)"X by A3,FUNCT_2:38;
then reconsider n = j as Element of M by Def10;
take n;
let p be Element of M such that
A4: n <= p;
j <= f.p by A4,Th11;
hence thesis by A2,YELLOW_0:def 2;
end;
hence thesis;
end;
theorem Th23:
for S being non empty 1-sorted, N being net of S, X for M being
subnet of N st M = N"X holds M is_eventually_in X
proof
let S be non empty 1-sorted, N be net of S, X;
let M be subnet of N such that
A1: M = N"X;
set i = the Element of M;
take i;
let j be Element of M such that
i <= j;
j in the carrier of M;
then j in (the mapping of N)"X by A1,Def10;
then
A2: (the mapping of N).j in X by FUNCT_1:def 7;
the mapping of M = (the mapping of N)|the carrier of M by A1,Def6;
hence thesis by A2,FUNCT_1:49;
end;
begin :: The Universe of Nets
definition
let X be non empty 1-sorted;
func NetUniv X -> set means
:Def11:
for x being object holds x in it iff ex N being strict net
of X st N = x & the carrier of N in the_universe_of the carrier of X;
existence
proof
deffunc f(set) = { NetStr(#$1,r,f#) where r is Relation of $1,$1, f is
Element of Funcs($1, the carrier of X) : NetStr(#$1,r,f#) is net of X };
set I = the_universe_of the carrier of X;
consider M being ManySortedSet of I such that
A1: for i being set st i in I holds M.i = f(i) from PBOOLE:sch 7;
take IT = Union M;
let x be object;
A2: Union M = union rng M by CARD_3:def 4;
hereby
assume x in IT;
then consider y such that
A3: x in y and
A4: y in rng M by A2,TARSKI:def 4;
consider z being object such that
A5: z in dom M and
A6: M.z = y by A4,FUNCT_1:def 3;
reconsider z as set by TARSKI:1;
z in I by A5;
then y ={ NetStr(#z,r,f#) where r is Relation of z,z, f is Element of
Funcs(z, the carrier of X) : NetStr(#z,r,f#) is net of X } by A1,A6;
then consider r being Relation of z,z, f being Element of Funcs(z, the
carrier of X) such that
A7: x = NetStr(#z,r,f#) and
A8: NetStr(#z,r,f#) is net of X by A3;
reconsider N = NetStr(#z,r,f#) as strict net of X by A8;
take N;
thus N = x by A7;
thus the carrier of N in the_universe_of the carrier of X by A5;
end;
given N being strict net of X such that
A9: N = x and
A10: the carrier of N in the_universe_of the carrier of X;
set i = the carrier of N;
i in dom M by A10,PARTFUN1:def 2;
then
A11: M.i in rng M by FUNCT_1:def 3;
A12: the mapping of N in Funcs(i, the carrier of X) by FUNCT_2:8;
M.i = { NetStr(#i,r,f#) where r is Relation of i,i, f is Element of
Funcs(i, the carrier of X) : NetStr(#i,r,f#) is net of X } by A1,A10;
then N in M.i by A12;
hence thesis by A2,A9,A11,TARSKI:def 4;
end;
uniqueness
proof
defpred P[object] means
ex N being strict net of X st N = $1 & the carrier of
N in the_universe_of the carrier of X;
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
registration
let X be non empty 1-sorted;
cluster NetUniv X -> non empty;
coherence
proof
{} in {{}} by TARSKI:def 1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(#{{}},r#);
A1: now
let x,y be Element of R;
x = {} & y = {} by TARSKI:def 1;
then [x,y] in {[{},{}]} by TARSKI:def 1;
hence x <= y by ORDERS_2:def 5;
end;
A2: R is transitive
by A1;
R is directed
proof
let x,y be Element of R;
take x;
thus thesis by A1;
end;
then reconsider R as transitive directed non empty RelStr by A2;
set V = the_universe_of the carrier of X;
set q = the Element of X;
set N = ConstantNet(R,q);
the RelStr of N = the RelStr of R & {} in V by Def5,CLASSES2:56;
then the carrier of N in V by CLASSES2:2;
hence thesis by Def11;
end;
end;
Lm6: for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of
S2 for N being constant net of S1 holds N is constant net of S2
proof
let S1,S2 be non empty 1-sorted such that
A1: the carrier of S1 = the carrier of S2;
let N be constant net of S1;
reconsider M = N as net of S2 by A1;
the mapping of N is constant;
then the mapping of M is constant;
hence thesis by Def4;
end;
Lm7: for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of
S2 holds NetUniv S1 = NetUniv S2
proof
let S1,S2 be non empty 1-sorted;
defpred P[object] means
ex N being strict net of S2 st N = $1 & the carrier of
N in the_universe_of the carrier of S2;
assume
A1: the carrier of S1 = the carrier of S2;
A2: now
let x be object;
hereby
assume x in NetUniv S1;
then consider N being strict net of S1 such that
A3: N = x & the carrier of N in the_universe_of the carrier of S1 by Def11;
reconsider N as strict net of S2 by A1;
thus P[x]
proof
take N;
thus thesis by A1,A3;
end;
end;
assume P[x];
then consider N being strict net of S2 such that
A4: N = x & the carrier of N in the_universe_of the carrier of S2;
reconsider N as strict net of S1 by A1;
now
take N;
thus N = x & the carrier of N in the_universe_of the carrier of S1 by A1
,A4;
end;
hence x in NetUniv S1 by Def11;
end;
A5: for x being object holds x in NetUniv S2 iff P[x] by Def11;
thus NetUniv S1 = NetUniv S2 from XBOOLE_0:sch 2(A2,A5);
end;
begin :: Parametrized Families of Nets, Iteration
definition
let X be set, T be 1-sorted;
mode net_set of X,T -> ManySortedSet of X means
:Def12:
for i being set st i in rng it holds i is net of T;
existence
proof
set N = the net of T;
take X --> N;
let i be set;
assume i in rng(X --> N);
hence thesis by TARSKI:def 1;
end;
end;
theorem Th24:
for X being set, T being 1-sorted, F being ManySortedSet of X
holds F is net_set of X,T iff for i being set st i in X holds F.i is net of T
proof
let X be set, T be 1-sorted, F be ManySortedSet of X;
hereby
assume
A1: F is net_set of X,T;
let i be set;
assume i in X;
then i in dom F by PARTFUN1:def 2;
then F.i in rng F by FUNCT_1:def 3;
hence F.i is net of T by A1,Def12;
end;
assume
A2: for i being set st i in X holds F.i is net of T;
let x be set;
assume x in rng F;
then ex i being object st i in dom F & x = F.i by FUNCT_1:def 3;
hence thesis by A2;
end;
definition
let X be non empty set, T be 1-sorted;
let J be net_set of X,T, i be Element of X;
redefine func J.i -> net of T; :: redefines . (FUNCT_1, definition)
coherence by Th24;
end;
registration
let X be set, T be 1-sorted;
cluster -> RelStr-yielding for net_set of X,T;
coherence
proof
let F be net_set of X,T;
let v be set;
assume v in rng F;
hence thesis by Def12;
end;
end;
registration
let T be 1-sorted, Y be net of T;
cluster -> yielding_non-empty_carriers for net_set of the carrier of Y,T;
coherence
by Def12;
end;
registration
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T;
cluster product J -> directed transitive;
coherence
proof
A1: the carrier of product J = product Carrier J by YELLOW_1:def 4;
thus product J is directed
proof
let x,y be Element of product J;
defpred P[Element of Y,object] means
[x .$1,$2] in the InternalRel of J.$1
& [y.$1,$2] in the InternalRel of J.$1;
A2: now
let i be Element of Y;
consider zi being Element of J.i such that
A3: x .i <= zi & y.i <= zi by Def3;
reconsider z = zi as object;
take z;
thus P[i,z] by A3,ORDERS_2:def 5;
end;
consider z being ManySortedSet of the carrier of Y such that
A4: for i being Element of Y holds P[i, z.i] from PBOOLE:sch 6(A2);
A5: now
let i be object;
assume i in dom Carrier J;
then reconsider j = i as Element of Y;
[x .j,z.j] in the InternalRel of J.j by A4;
then z.j in the carrier of J.j by ZFMISC_1:87;
hence z.i in (Carrier J).i by Th2;
end;
dom z = the carrier of Y by PARTFUN1:def 2
.= dom Carrier J by PARTFUN1:def 2;
then reconsider z as Element of product J by A1,A5,CARD_3:9;
take z;
for i be object st i in the carrier of Y ex R being RelStr, xi,yi
being Element of R st R = J.i & xi = x .i & yi = z.i & xi <= yi
proof
let i be object;
assume i in the carrier of Y;
then reconsider j = i as Element of Y;
reconsider xi = x .j, zi = z.j as Element of J.j;
take J.j, xi, zi;
thus J.j = J.i & xi = x .i & zi = z.i;
[xi,zi] in the InternalRel of J.j by A4;
hence thesis by ORDERS_2:def 5;
end;
hence x <= z by A1,YELLOW_1:def 4;
for i be object st i in the carrier of Y ex R being RelStr, yi,zi
being Element of R st R = J.i & yi = y.i & zi = z.i & yi <= zi
proof
let i be object;
assume i in the carrier of Y;
then reconsider j = i as Element of Y;
reconsider yi = y.j, zi = z.j as Element of J.j;
take J.j, yi, zi;
thus J.j = J.i & yi = y.i & zi = z.i;
[yi,zi] in the InternalRel of J.j by A4;
hence thesis by ORDERS_2:def 5;
end;
hence thesis by A1,YELLOW_1:def 4;
end;
let x,y,z be Element of product J such that
A6: x <= y and
A7: y <= z;
A8: ex fy,gz being Function st fy = y & gz = z &
for i be object st i in the
carrier of Y ex R being RelStr, xi,yi being Element of R st R = J.i & xi = fy.i
& yi = gz.i & xi <= yi by A1,A7,YELLOW_1:def 4;
A9: ex fx,gy being Function st fx = x & gy = y &
for i be object st i in the
carrier of Y ex R being RelStr, xi,yi being Element of R st R = J.i & xi = fx.i
& yi = gy.i & xi <= yi by A1,A6,YELLOW_1:def 4;
for i be object st i in the carrier of Y ex R being RelStr, xi,yi being
Element of R st R = J.i & xi = x .i & yi = z.i & xi <= yi
proof
let i be object;
assume
A10: i in the carrier of Y;
then reconsider j = i as Element of Y;
consider R1 being RelStr, xi,yi being Element of R1 such that
A11: R1 = J.i and
A12: xi = x .i and
A13: yi = y.i & xi <= yi by A9,A10;
consider R2 being RelStr, yi9,zi being Element of R2 such that
A14: R2 = J.i and
A15: yi9 = y.i and
A16: zi = z.i and
A17: yi9 <= zi by A8,A10;
reconsider xi, zi as Element of J.j by A11,A14;
take J.j, xi, zi;
thus J.j = J.i & xi = x .i & zi = z.i by A12,A16;
thus thesis by A11,A13,A14,A15,A17,YELLOW_0:def 2;
end;
hence thesis by A1,YELLOW_1:def 4;
end;
end;
registration
let X be set, T be 1-sorted;
cluster -> yielding_non-empty_carriers for net_set of X,T;
coherence
by Def12;
end;
registration
let X be set, T be 1-sorted;
cluster yielding_non-empty_carriers for net_set of X,T;
existence
proof
set F = the net_set of X,T;
take F;
thus thesis;
end;
end;
definition
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T;
func Iterated J -> strict net of T means
:Def13:
the RelStr of it = [:Y,
product J:] & for i being Element of Y, f being Function st i in the carrier of
Y & f in the carrier of product J holds (the mapping of it).(i,f) =(the mapping
of J.i).(f.i);
existence
proof
deffunc F(Element of Y, Element of product J) = (the mapping of J.$1).($2.
$1);
set R = [:Y, product J:];
A1: for i be Element of Y, f be Element of product J holds F(i,f) in the
carrier of T;
consider F being Function of [:the carrier of Y, the carrier of product J
:], T such that
A2: for i being Element of Y, f being Element of product J holds F.(i,
f) = F(i,f) from FUNCT_7:sch 1(A1);
the carrier of R = [:the carrier of Y, the carrier of product J:] by
YELLOW_3:def 2;
then reconsider F as Function of R,T;
reconsider N = NetStr(#the carrier of R, the InternalRel of R,F#) as
strict net of T by Lm1,Lm2;
take N;
thus the RelStr of N = [:Y, product J:];
let i be Element of Y, f be Function such that
i in the carrier of Y and
A3: f in the carrier of product J;
thus thesis by A2,A3;
end;
uniqueness
proof
let IT1,IT2 be strict net of T such that
A4: the RelStr of IT1 = [:Y, product J:] and
A5: for i being Element of Y, f being Function st i in the carrier of
Y & f in the carrier of product J holds (the mapping of IT1).(i,f) =(the
mapping of J.i).(f.i) and
A6: the RelStr of IT2 = [:Y, product J:] and
A7: for i being Element of Y, f being Function st i in the carrier of
Y & f in the carrier of product J holds (the mapping of IT2).(i,f) =(the
mapping of J.i).(f.i);
the carrier of the RelStr of IT2 = [:the carrier of Y,the carrier of
product J:] by A6,YELLOW_3:def 2;
then reconsider
m1 = the mapping of IT1, m2 = the mapping of IT2 as Function of
[:the carrier of Y,the carrier of product J:], T by A4,A6;
now
let c be Element of [:the carrier of Y,the carrier of product J:];
consider c1 being Element of Y, c2 being Element of product J such that
A8: c = [c1,c2] by DOMAIN_1:1;
reconsider d = c2 as Element of product Carrier J by YELLOW_1:def 4;
thus m1.c = m1.(c1,d) by A8
.= (the mapping of J.c1).(d.c1) by A5
.= m2.(c1,d) by A7
.= m2.c by A8;
end;
hence thesis by A4,A6,FUNCT_2:63;
end;
end;
theorem Th25:
for T being non empty 1-sorted, Y being net of T, J being
net_set of the carrier of Y,T st Y in NetUniv T & for i being Element of Y
holds J.i in NetUniv T holds Iterated J in NetUniv T
proof
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T such that
A1: Y in NetUniv T and
A2: for i being Element of Y holds J.i in NetUniv T;
A3: rng Carrier J c= the_universe_of the carrier of T
proof
let x be object;
assume x in rng Carrier J;
then consider y being object such that
A4: y in dom Carrier J and
A5: (Carrier J).y = x by FUNCT_1:def 3;
reconsider i = y as Element of Y by A4;
J.i in NetUniv T by A2;
then ex N being strict net of T st N = J.i & the carrier of N in
the_universe_of the carrier of T by Def11;
hence thesis by A5,Th2;
end;
the RelStr of Iterated J = [:Y, product J:] by Def13;
then
A6: the carrier of Iterated J = [:the carrier of Y, the carrier of product J
:] by YELLOW_3:def 2;
A7: ex N being strict net of T st N = Y & the carrier of N in
the_universe_of the carrier of T by A1,Def11;
then dom Carrier J in the_universe_of the carrier of T by PARTFUN1:def 2;
then product Carrier J in the_universe_of the carrier of T by A3,Th1;
then the carrier of product J in the_universe_of the carrier of T by
YELLOW_1:def 4;
then
the carrier of Iterated J in the_universe_of the carrier of T by A6,A7,
CLASSES2:61;
hence thesis by Def11;
end;
theorem Th26:
for T being non empty 1-sorted, N being net of T for J being
net_set of the carrier of N, T holds the carrier of Iterated J = [:the carrier
of N, product Carrier J:]
proof
let T be non empty 1-sorted, N be net of T;
let J be net_set of the carrier of N, T;
the RelStr of Iterated J = [:N, product J:] by Def13;
hence the carrier of Iterated J = [:the carrier of N, the carrier of product
J:] by YELLOW_3:def 2
.= [:the carrier of N, product Carrier J:] by YELLOW_1:def 4;
end;
theorem Th27:
for T being non empty 1-sorted, N being net of T, J being
net_set of the carrier of N, T, i being Element of N, f being Element of
product J, x being Element of Iterated J st x = [i,f] holds (Iterated J).x = (
the mapping of J.i).(f.i)
proof
let T be non empty 1-sorted, N be net of T, J be net_set of the carrier of N
, T, i be Element of N, f be Element of product J, x be Element of Iterated J;
assume x = [i,f];
hence (Iterated J).x = (the mapping of Iterated J).(i,f)
.= (the mapping of J.i).(f.i) by Def13;
end;
theorem Th28:
for T being non empty 1-sorted, Y being net of T, J being
net_set of the carrier of Y,T holds rng the mapping of Iterated J c= union
the set of all
rng the mapping of J.i where i is Element of Y
proof
let T be non empty 1-sorted, Y be net of T, J be net_set of the carrier of Y
,T;
let x be object;
set X = the set of all rng the mapping of J.i where i is Element of Y;
assume x in rng the mapping of Iterated J;
then consider y being object such that
A1: y in dom the mapping of Iterated J and
A2: (the mapping of Iterated J).y = x by FUNCT_1:def 3;
y in the carrier of Iterated J by A1;
then y in [:the carrier of Y, product Carrier J:] by Th26;
then consider
y1 being Element of Y, y2 being Element of product Carrier J such
that
A3: y = [y1,y2] by DOMAIN_1:1;
y1 in the carrier of Y;
then y1 in dom Carrier J by PARTFUN1:def 2;
then y2.y1 in (Carrier J).y1 by CARD_3:9;
then y2.y1 in the carrier of J.y1 by Th2;
then
A4: y2.y1 in dom the mapping of J.y1 by FUNCT_2:def 1;
y2 in product Carrier J;
then
A5: y2 in the carrier of product J by YELLOW_1:def 4;
x = (the mapping of Iterated J).(y1,y2) by A2,A3
.= (the mapping of J.y1).(y2.y1) by A5,Def13;
then
A6: x in rng the mapping of J.y1 by A4,FUNCT_1:def 3;
reconsider y1 as Element of Y;
rng the mapping of J.y1 in X;
hence thesis by A6,TARSKI:def 4;
end;
begin :: Poset of open neighborhoods
definition
let T be non empty TopSpace, p be Point of T;
func OpenNeighborhoods p -> RelStr equals
(InclPoset { V where V is Subset
of T: p in V & V is open })~;
correctness;
end;
registration
let T be non empty TopSpace, p be Point of T;
cluster OpenNeighborhoods p -> non empty;
coherence
proof
set Xp = { v where v is Subset of T: p in v & v is open };
[#]T in the carrier of InclPoset Xp;
hence the carrier of OpenNeighborhoods p is non empty;
end;
end;
theorem Th29:
for T being non empty TopSpace, p being Point of T, x being
Element of OpenNeighborhoods p ex W being Subset of T st W = x & p in W & W is
open
proof
let T be non empty TopSpace, p be Point of T, x be Element of
OpenNeighborhoods p;
set X = { V where V is Subset of T: p in V & V is open };
x in the carrier of (InclPoset X)~;
then x in the carrier of InclPoset X by Th3;
hence thesis;
end;
theorem Th30:
for T be non empty TopSpace, p be Point of T for x being Subset
of T holds x in the carrier of OpenNeighborhoods p iff p in x & x is open
proof
let T be non empty TopSpace, p be Point of T;
let x be Subset of T;
set Xp = { v where v is Subset of T: p in v & v is open };
reconsider i = x as Subset of T;
thus x in the carrier of OpenNeighborhoods p implies p in x & x is open
proof
assume x in the carrier of OpenNeighborhoods p;
then ex v being Subset of T st i = v & p in v & v is open by Th29;
hence thesis;
end;
assume p in x & x is open;
then x in the carrier of InclPoset Xp;
hence thesis by Th3;
end;
theorem Th31:
for T be non empty TopSpace, p be Point of T for x,y being
Element of OpenNeighborhoods p holds x <= y iff y c= x
proof
let T be non empty TopSpace, p be Point of T;
set X = { V where V is Subset of T: p in V & V is open };
[#]T in X;
then reconsider X as non empty set;
let x,y be Element of OpenNeighborhoods p;
(InclPoset X)~ = RelStr(#the carrier of InclPoset X, (the InternalRel of
InclPoset X)~#) by LATTICE3:def 5;
then reconsider a = x, b = y as Element of InclPoset X;
A1: b <= a iff y c= x by YELLOW_1:3;
x = a~ & y = b~ by LATTICE3:def 6;
hence thesis by A1,LATTICE3:9;
end;
registration
let T be non empty TopSpace, p be Point of T;
cluster OpenNeighborhoods p -> transitive directed;
coherence
proof
thus OpenNeighborhoods p is transitive;
let x,y be Element of OpenNeighborhoods p;
set X = { V where V is Subset of T: p in V & V is open };
consider V being Subset of T such that
A1: x = V and
A2: p in V & V is open by Th29;
consider W being Subset of T such that
A3: y = W and
A4: p in W & W is open by Th29;
set z = V /\ W;
p in z & z is open by A2,A4,XBOOLE_0:def 4;
then z in X;
then reconsider z as Element of OpenNeighborhoods p by Th3;
A5: z c= y by A3,XBOOLE_1:17;
take z;
z c= x by A1,XBOOLE_1:17;
hence thesis by A5,Th31;
end;
end;
begin :: Nets in topological spaces
definition
let T be non empty TopSpace, N be net of T;
defpred P[Point of T] means for V being a_neighborhood of $1 holds N
is_eventually_in V;
func Lim N -> Subset of T means
:Def15:
for p being Point of T holds p in it
iff for V being a_neighborhood of p holds N is_eventually_in V;
existence
proof
consider IT being Subset of T such that
A1: for p being Point of T holds p in IT iff P[p] from SUBSET_1:sch 3;
take IT;
let p be Point of T;
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be Subset of T such that
A2: for p being Point of T holds p in it1 iff P[p] and
A3: for p being Point of T holds p in it2 iff P[p];
thus thesis from SUBSET_1:sch 4(A2,A3);
end;
end;
theorem Th32:
for T being non empty TopSpace, N being net of T, Y being subnet
of N holds Lim N c= Lim Y
proof
let T be non empty TopSpace, N be net of T, Y be subnet of N;
let x be object;
consider f being Function of Y, N such that
A1: the mapping of Y = (the mapping of N)*f and
A2: for m being Element of N ex n being Element of Y st for p being
Element of Y st n <= p holds m <= f.p by Def9;
assume
A3: x in Lim N;
then reconsider p = x as Point of T;
for V being a_neighborhood of p holds Y is_eventually_in V
proof
let V be a_neighborhood of p;
N is_eventually_in V by A3,Def15;
then consider ii being Element of N such that
A4: for j being Element of N st ii <= j holds N.j in V;
consider n being Element of Y such that
A5: for p being Element of Y st n <= p holds ii <= f.p by A2;
take n;
let j be Element of Y;
assume
A6: n <= j;
N.(f.j) = Y.j by A1,FUNCT_2:15;
hence thesis by A4,A5,A6;
end;
hence thesis by Def15;
end;
theorem Th33:
for T being non empty TopSpace, N be constant net of T holds
the_value_of N in Lim N
proof
let T be non empty TopSpace, N be constant net of T;
set p = the_value_of N;
for S being a_neighborhood of p holds N is_eventually_in S
proof
set i = the Element of N;
let S be a_neighborhood of p;
take i;
let j be Element of N such that
i <= j;
N.j = p by Th16;
hence thesis by CONNSP_2:4;
end;
hence thesis by Def15;
end;
theorem Th34:
for T being non empty TopSpace, N be net of T, p be Point of T
st p in Lim N for d being Element of N ex S being Subset of T st S = { N.c
where c is Element of N : d <= c } & p in Cl S
proof
let T be non empty TopSpace, N be net of T, p be Point of T such that
A1: p in Lim N;
let d be Element of N;
{ N.c where c is Element of N : d <= c } c= the carrier of T
proof
let x be object;
assume x in { N.c where c is Element of N : d <= c };
then ex c being Element of N st x = N.c & d <= c;
hence thesis;
end;
then reconsider S = { N.c where c is Element of N : d <= c } as Subset of T;
take S;
thus S = { N.c where c is Element of N : d <= c };
now
let G be a_neighborhood of p;
N is_eventually_in G by A1,Def15;
then consider i being Element of N such that
A2: for j being Element of N st i <= j holds N.j in G;
consider e being Element of N such that
A3: d <= e and
A4: i <= e by Def3;
A5: N.e in S by A3;
N.e in G by A2,A4;
hence G meets S by A5,XBOOLE_0:3;
end;
hence thesis by CONNSP_2:27;
end;
theorem Th35:
for T being non empty TopSpace holds T is Hausdorff iff for N
being net of T, p,q being Point of T st p in Lim N & q in Lim N holds p = q
proof
let T be non empty TopSpace;
thus T is Hausdorff implies for N being net of T, p,q being Point of T st p
in Lim N & q in Lim N holds p = q
proof
assume
A1: T is Hausdorff;
let N be net of T;
given p1,p2 being Point of T such that
A2: p1 in Lim N and
A3: p2 in Lim N and
A4: p1 <> p2;
consider W,V being Subset of T such that
A5: W is open and
A6: V is open and
A7: p1 in W and
A8: p2 in V and
A9: W misses V by A1,A4;
V is a_neighborhood of p2 by A6,A8,CONNSP_2:3;
then
A10: N is_eventually_in V by A3,Def15;
W is a_neighborhood of p1 by A5,A7,CONNSP_2:3;
then N is_eventually_in W by A2,Def15;
hence contradiction by A9,A10,Th17;
end;
assume
A11: for N being net of T, p,q being Point of T st p in Lim N & q in Lim
N holds p = q;
given p,q be Point of T such that
A12: p <> q and
A13: for W,V being Subset of T st W is open & V is open & p in W & q in
V holds W meets V;
set pN = [:OpenNeighborhoods p,OpenNeighborhoods q:];
set cT = the carrier of T, cpN = the carrier of pN;
deffunc F(Element of cpN) = $1`1 /\ $1`2;
A14: for i being Element of cpN holds cT meets F(i)
proof
let i be Element of cpN;
consider W being Subset of T such that
A15: W = i`1 and
A16: p in W & W is open by Th29;
consider V being Subset of T such that
A17: V = i`2 and
A18: q in V & V is open by Th29;
i`1 meets i`2 by A13,A15,A16,A17,A18;
then W /\ V c= cT & i`1 /\ i`2 <> {} by XBOOLE_0:def 7;
then cT /\ (i`1 /\ i`2) <> {} by A15,A17,XBOOLE_1:28;
hence thesis by XBOOLE_0:def 7;
end;
consider f being Function of cpN, cT such that
A19: for i being Element of cpN holds f.i in F(i) from FUNCT_2:sch 10(
A14);
reconsider N = NetStr(#the carrier of pN, the InternalRel of pN, f#) as net
of T by Lm1,Lm2;
A20: cpN = [:the carrier of OpenNeighborhoods p, the carrier of
OpenNeighborhoods q:] by YELLOW_3:def 2;
now
let V be a_neighborhood of q;
A21: N is_eventually_in Int V
proof
A22: [#]T in the carrier of OpenNeighborhoods p by Th30;
q in Int V & Int V is open by CONNSP_2:def 1;
then Int V in the carrier of OpenNeighborhoods q by Th30;
then reconsider i = [[#]T,Int V] as Element of N by A20,A22,ZFMISC_1:87;
take i;
let j be Element of N;
reconsider j9=j, i9=i as Element of pN;
consider j1 being Element of OpenNeighborhoods p, j2 being Element of
OpenNeighborhoods q such that
A23: j = [j1,j2] by A20,DOMAIN_1:1;
A24: j`2 = j2 by A23;
consider W1 being Subset of T such that
A25: j1 = W1 and
p in W1 and
W1 is open by Th29;
consider W2 being Subset of T such that
A26: j2 = W2 and
q in W2 and
W2 is open by Th29;
assume i <= j;
then [i,j] in the InternalRel of pN by ORDERS_2:def 5;
then i9 <= j9 by ORDERS_2:def 5;
then i9`2 = Int V & i9`2 <= j9`2 by YELLOW_3:12;
then W2 c= Int V by A24,A26,Th31;
then
A27: W1 /\ W2 c= (Int V) /\ [#]T by XBOOLE_1:27;
j`1 = j1 by A23;
then f.j in W1 /\ W2 by A19,A24,A25,A26;
then f.j in (Int V) /\ [#]T by A27;
hence thesis by XBOOLE_1:28;
end;
Int V c= V by TOPS_1:16;
hence N is_eventually_in V by A21,WAYBEL_0:8;
end;
then
A28: q in Lim N by Def15;
now
let V be a_neighborhood of p;
A29: N is_eventually_in Int V
proof
A30: [#]T in the carrier of OpenNeighborhoods q by Th30;
p in Int V & Int V is open by CONNSP_2:def 1;
then Int V in the carrier of OpenNeighborhoods p by Th30;
then reconsider i = [Int V,[#]T] as Element of N by A20,A30,ZFMISC_1:87;
take i;
let j be Element of N;
reconsider j9=j, i9=i as Element of pN;
consider j1 being Element of OpenNeighborhoods p, j2 being Element of
OpenNeighborhoods q such that
A31: j = [j1,j2] by A20,DOMAIN_1:1;
A32: j`1 = j1 by A31;
consider W2 being Subset of T such that
A33: j2 = W2 and
q in W2 and
W2 is open by Th29;
consider W1 being Subset of T such that
A34: j1 = W1 and
p in W1 and
W1 is open by Th29;
assume i <= j;
then [i,j] in the InternalRel of pN by ORDERS_2:def 5;
then i9 <= j9 by ORDERS_2:def 5;
then i9`1 = Int V & i9`1 <= j9`1 by YELLOW_3:12;
then W1 c= Int V by A32,A34,Th31;
then
A35: W1 /\ W2 c= (Int V) /\ [#]T by XBOOLE_1:27;
j`2 = j2 by A31;
then f.j in W1 /\ W2 by A19,A32,A34,A33;
then f.j in (Int V) /\ [#]T by A35;
hence thesis by XBOOLE_1:28;
end;
Int V c= V by TOPS_1:16;
hence N is_eventually_in V by A29,WAYBEL_0:8;
end;
then p in Lim N by Def15;
hence contradiction by A11,A12,A28;
end;
registration
let T be Hausdorff non empty TopSpace, N be net of T;
cluster Lim N -> trivial;
coherence
proof
for p,q being Point of T st p in Lim N & q in Lim N holds p = q by Th35;
hence thesis by SUBSET_1:45;
end;
end;
definition
let T be non empty TopSpace, N be net of T;
attr N is convergent means
:Def16:
Lim N <> {};
end;
registration
let T be non empty TopSpace;
cluster constant -> convergent for net of T;
coherence
by Th33;
end;
registration
let T be non empty TopSpace;
cluster convergent strict for net of T;
existence
proof
set R = the non empty transitive directed RelStr,p = the Point of T;
take ConstantNet(R,p);
thus thesis;
end;
end;
definition
let T be Hausdorff non empty TopSpace, N be convergent net of T;
func lim N -> Element of T means
:Def17:
it in Lim N;
existence
by Def16,SUBSET_1:4;
correctness by ZFMISC_1:def 10;
end;
theorem
for T be Hausdorff non empty TopSpace, N be constant net of T holds
lim N = the_value_of N
proof
let T be Hausdorff non empty TopSpace, N be constant net of T;
the_value_of N in Lim N by Th33;
hence thesis by Def17;
end;
theorem
for T being non empty TopSpace, N being net of T for p being Point of
T st not p in Lim N ex Y being subnet of N st not ex Z being subnet of Y st p
in Lim Z
proof
let T be non empty TopSpace, N be net of T;
let p be Point of T;
assume not p in Lim N;
then consider V be a_neighborhood of p such that
A1: not N is_eventually_in V by Def15;
N is_often_in (the carrier of T) \ V by A1,WAYBEL_0:9;
then reconsider Y = N"((the carrier of T) \ V) as subnet of N by Th22;
take Y;
let Z be subnet of Y;
assume p in Lim Z;
then Z is_eventually_in V by Def15;
then
A2: Y is_often_in V by Th18,Th19;
Y is_eventually_in (the carrier of T) \ V by Th23;
hence contradiction by A2,WAYBEL_0:10;
end;
theorem Th38:
for T being non empty TopSpace, N being net of T st N in NetUniv
T for p being Point of T st not p in Lim N ex Y being subnet of N st Y in
NetUniv T & not ex Z being subnet of Y st p in Lim Z
proof
let T be non empty TopSpace, N be net of T;
assume N in NetUniv T;
then
A1: ex M being strict net of T st M = N & the carrier of M in
the_universe_of the carrier of T by Def11;
let p be Point of T;
assume not p in Lim N;
then consider V be a_neighborhood of p such that
A2: not N is_eventually_in V by Def15;
N is_often_in (the carrier of T) \ V by A2,WAYBEL_0:9;
then reconsider Y = N"((the carrier of T) \ V) as subnet of N by Th22;
take Y;
the carrier of Y = (the mapping of N)"((the carrier of T) \ V) by Def10;
then the carrier of Y in the_universe_of the carrier of T by A1,
CLASSES1:def 1;
hence Y in NetUniv T by Def11;
let Z be subnet of Y;
assume p in Lim Z;
then Z is_eventually_in V by Def15;
then
A3: Y is_often_in V by Th18,Th19;
Y is_eventually_in (the carrier of T) \ V by Th23;
hence contradiction by A3,WAYBEL_0:10;
end;
theorem Th39:
for T being non empty TopSpace, N being net of T, p being Point
of T st p in Lim N for J being net_set of the carrier of N, T st for i being
Element of N holds N.i in Lim(J.i) holds p in Lim Iterated J
proof
let T be non empty TopSpace, N be net of T, p be Point of T such that
A1: p in Lim N;
let J be net_set of the carrier of N, T such that
A2: for i being Element of N holds N.i in Lim(J.i);
for V being a_neighborhood of p holds Iterated J is_eventually_in V
proof
let V be a_neighborhood of p;
p in Int Int V by CONNSP_2:def 1;
then reconsider W = Int V as a_neighborhood of p by CONNSP_2:def 1;
N is_eventually_in W by A1,Def15;
then consider i being Element of N such that
A3: for j being Element of N st i <= j holds N.j in W;
defpred P[Element of N,object] means
ex m being Element of J.$1 st m = $2 & (
i <= $1 implies for n being Element of J.$1 st m <= n holds J.$1.n in W);
A4: Int V = Int Int V;
A5: for j being Element of N ex e being object st P[j, e]
proof
let j be Element of N;
reconsider j9 = j as Element of N;
per cases;
suppose
i <= j;
then N.j9 in W by A3;
then
A6: W is a_neighborhood of N.j by A4,CONNSP_2:def 1;
N.j in Lim(J.j) by A2;
then J.j is_eventually_in W by A6,Def15;
then consider e being Element of J.j such that
A7: for u being Element of J.j st e <= u holds J.j.u in W;
take e,e;
thus e = e;
assume i <= j;
thus thesis by A7;
end;
suppose
A8: not i <= j;
set e = the Element of J.j;
take e,e;
thus thesis by A8;
end;
end;
consider f being ManySortedSet of the carrier of N such that
A9: for j being Element of N holds P[j, f.j] from PBOOLE:sch 6(A5);
A10: for x being object st x in dom Carrier J holds f.x in (Carrier J).x
proof
let x be object;
assume x in dom Carrier J;
then reconsider j = x as Element of N;
ex m being Element of J.j st m = f.j & (i <= j implies for n being
Element of J.j st m <= n holds J.j.n in W) by A9;
then f.x in the carrier of J.j;
hence thesis by Th2;
end;
dom Carrier J = the carrier of N by PARTFUN1:def 2;
then dom f = dom Carrier J by PARTFUN1:def 2;
then
A11: f in product Carrier J by A10,CARD_3:9;
A12: the carrier of Iterated J = [:the carrier of N, product Carrier J:]
by Th26;
then reconsider x = [i,f] as Element of Iterated J by A11,ZFMISC_1:87;
take x;
let j be Element of Iterated J such that
A13: x <= j;
consider j1 being Element of N, j2 being Element of product Carrier J such
that
A14: j = [j1,j2] by A12,DOMAIN_1:1;
reconsider j2, i2 = f as Element of product J by A11,YELLOW_1:def 4;
reconsider i1 = i, j1 as Element of N;
i2 in the carrier of product J;
then
A15: i2 in product Carrier J by YELLOW_1:def 4;
the RelStr of Iterated J = [:N, product J:] by Def13;
then
A16: [i1,i2] <= [j1,j2] by A13,A14,YELLOW_0:1;
then i2 <= j2 by YELLOW_3:11;
then ex f,g being Function st f = i2 & g = j2 &
for i be object st i in the
carrier of N ex R being RelStr, xi,yi being Element of R st R = J.i & xi = f.i
& yi = g.i & xi <= yi by A15,YELLOW_1:def 4;
then
A17: ex R being RelStr, xi,yi being Element of R st R = J.j1 & xi = i2.j1
& yi = j2.j1 & xi <= yi;
ex m being Element of J.j1 st m = f.j1 &( i <= j1 implies for n being
Element of J.j1 st m <= n holds J.j1.n in W) by A9;
then (J.j1).(j2.j1) in W by A16,A17,YELLOW_3:11;
then
A18: (Iterated J).j in W by A14,Th27;
W c= V by TOPS_1:16;
hence thesis by A18;
end;
hence thesis by Def15;
end;
begin :: Convergence Classes
definition
let S be non empty 1-sorted;
mode Convergence-Class of S -> set means
:Def18:
it c= [:NetUniv S,the carrier of S :];
existence;
end;
registration
let S be non empty 1-sorted;
cluster -> Relation-like for Convergence-Class of S;
coherence
proof
let C be Convergence-Class of S;
C is Subset of [:NetUniv S,the carrier of S:] by Def18;
hence thesis;
end;
end;
definition
let T be non empty TopSpace;
func Convergence T -> Convergence-Class of T means
:Def19:
for N being net
of T, p being Point of T holds [N,p] in it iff N in NetUniv T & p in Lim N;
existence
proof
defpred P[object,object] means
ex N being net of T, p being Point of T st N = $1
& p = $2 & p in Lim N;
consider R being Relation of NetUniv T, the carrier of T such that
A1: for x,y being object
holds [x,y] in R iff x in NetUniv T & y in the carrier of
T & P[x,y] from RELSET_1:sch 1;
reconsider R as Convergence-Class of T by Def18;
take R;
let N be net of T, p be Point of T;
hereby
assume
A2: [N,p] in R;
hence N in NetUniv T by A1;
ex N9 being net of T, p9 being Point of T st N9 = N & p9 = p & p9 in
Lim N9 by A1,A2;
hence p in Lim N;
end;
thus thesis by A1;
end;
uniqueness
proof
let it1,it2 be Convergence-Class of T such that
A3: for N being net of T, p being Point of T holds [N,p] in it1 iff N
in NetUniv T & p in Lim N and
A4: for N being net of T, p being Point of T holds [N,p] in it2 iff N
in NetUniv T & p in Lim N;
let x,y be object;
A5: it1 c= [:NetUniv T,the carrier of T:] by Def18;
thus [x,y] in it1 implies [x,y] in it2
proof
assume
A6: [x,y] in it1;
then reconsider p = y as Point of T by A5,ZFMISC_1:87;
x in NetUniv T by A5,A6,ZFMISC_1:87;
then consider N being strict net of T such that
A7: N = x and
the carrier of N in the_universe_of the carrier of T by Def11;
[N,p] in it1 by A6,A7;
then
A8: N in NetUniv T by A3;
p in Lim N by A3,A6,A7;
hence thesis by A4,A7,A8;
end;
assume
A9: [x,y] in it2;
A10: it2 c= [:NetUniv T,the carrier of T:] by Def18;
then reconsider p = y as Point of T by A9,ZFMISC_1:87;
x in NetUniv T by A10,A9,ZFMISC_1:87;
then consider N being strict net of T such that
A11: N = x and
the carrier of N in the_universe_of the carrier of T by Def11;
[N,p] in it2 by A9,A11;
then
A12: N in NetUniv T by A4;
p in Lim N by A4,A9,A11;
hence thesis by A3,A11,A12;
end;
end;
definition
let T be non empty 1-sorted, C be Convergence-Class of T;
attr C is (CONSTANTS) means
:Def20:
for N being constant net of T st N in
NetUniv T holds [N,the_value_of N] in C;
attr C is (SUBNETS) means
:Def21:
for N being net of T, Y being subnet of N
st Y in NetUniv T for p being Element of T holds [N,p] in C implies [Y,p] in C;
attr C is (DIVERGENCE) means
:Def22:
for X being net of T, p being Element
of T st X in NetUniv T & not [X,p] in C ex Y being subnet of X st Y in NetUniv
T & not ex Z being subnet of Y st [Z,p] in C;
attr C is (ITERATED_LIMITS) means
:Def23:
for X being net of T, p being
Element of T st [X,p] in C for J being net_set of the carrier of X, T st for i
being Element of X holds [J.i,X.i] in C holds [Iterated J,p] in C;
end;
registration
let T be non empty TopSpace;
cluster Convergence T -> (CONSTANTS) (SUBNETS) (DIVERGENCE)
(ITERATED_LIMITS);
coherence
proof
set C = Convergence T;
thus C is (CONSTANTS)
proof
let N be constant net of T such that
A1: N in NetUniv T;
the_value_of N in Lim N by Th33;
hence thesis by A1,Def19;
end;
thus C is (SUBNETS)
proof
let N be net of T, Y be subnet of N such that
A2: Y in NetUniv T;
let p be Element of T;
assume [N,p] in C;
then
A3: p in Lim N by Def19;
Lim N c= Lim Y by Th32;
hence thesis by A2,A3,Def19;
end;
thus C is (DIVERGENCE)
proof
let X be net of T, p be Element of T such that
A4: X in NetUniv T;
assume not [X,p] in C;
then not p in Lim X by A4,Def19;
then consider Y being subnet of X such that
A5: Y in NetUniv T and
A6: not ex Z being subnet of Y st p in Lim Z by A4,Th38;
take Y;
thus Y in NetUniv T by A5;
let Z be subnet of Y;
not p in Lim Z by A6;
hence thesis by Def19;
end;
let X be net of T, p be Element of T;
assume
A7: [X,p] in C;
let J be net_set of the carrier of X, T such that
A8: for i being Element of X holds [J.i,X.i] in C;
A9: now
let i be Element of X;
[J.i,X.i] in C by A8;
hence X.i in Lim(J.i) & J.i in NetUniv T by Def19;
end;
X in NetUniv T by A7,Def19;
then
A10: Iterated J in NetUniv T by A9,Th25;
p in Lim X by A7,Def19;
then p in Lim Iterated J by A9,Th39;
hence thesis by A10,Def19;
end;
end;
definition
let S be non empty 1-sorted, C be Convergence-Class of S;
func ConvergenceSpace C -> strict TopStruct means
:Def24:
the carrier of it
= the carrier of S & the topology of it = { V where V is Subset of S: for p
being Element of S st p in V for N being net of S st [N,p] in C holds N
is_eventually_in V};
existence
proof
defpred P[set] means for p being Element of S st p in $1 for N being net
of S st [N,p] in C holds N is_eventually_in $1;
reconsider X = { V where V is Subset of S: P[V]} as Subset-Family of S
from DOMAIN_1:sch 7;
take TopStruct(#the carrier of S,X#);
thus thesis;
end;
correctness;
end;
registration
let S be non empty 1-sorted, C be Convergence-Class of S;
cluster ConvergenceSpace C -> non empty;
coherence
proof
the carrier of ConvergenceSpace C = the carrier of S by Def24;
hence the carrier of ConvergenceSpace C is non empty;
end;
end;
registration
let S be non empty 1-sorted, C be Convergence-Class of S;
cluster ConvergenceSpace C -> TopSpace-like;
coherence
proof
set IT = ConvergenceSpace C;
A1: the topology of IT = { V where V is Subset of S: for p being Element
of S st p in V for N being net of S st [N,p] in C holds N is_eventually_in V}
by Def24;
reconsider V = [#]IT as Subset of S by Def24;
V = the carrier of S by Def24;
then
for p being Element of S st p in V for N being net of S st [N,p] in C
holds N is_eventually_in V by Th20;
hence the carrier of IT in the topology of IT by A1;
hereby
let a be Subset-Family of IT such that
A2: a c= the topology of IT;
reconsider V = union a as Subset of S by Def24;
now
let p be Element of S;
assume p in V;
then consider X such that
A3: p in X and
A4: X in a by TARSKI:def 4;
A5: X c= V by A4,ZFMISC_1:74;
X in the topology of IT by A2,A4;
then
A6: ex W being Subset of S st X = W & for p being Element of S st p in
W for N being net of S st [N,p] in C holds N is_eventually_in W by A1;
let N be net of S;
assume [N,p] in C;
hence N is_eventually_in V by A3,A6,A5,WAYBEL_0:8;
end;
hence union a in the topology of IT by A1;
end;
let a,b be Subset of IT;
assume a in the topology of IT;
then consider Va being Subset of S such that
A7: a = Va and
A8: for p being Element of S st p in Va for N being net of S st [N,p]
in C holds N is_eventually_in Va by A1;
reconsider V = a /\ b as Subset of S by Def24;
assume b in the topology of IT;
then consider Vb being Subset of S such that
A9: b = Vb and
A10: for p being Element of S st p in Vb for N being net of S st [N,p]
in C holds N is_eventually_in Vb by A1;
now
let p be Element of S such that
A11: p in V;
let N be net of S;
assume
A12: [N,p] in C;
p in b by A11,XBOOLE_0:def 4;
then N is_eventually_in Vb by A9,A10,A12;
then consider i2 being Element of N such that
A13: for j being Element of N st i2 <= j holds N.j in Vb;
p in a by A11,XBOOLE_0:def 4;
then N is_eventually_in Va by A7,A8,A12;
then consider i1 being Element of N such that
A14: for j being Element of N st i1 <= j holds N.j in Va;
consider i being Element of N such that
A15: i1 <= i and
A16: i2 <= i by Def3;
thus N is_eventually_in V
proof
take i;
let j be Element of N;
assume
A17: i <= j;
then i2 <= j by A16,YELLOW_0:def 2;
then
A18: N.j in Vb by A13;
i1 <= j by A15,A17,YELLOW_0:def 2;
then N.j in Va by A14;
hence thesis by A7,A9,A18,XBOOLE_0:def 4;
end;
end;
hence thesis by A1;
end;
end;
theorem Th40:
for S be non empty 1-sorted, C be Convergence-Class of S holds C
c= Convergence ConvergenceSpace C
proof
let S be non empty 1-sorted, C be Convergence-Class of S;
set T = ConvergenceSpace C;
let x,y be object;
assume
A1: [x,y] in C;
C c= [:NetUniv S,the carrier of S:] by Def18;
then consider M being Element of NetUniv S, p being Element of S such that
A2: [x,y] = [M,p] by A1,DOMAIN_1:1;
reconsider q = p as Point of T by Def24;
A3: the carrier of S = the carrier of T & M in NetUniv S by Def24;
ex N being strict net of S st N = M & the carrier of N in
the_universe_of the carrier of S by Def11;
then reconsider M as net of S;
reconsider N = M as net of T by Def24;
A4: the topology of T = { V where V is Subset of S: for p being Element of S
st p in V for N being net of S st [N,p] in C holds N is_eventually_in V} by
Def24;
now
let V be a_neighborhood of q;
Int V in the topology of T by PRE_TOPC:def 2;
then p in Int V & ex W being Subset of S st W = Int V & for p being
Element of S st p in W for N being net of S st [N,p] in C holds N
is_eventually_in W by A4,CONNSP_2:def 1;
then M is_eventually_in Int V by A1,A2;
then consider ii being Element of M such that
A5: for j being Element of M st ii <= j holds M.j in Int V;
reconsider i = ii as Element of N;
now
let j be Element of N such that
A6: i <= j;
reconsider jj = j as Element of M;
M.jj = N.j;
hence N.j in Int V by A5,A6;
end;
then Int V c= V & N is_eventually_in Int V by TOPS_1:16;
hence N is_eventually_in V by WAYBEL_0:8;
end;
then
A7: p in Lim N by Def15;
N in NetUniv T by A3,Lm7;
hence thesis by A2,A7,Def19;
end;
definition
let T be non empty 1-sorted, C be Convergence-Class of T;
attr C is topological means
C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);
end;
registration
let T be non empty 1-sorted;
cluster non empty topological for Convergence-Class of T;
existence
proof
reconsider C = [:NetUniv T, the carrier of T:] as Convergence-Class of T
by Def18;
take C;
thus C is non empty;
thus C is topological
proof
thus C is (CONSTANTS)
by ZFMISC_1:87;
thus C is (SUBNETS)
by ZFMISC_1:87;
thus C is (DIVERGENCE)
by ZFMISC_1:87;
let X be net of T, p be Element of T;
assume [X,p] in C;
then
A1: X in NetUniv T by ZFMISC_1:87;
let J be net_set of the carrier of X, T such that
A2: for i being Element of X holds [J.i,X.i] in C;
now
let i be Element of X;
[J.i,X.i] in C by A2;
hence J.i in NetUniv T by ZFMISC_1:87;
end;
then Iterated J in NetUniv T by A1,Th25;
hence thesis by ZFMISC_1:87;
end;
end;
end;
registration
let T be non empty 1-sorted;
cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS)
for Convergence-Class of T;
coherence;
cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological
for Convergence-Class of T;
coherence;
end;
theorem Th41:
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty
TopSpace) holds S is open iff for p being Element of T st p in S for N being
net of T st [N,p] in C holds N is_eventually_in S
proof
let T be non empty 1-sorted, C be topological Convergence-Class of T, S be
Subset of ConvergenceSpace C;
A1: the topology of ConvergenceSpace C = { V where V is Subset of T: for p
being Element of T st p in V for N being net of T st [N,p] in C holds N
is_eventually_in V} by Def24;
then
A2: S in the topology of ConvergenceSpace C implies ex V be Subset of T st S
= V & for p being Element of T st p in V for N being net of T st [N,p] in C
holds N is_eventually_in V;
the carrier of ConvergenceSpace C = the carrier of T by Def24;
then (for p being Element of T st p in S for N being net of T st [N,p] in C
holds N is_eventually_in S) implies S in the topology of ConvergenceSpace C by
A1;
hence thesis by A2;
end;
theorem Th42:
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of (ConvergenceSpace C qua non empty
TopSpace) holds S is closed iff for p being Element of T holds for N being net
of T st [N,p] in C & N is_often_in S holds p in S
proof
let T be non empty 1-sorted, C be topological Convergence-Class of T, S be
Subset of ConvergenceSpace C;
set CC = ConvergenceSpace C;
A1: the carrier of T = the carrier of CC by Def24;
hereby
assume S is closed;
then
A2: S` is open;
let p be Element of T;
let N be net of T such that
A3: [N,p] in C;
assume N is_often_in S;
then not N is_eventually_in [#]CC\S by A1,WAYBEL_0:10;
then not p in S` by A3,A2,Th41;
hence p in S by A1,XBOOLE_0:def 5;
end;
assume
A4: for p being Element of T holds for N being net of T st [N,p] in C &
N is_often_in S holds p in S;
now
let p be Element of T;
assume p in S`;
then
A5: not p in S by XBOOLE_0:def 5;
let N be net of T;
assume [N,p] in C;
then not N is_often_in S by A4,A5;
hence N is_eventually_in S` by A1,WAYBEL_0:10;
end;
then S` is open by Th41;
hence thesis;
end;
theorem Th43:
for T being non empty 1-sorted, C being topological
Convergence-Class of T, S being Subset of ConvergenceSpace C, p being Point of
ConvergenceSpace C st p in Cl S ex N being net of ConvergenceSpace C st [N,p]
in C & rng the mapping of N c= S & p in Lim N
proof
let T be non empty 1-sorted, C be topological Convergence-Class of T, S be
Subset of (ConvergenceSpace C qua non empty TopSpace), p be Point of
ConvergenceSpace C such that
A1: p in Cl S;
set CC = ConvergenceSpace C;
defpred P[Point of CC] means ex N being net of ConvergenceSpace C st [N,$1]
in C & rng the mapping of N c= S & $1 in Lim N;
set F = { q where q is Point of CC: P[q]};
F is Subset of CC from DOMAIN_1:sch 7;
then reconsider F as Subset of CC;
for p being Element of T holds for N being net of T st [N,p] in C & N
is_often_in F holds p in F
proof
let p be Element of T;
reconsider q = p as Point of CC by Def24;
let N be net of T such that
A2: [N,p] in C and
A3: N is_often_in F;
C c= [:NetUniv T, the carrier of T:] by Def18;
then N in NetUniv T by A2,ZFMISC_1:87;
then
A4: ex N0 being strict net of T st N0 = N & the carrier of N0 in
the_universe_of the carrier of T by Def11;
reconsider M = N"F as subnet of N by A3,Th22;
defpred P[Element of M, object] means
[$2,M.$1] in C & ex X being net of T st
X = $2 & rng the mapping of X c= S;
A5: now
let i be Element of M;
i in the carrier of M;
then i in (the mapping of N)"F by Def10;
then
A6: (the mapping of N).i in F by FUNCT_2:38;
the mapping of M = (the mapping of N)|the carrier of M by Def6;
then (the mapping of M).i in F by A6,FUNCT_1:49;
then consider q being Point of CC such that
A7: M.i = q and
A8: ex N being net of ConvergenceSpace C st [N,q] in C & rng the
mapping of N c= S & q in Lim N;
consider N being net of CC such that
A9: [N,q] in C and
A10: rng the mapping of N c= S and
q in Lim N by A8;
reconsider x = N as object;
take x;
thus P[i, x]
proof
thus [x,M.i] in C by A7,A9;
reconsider X = N as net of T by Def24;
take X;
thus X = x;
thus thesis by A10;
end;
end;
consider J being ManySortedSet of the carrier of M such that
A11: for i being Element of M holds P[i, J.i] from PBOOLE:sch 6(A5);
for i being set st i in the carrier of M holds J.i is net of T
proof
let i be set;
assume i in the carrier of M;
then
ex X being net of T st X = J.i & rng the mapping of X c= S by A11;
hence thesis;
end;
then reconsider J as net_set of the carrier of M,T by Th24;
set XX = the set of all rng the mapping of J.i where i is Element of M;
A12: for i being Element of M holds [J.i,M.i] in C & rng the mapping of J.
i c= S
proof
let i be Element of M;
thus [J.i,M.i] in C by A11;
ex X being net of T st X = J.i & rng the mapping of X c= S by A11;
hence thesis;
end;
for x st x in XX holds x c= S
proof
let x;
assume x in XX;
then ex i being Element of M st x = rng the mapping of J.i;
hence thesis by A12;
end;
then
A13: union XX c= S by ZFMISC_1:76;
reconsider I = Iterated J as net of CC by Def24;
rng the mapping of I c= union XX by Th28;
then
A14: rng the mapping of I c= S by A13;
the carrier of M = (the mapping of N)"F by Def10;
then the carrier of M in the_universe_of the carrier of T by A4,
CLASSES1:def 1;
then M in NetUniv T by Def11;
then [M,p] in C by A2,Def21;
then
A15: [I,p] in C by A12,Def23;
C c= Convergence CC by Th40;
then q in Lim I by A15,Def19;
hence thesis by A15,A14;
end;
then
A16: F is closed by Th42;
S c= F
proof
{} in {{}} by TARSKI:def 1;
then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:3;
set R = RelStr(#{{}},r#);
A17: now
let x,y be Element of R;
x = {} & y = {} by TARSKI:def 1;
then [x,y] in {[{},{}]} by TARSKI:def 1;
hence x <= y by ORDERS_2:def 5;
end;
A18: R is transitive
by A17;
R is directed
proof
let x,y be Element of R;
take x;
thus thesis by A17;
end;
then reconsider R as transitive directed non empty RelStr by A18;
let x be object;
set V = the_universe_of the carrier of T;
assume
A19: x in S;
then reconsider q = x as Point of CC;
set N = ConstantNet(R,q);
the mapping of N = (the carrier of N) --> q by Def5;
then rng the mapping of N = {q} by FUNCOP_1:8;
then
A20: rng the mapping of N c= S by A19,ZFMISC_1:31;
{} in V by CLASSES2:56;
then
A21: the carrier of R in V by CLASSES2:2;
the carrier of CC = the carrier of T by Def24;
then reconsider M = N as constant strict net of T by Lm6;
A22: the_value_of N = q by Th13;
then the_value_of the mapping of M = q by Def8;
then
A23: the_value_of M = q by Def8;
the RelStr of N = the RelStr of R by Def5;
then M in NetUniv T by A21,Def11;
then
A24: [M,q] in C by A23,Def20;
q in Lim N by A22,Th33;
hence thesis by A24,A20;
end;
then Cl S c= F by A16,TOPS_1:5;
then p in F by A1;
then ex q being Point of CC st p = q & ex N being net of ConvergenceSpace C
st [N,q] in C & rng the mapping of N c= S & q in Lim N;
hence thesis;
end;
theorem
for T be non empty 1-sorted, C be Convergence-Class of T holds
Convergence ConvergenceSpace C = C iff C is topological
proof
let T be non empty 1-sorted, C be Convergence-Class of T;
set CC = ConvergenceSpace C, CCC = Convergence ConvergenceSpace C;
A1: the carrier of ConvergenceSpace C = the carrier of T by Def24;
A2: for N being net of T, n being net of CC st N = n for x being subnet of n
holds x is subnet of N
proof
let N be net of T, n be net of CC such that
A3: N = n;
let X be subnet of n;
reconsider x = X as net of T by Def24;
consider f being Function of X, n such that
A4: the mapping of X = (the mapping of n)*f and
A5: for m being Element of n ex n being Element of X st for p being
Element of X st n <= p holds m <= f.p by Def9;
reconsider f as Function of x, N by A3;
the mapping of x = (the mapping of N)*f by A3,A4;
hence thesis by A3,A5,Def9;
end;
A6: for N being net of T, n being net of CC st N = n for X being subnet of N
holds X is subnet of n
proof
let N be net of T, n be net of CC such that
A7: N = n;
let X be subnet of N;
reconsider x = X as net of CC by Def24;
consider f being Function of X, N such that
A8: the mapping of X = (the mapping of N)*f and
A9: for m being Element of N ex n being Element of X st for p being
Element of X st n <= p holds m <= f.p by Def9;
reconsider f as Function of x, n by A7;
the mapping of x = (the mapping of n)*f by A7,A8;
hence thesis by A7,A9,Def9;
end;
A10: for N being net of T holds N is net of CC by Def24;
hereby
assume
A11: CCC = C;
A12: C is (SUBNETS)
proof
let N be net of T, Y be subnet of N;
reconsider M = N as net of CC by Def24;
reconsider X = Y as subnet of M by A6;
assume Y in NetUniv T;
then
A13: X in NetUniv CC by A1,Lm7;
let p be Element of T;
reconsider q = p as Element of CC by Def24;
assume [N,p] in C;
then [M,q] in CCC by A11;
hence thesis by A11,A13,Def21;
end;
A14: C is (ITERATED_LIMITS)
proof
let X be net of T, p be Element of T;
reconsider q = p as Element of CC by Def24;
reconsider x = X as net of CC by Def24;
assume
A15: [X,p] in C;
let J be net_set of the carrier of X, T;
reconsider I = J as ManySortedSet of the carrier of x;
I is net_set of the carrier of x,CC
proof
let i be set;
assume i in rng I;
then i is net of T by Def12;
hence thesis by A10;
end;
then reconsider I = J as net_set of the carrier of x,CC;
assume
A16: for i being Element of X holds [J.i,X.i] in C;
now
let i be Element of x;
reconsider j = i as Element of X;
X.j = x .i;
hence [I.i,x .i] in CCC by A11,A16;
end;
then
A17: [Iterated I,q] in CCC by A11,A15,Def23;
A18: the RelStr of Iterated I = [:X, product J:] by Def13
.= the RelStr of Iterated J by Def13;
A19: now
let j be object;
assume j in dom the mapping of Iterated I;
then reconsider jj = j as Element of Iterated I;
the carrier of Iterated I = [:the carrier of x, product Carrier I
:] by Th26;
then consider
j1 being Element of x, j2 being Element of product Carrier I
such that
A20: jj = [j1,j2] by DOMAIN_1:1;
reconsider i1 = j1 as Element of X;
reconsider j2 as Element of product I by YELLOW_1:def 4;
set i2 = j2;
the carrier of Iterated J = [:the carrier of X, product Carrier J
:] by Th26;
then reconsider i = [i1,i2] as Element of Iterated J by ZFMISC_1:87;
thus (the mapping of Iterated I).j = (Iterated I).jj
.= (the mapping of I.j1).(j2.j1) by A20,Th27
.= (the mapping of J.i1).(i2.i1)
.= (Iterated J).i by Th27
.= (the mapping of Iterated J).j by A20;
end;
dom the mapping of Iterated I = the carrier of Iterated I by
FUNCT_2:def 1;
then dom the mapping of Iterated I = dom the mapping of Iterated J by A18
,FUNCT_2:def 1;
then the mapping of Iterated I = the mapping of Iterated J by A19,
FUNCT_1:2;
hence thesis by A11,A17,A18;
end;
A21: C is (DIVERGENCE)
proof
let X be net of T, p be Element of T;
reconsider q = p as Element of CC by Def24;
reconsider x = X as net of CC by Def24;
assume X in NetUniv T;
then
A22: x in NetUniv CC by A1,Lm7;
assume not [X,p] in C;
then consider y being subnet of x such that
A23: y in NetUniv CC and
A24: not ex z being subnet of y st [z,q] in CCC by A11,A22,Def22;
reconsider Y = y as subnet of X by A2;
take Y;
thus Y in NetUniv T by A1,A23,Lm7;
let Z be subnet of Y;
reconsider z = Z as subnet of y by A6;
not [z,q] in CCC by A24;
hence thesis by A11;
end;
C is (CONSTANTS)
proof
let N be constant net of T;
reconsider M = N as net of CC by Def24;
the mapping of N is constant;
then the mapping of M is constant;
then reconsider M as constant net of CC by Def4;
assume N in NetUniv T;
then
A25: M in NetUniv CC by A1,Lm7;
the_value_of M = the_value_of the mapping of M by Def8
.= the_value_of the mapping of N
.= the_value_of N by Def8;
hence thesis by A11,A25,Def20;
end;
hence C is topological by A12,A21,A14;
end;
assume
A26: C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS);
then reconsider C9 = C as topological Convergence-Class of T;
A27: Convergence ConvergenceSpace C c= C
proof
let x,y be object;
assume
A28: [x,y] in Convergence CC;
Convergence CC c= [:NetUniv CC,the carrier of CC:] by Def18;
then consider
M being Element of NetUniv CC, p being Element of CC such that
A29: [x,y] = [M,p] by A28,DOMAIN_1:1;
reconsider q = p as Point of T by Def24;
A30: M in NetUniv CC;
A31: ex N being strict net of CC st N = M & the carrier of N in
the_universe_of the carrier of CC by Def11;
assume
A32: not [x,y] in C;
reconsider M as net of CC by A31;
reconsider N = M as net of T by Def24;
N in NetUniv T by A1,A30,Lm7;
then consider Y being subnet of N such that
A33: Y in NetUniv T and
A34: not ex Z being subnet of Y st [Z,q] in C by A26,A29,A32;
reconsider Y9 = Y as subnet of M by A6;
reconsider YY = the RelStr of Y as transitive directed non empty RelStr by
Lm1,Lm2;
set X = ConstantNet(YY,q);
defpred P[object,object] means
ex i being Element of Y, Ji being net of T st $1
= i & Ji = $2 & [Ji,p] in C & rng the mapping of Ji c= { Y.c where c is Element
of Y : i <= c };
A35: the RelStr of X = YY by Def5;
reconsider X as constant non empty strict net of T;
A36: p in Lim M by A28,A29,Def19;
A37: for x being object st x in the carrier of X
ex j being object st P[x, j]
proof
let x be object;
assume x in the carrier of X;
then reconsider i9 = x as Element of Y9 by Th4;
reconsider i = i9 as Element of Y;
Lim M c= Lim Y9 by Th32;
then consider S being Subset of CC such that
A38: S = { Y9.c where c is Element of Y9 : i9 <= c } and
A39: p in Cl S by A36,Th34;
consider Go being net of ConvergenceSpace C9 such that
A40: [Go,p] in C9 and
A41: rng the mapping of Go c= S and
p in Lim Go by A39,Th43;
reconsider Ji = Go as net of T by Def24;
take Ji,i,Ji;
thus x = i & Ji = Ji & [Ji,p] in C by A40;
let e be object;
assume e in rng the mapping of Ji;
then e in S by A41;
then consider c9 being Element of Y9 such that
A42: e = Y9.c9 and
A43: i9 <= c9 by A38;
reconsider cc = c9 as Element of Y;
e = Y.cc by A42;
hence thesis by A43;
end;
consider J being ManySortedSet of the carrier of X such that
A44: for x being object st x in the carrier of X holds P[x, J.x] from
PBOOLE:sch 3(A37);
now
let x be set;
assume x in the carrier of X;
then ex i being Element of Y, Ji being net of T st x = i & Ji = J.x & [
Ji,p] in C & rng the mapping of Ji c= { Y.c where c is Element of Y : i <= c }
by A44;
hence J.x is net of T;
end;
then reconsider
J as yielding_non-empty_carriers net_set of the carrier of X,T
by Th24;
reconsider X9 = X as net of CC by Def24;
A45: the mapping of X9 is constant;
A46: for i being Element of X holds [J.i,X.i] in C
proof
let i be Element of X;
ex ii being Element of Y, Ji being net of T st i = ii & Ji = J.i &
[Ji,p] in C & rng the mapping of Ji c= { Y.c where c is Element of Y : ii <= c
} by A44;
hence thesis by Th5;
end;
A47: the_value_of X = q by Th13;
reconsider X9 as constant net of CC by A45,Def4;
A48: the RelStr of Iterated J = [:X, product J:] by Def13;
then
A49: the carrier of Iterated J = [:the carrier of X, the carrier of
product J:] by YELLOW_3:def 2;
A50: Iterated J is subnet of Y
proof
set F = the Element of product J;
set h = the mapping of Iterated J, g = the mapping of Y9;
defpred P[object,object,object] means
ex f being Function, x being Element of X
st f.$2 = $1 & x = $3 & (the mapping of J.x).$2 = (the mapping of Y).$1;
deffunc F(Element of Y) = { c where c is Element of Y : $1 <= c };
consider B being ManySortedSet of the carrier of Y such that
A51: for i being Element of Y holds B.i = F(i) from PBOOLE:sch 5;
now
assume {} in rng B;
then consider i be object such that
A52: i in dom B and
A53: B.i = {} by FUNCT_1:def 3;
reconsider i as Element of Y by A52;
consider j being Element of Y such that
A54: i <= j and
i <= j by Def3;
j in { c where c is Element of Y : i <= c } by A54;
hence contradiction by A51,A53;
end;
then reconsider B as non-empty ManySortedSet of the carrier of Y by
RELAT_1:def 9;
deffunc F(Element of X) = the carrier of J.$1;
consider M being ManySortedSet of the carrier of X such that
A55: for x being Element of X holds M.x = F(x) from PBOOLE:sch 5;
reconsider B9 = B as non-empty ManySortedSet of the carrier of X by A35;
A56: for i be object st i in the carrier of X
for x be object st x in M.i ex y be object st y in B9.i & P[y,x,i]
proof
let i be object such that
A57: i in the carrier of X;
consider e being Element of Y, Ji being net of T such that
A58: i = e and
A59: Ji = J.i and
[Ji,p] in C and
A60: rng the mapping of Ji c= { Y.c where c is Element of Y : e
<= c } by A44,A57;
reconsider i9 = i as Element of X by A57;
defpred P[object,object] means
(the mapping of Ji).$1 = (the mapping of Y).$2;
A61: for ji being Element of Ji ex u being Element of B9.i9 st P[ji, u]
proof
let ji be Element of Ji;
ji in the carrier of Ji;
then ji in dom the mapping of Ji by FUNCT_2:def 1;
then (the mapping of Ji).ji in rng the mapping of Ji by FUNCT_1:def 3
;
then (the mapping of Ji).ji in { Y.c where c is Element of Y : e <=
c } by A60;
then consider c being Element of Y such that
A62: (the mapping of Ji).ji = Y.c and
A63: e <= c;
c in { cc where cc is Element of Y : e <= cc } by A63;
then reconsider c as Element of B9.i9 by A51,A58;
take c;
thus (the mapping of Ji).ji = (the mapping of Y).c by A62;
end;
consider f being Function of Ji, B9.i9 such that
A64: for ji being Element of Ji holds P[ji, f.ji] from FUNCT_2:
sch 3(A61 );
let x be object;
assume x in M.i;
then reconsider ji = x as Element of Ji by A55,A57,A59;
reconsider f as Function of Ji, B.i;
take f.x;
f.ji in B.i;
hence f.x in B9.i;
take f,i9;
thus f.x = f.x & i9 = i;
thus (the mapping of J.i9).x = (the mapping of Ji).ji by A59
.= (the mapping of Y).(f.x) by A64;
end;
consider u be ManySortedFunction of M, B9 such that
A65: for i be object st i in the carrier of X holds ex f be Function
of M.i, B9.i st f = u.i &
for x be object st x in M.i holds P[f.x,x,i] from
MSSUBFAM:sch 1(A56);
deffunc F(Element of X, Element of product J) = u.$1 .($2.$1);
A66: for x being Element of X, y being Element of product J holds F(x,y
) in the carrier of Y
proof
let x be Element of X, y be Element of product J;
reconsider x9 = x as Element of X9;
reconsider k = x as Element of Y by A35;
defpred P[Element of Y] means k <= $1;
set ZZ = { c where c is Element of Y : P[c] };
A67: ZZ is Subset of Y from DOMAIN_1:sch 7;
x9 in the carrier of X9;
then
A68: x9 in dom Carrier J by PARTFUN1:def 2;
y in the carrier of product J;
then y in product Carrier J by YELLOW_1:def 4;
then y.x9 in (Carrier J).x9 by A68,CARD_3:9;
then y.x9 in the carrier of J.x by Th2;
then u.k is Function of M.k, B.k & y.x in M.k by A55,PBOOLE:def 15;
then
A69: u.k.(y.x) in B.k by FUNCT_2:5;
B.k = ZZ by A51;
hence thesis by A67,A69;
end;
consider f being Function of [:the carrier of X, the carrier of product
J:], Y such that
A70: for x being Element of X, y being Element of product J holds f
.(x,y) = F(x,y) from FUNCT_7:sch 1(A66);
reconsider f as Function of Iterated J,Y by A49;
A71: for x being Element of X, j being Element of M.x holds (the
mapping of J.x).j = (the mapping of Y).(u.x .j)
proof
let i be Element of X, j be Element of M.i;
consider f be Function of M.i, B9.i such that
A72: f = u.i and
A73: for x be object st x in M.i holds P[f.x,x,i] by A65;
M.i = the carrier of J.i by A55;
then P[f.j,j,i] by A73;
hence thesis by A72;
end;
A74: for x being object st x in dom h holds h.x = g.(f.x)
proof
let x be object;
assume x in dom h;
then x in the carrier of Iterated J;
then x in [:the carrier of X9,product Carrier J:] by Th26;
then x in [:the carrier of X9,the carrier of product J:] by
YELLOW_1:def 4;
then consider
x1 being Element of X9, x2 being Element of product J such
that
A75: x = [x1,x2] by DOMAIN_1:1;
reconsider x9 = x1 as Element of X;
x2 in the carrier of product J;
then
A76: x2 in product Carrier J by YELLOW_1:def 4;
dom Carrier J = the carrier of X9 & the carrier of J.x9 = (
Carrier J).x1 by Th2,PARTFUN1:def 2;
then x2.x1 in the carrier of J.x9 by A76,CARD_3:9;
then reconsider j = x2.x1 as Element of M.x9 by A55;
thus h.x = h.(x1,x2) by A75
.= (the mapping of J.x9).(x2.x1) by Def13
.= g.(u.x9.j) by A71
.= g.(f.(x1,x2)) by A70
.= g.(f.x) by A75;
end;
take f;
for x being object holds x in dom h iff x in dom f & f.x in dom g
proof
let x be object;
hereby
assume x in dom h;
then x in the carrier of Iterated J;
then x in [:the carrier of X9,product Carrier J:] by Th26;
then
A77: x in [:the carrier of X9,the carrier of product J:] by YELLOW_1:def 4
;
hence x in dom f by FUNCT_2:def 1;
f.x in the carrier of Y by A77,FUNCT_2:5;
hence f.x in dom g by FUNCT_2:def 1;
end;
assume that
A78: x in dom f and
f.x in dom g;
x in [:the carrier of X9,the carrier of product J:] by A78,
FUNCT_2:def 1;
then x in [:the carrier of X9,product Carrier J:] by YELLOW_1:def 4;
then x in the carrier of Iterated J by Th26;
hence thesis by FUNCT_2:def 1;
end;
hence the mapping of Iterated J = (the mapping of Y)*f by A74,FUNCT_1:10;
let m be Element of Y;
reconsider n = [m,F] as Element of Iterated J by A35,A49,ZFMISC_1:87;
take n;
let p be Element of Iterated J;
consider k9 being Element of X, G being Element of product J such that
A79: p = [k9,G] by A49,DOMAIN_1:1;
reconsider m9 = m as Element of X by A35;
reconsider F as Element of product J;
G in the carrier of product J;
then
A80: dom Carrier J = the carrier of X9 & G in product Carrier J by
PARTFUN1:def 2,YELLOW_1:def 4;
reconsider k = k9 as Element of Y by A35;
A81: f.(k9,G) = u.k.(G.k) by A70;
reconsider k99 = k9 as Element of X9;
A82: u.k is Function of M.k, B.k by PBOOLE:def 15;
then
A83: rng(u.k) c= B.k by RELAT_1:def 19;
dom(u.k) = M.k by A82,FUNCT_2:def 1
.= the carrier of J.k9 by A55
.= (Carrier J).k99 by Th2;
then
A84: G.k99 in dom(u.k) by A80,CARD_3:9;
reconsider k9 = k as Element of X;
reconsider G as Element of product J;
assume n <= p;
then [m9,F] <= [k9,G] by A48,A79,Lm3;
then m9 <= k9 by YELLOW_3:11;
then
A85: m <= k by A35,Lm3;
f.p in rng(u.k) by A79,A81,A84,FUNCT_1:def 3;
then f.p in B.k by A83;
then f.p in { c where c is Element of Y : k <= c } by A51;
then ex c being Element of Y st c = f.p & k <= c;
hence thesis by A85,YELLOW_0:def 2;
end;
A86: the RelStr of X = the RelStr of Y by Def5;
ex N0 being strict net of T st N0 = Y & the carrier of N0 in
the_universe_of the carrier of T by A33,Def11;
then X in NetUniv T by A86,Def11;
then [X,q] in C by A26,A47;
then [Iterated J,q] in C by A26,A46;
hence contradiction by A34,A50;
end;
C c= Convergence ConvergenceSpace C by Th40;
hence thesis by A27;
end;