### The Mizar article:

### Moore-Smith Convergence

**by****Andrzej Trybulec**

- Received November 12, 1996
Copyright (c) 1996 Association of Mizar Users

- MML identifier: YELLOW_6
- [ MML identifier index ]

environ vocabulary FUNCOP_1, SEQM_3, RELAT_1, FUNCT_1, BOOLE, CARD_1, ZF_LANG, ORDINAL1, CLASSES1, CLASSES2, CARD_3, FUNCT_2, PROB_1, TARSKI, PRE_TOPC, CONNSP_2, TOPS_1, COMPTS_1, COMPLSP1, SUBSET_1, PRALG_1, PBOOLE, RLVECT_2, WAYBEL_3, YELLOW_1, FRAENKEL, ZF_REFLE, ORDERS_1, WAYBEL_0, QUANTAL1, LATTICES, RELAT_2, CAT_1, YELLOW_0, WELLORD1, ORDINAL2, MCART_1, REALSET1, SEQ_2, SETFAM_1, CLOSURE1, YELLOW_6; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, COMPLSP1, RELAT_1, RELSET_1, FUNCT_1, FUNCT_2, BINOP_1, REALSET1, CARD_1, CARD_3, MSUALG_1, PRE_CIRC, PROB_1, ORDINAL1, CLASSES1, CLASSES2, TOLER_1, SEQM_3, STRUCT_0, TOPS_1, COMPTS_1, CONNSP_2, PBOOLE, PRALG_1, ORDERS_1, LATTICE3, PRE_TOPC, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_3, FRAENKEL, WAYBEL_3, GRCAT_1; constructors SEQM_3, CLASSES1, TOPS_1, CONNSP_2, COMPTS_1, COMPLSP1, PRALG_1, WAYBEL_3, TOLER_1, YELLOW_3, BINOP_1, MSUALG_1, DOMAIN_1, PRE_CIRC, GRCAT_1, LATTICE3, PROB_1, TOPS_2, PRE_TOPC; clusters SUBSET_1, STRUCT_0, RELSET_1, WAYBEL_0, ORDERS_1, PRALG_1, AMI_1, YELLOW_1, YELLOW_3, INDEX_1, PRE_TOPC, MSUALG_1, COMPLSP1, LATTICE3, YELLOW_0, PBOOLE, FUNCOP_1, RELAT_1, FUNCT_1, CLASSES2, CARD_1, FRAENKEL, SEQM_3, ZFMISC_1; requirements NUMERALS, BOOLE, SUBSET; definitions TARSKI, STRUCT_0, WAYBEL_0, PRALG_1, YELLOW_1, COMPTS_1, YELLOW_0, RELAT_1, PRE_TOPC, WAYBEL_3, CONNSP_2; theorems STRUCT_0, CONNSP_2, TOPS_1, FUNCOP_1, WAYBEL_0, PRE_TOPC, ORDERS_1, TMAP_1, RELAT_1, FUNCT_2, SEQM_3, ZFMISC_1, FUNCT_1, TARSKI, PBOOLE, YELLOW_1, CARD_3, PRALG_1, YELLOW_3, MSUALG_1, RELSET_1, BINOP_1, DOMAIN_1, YELLOW_0, CLASSES2, CLASSES1, CARD_2, FUNCT_6, COMPLSP1, PROB_1, LATTICE3, SPPOL_1, COMPTS_1, MCART_1, SUBSET_1, WELLORD1, WAYBEL_3, GRCAT_1, SETFAM_1, XBOOLE_0, XBOOLE_1, ORDINAL1, PARTFUN1; schemes MSUALG_1, FUNCT_7, MSUALG_9, SETWISEO, NATTRA_1, RELSET_1, DOMAIN_1, MSSUBFAM, PRALG_2, FUNCT_2, XBOOLE_0; begin :: Preliminaries, classical mathematics scheme SubsetEq{X()-> non empty set, A,B()-> Subset of X(), P[set]}: A() = B() provided A1: for y being Element of X() holds y in A() iff P[y] and A2: for y being Element of X() holds y in B() iff P[y] proof defpred Q[set] means $1 in X() & P[$1]; A3: for y being set holds y in A() iff Q[y] by A1; A4: for y being set holds y in B() iff Q[y] by A2; thus A() = B() from Extensionality(A3,A4); end; canceled; definition let f be Function; assume A1: f is non empty constant; func the_value_of f means :Def1: ex x being set st x in dom f & it = f.x; existence proof dom f <> {} by A1,RELAT_1:64; then consider x being set such that A2: x in dom f by XBOOLE_0:def 1; take f.x; thus thesis by A2; end; uniqueness by A1,SEQM_3:def 5; end; definition cluster non empty constant Function; existence proof consider S being set; take f = {{}} --> S; thus f is non empty; thus f is constant; end; end; theorem Th2: for X being non empty set, x being set holds the_value_of (X --> x) = x proof let X be non empty set, x be set; set f = X --> x; consider i being set such that A1: i in dom f & the_value_of f = f.i by Def1; i in X by A1,PBOOLE:def 3; hence the_value_of f = x by A1,FUNCOP_1:13; end; theorem Th3: for f being Function holds Card rng f c= Card dom f proof let f be Function; rng f = f.:dom f by RELAT_1:146; hence Card rng f c= Card dom f by CARD_2:3; end; definition cluster universal -> epsilon-transitive being_Tarski-Class set; coherence by CLASSES2:def 1; cluster epsilon-transitive being_Tarski-Class -> universal set; coherence by CLASSES2:def 1; end; reserve x,y,z,X for set, T for Universe; definition let X; canceled; func the_universe_of X equals :Def3: Tarski-Class the_transitive-closure_of X; correctness; end; definition let X; cluster the_universe_of X -> epsilon-transitive being_Tarski-Class; coherence proof Tarski-Class the_transitive-closure_of X is epsilon-transitive being_Tarski-Class; hence thesis by Def3; end; end; definition let X; cluster the_universe_of X -> universal non empty; coherence proof the_universe_of X = Tarski-Class the_transitive-closure_of X by Def3; hence thesis; end; end; canceled; theorem Th5: 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; A3: product f c= Funcs(dom f, Union f) by FUNCT_6:10; A4: Card dom f in Card T by A1,CLASSES2:1; Card rng f c= Card dom f by Th3; then Card rng f in Card T by A4,ORDINAL1:22; then rng f in T by A2,CLASSES1:2; then union rng f in T by CLASSES2:65; then Union f in T by PROB_1:def 3; then Funcs(dom f, Union f) in T by A1,CLASSES2:67; hence product f in T by A3,CLASSES1:def 1; end; begin :: Topological spaces, preliminaries theorem Th6: :: PRE_TOPC:def 13 for T being non empty TopSpace, A being Subset of T for p being Point of T holds p in Cl A iff for G being a_neighborhood of p holds G meets A proof let T be non empty TopSpace, A be Subset of T; let p be Point of T; hereby assume A1: p in Cl A; let G be a_neighborhood of p; A2: Int G c= G by TOPS_1:44; p in Int G & Int G is open by CONNSP_2:def 1,TOPS_1:51; then A meets Int G by A1,PRE_TOPC:def 13; hence G meets A by A2,XBOOLE_1:63; end; assume A3: for G being a_neighborhood of p holds G meets A; now let G be Subset of T; assume G is open & p in G; then G is a_neighborhood of p by CONNSP_2:5; hence A meets G by A3; end; hence p in Cl A by PRE_TOPC:def 13; end; definition let T be non empty TopSpace; redefine attr T is being_T2; synonym T is Hausdorff; end; definition cluster Hausdorff (non empty TopSpace); existence proof take the_Complex_Space 1; thus thesis by COMPLSP1:111; end; end; theorem for X be non empty TopSpace, A be Subset of X holds [#]X is a_neighborhood of A proof let X be non empty TopSpace, A be Subset of X; Int [#]X = [#]X by TOPS_1:43; hence A c= Int [#]X by PRE_TOPC:14; end; theorem for X be non empty TopSpace, A be Subset of X, Y being a_neighborhood of A holds A c= Y proof let X be non empty TopSpace, A be Subset of X, Y be a_neighborhood of A; A c= Int Y & Int Y c= Y by CONNSP_2:def 2,TOPS_1:44; hence A c= Y by XBOOLE_1:1; end; begin :: 1-sorted structures theorem Th9: 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 13; hence (Carrier J).i = the carrier of J.i; end; definition cluster non empty constant 1-sorted-yielding Function; existence proof consider S being 1-sorted; take f = {{}} --> S; A1: dom(f) = {{}} by FUNCOP_1:19; thus f is non empty; thus f is constant; let x be set; assume x in dom(f); hence (f).x is 1-sorted by A1,FUNCOP_1:13; end; end; definition let J be 1-sorted-yielding Function; redefine attr J is non-Empty means :Def4: for i being set st i in rng J holds i is non empty 1-sorted; compatibility proof hereby assume A1: J is non-Empty; let i be set; assume A2: i in rng J; then ex x being set st x in dom J & i = J.x by FUNCT_1:def 5; hence i is non empty 1-sorted by A1,A2,PRALG_1:def 11,WAYBEL_3:def 7; end; assume A3: for i being set st i in rng J holds i is non empty 1-sorted; let S be 1-sorted; thus thesis by A3; end; synonym J is yielding_non-empty_carriers; end; definition let X be set; let L be 1-sorted; cluster X --> L -> 1-sorted-yielding; coherence proof set IT = X --> L; let x be set; assume A1: x in dom IT; then x in X by PBOOLE:def 3; then A2: rng IT = {L} by FUNCOP_1:14; IT.x in rng IT by A1,FUNCT_1:def 5; hence IT.x is 1-sorted by A2,TARSKI:def 1; end; end; definition let I be set; cluster yielding_non-empty_carriers (1-sorted-yielding ManySortedSet of I); existence proof consider R being non empty 1-sorted; take I --> R; let i be set; A1: rng(I --> R) c= {R} by FUNCOP_1:19; assume i in rng(I --> R); hence i is non empty 1-sorted by A1,TARSKI:def 1; end; end; definition 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 the carrier of product J is functional by YELLOW_1:def 4; end; end; definition 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 set such that A1: i in dom Carrier J and A2: (Carrier J).i = {} by FUNCT_1:def 5; A3: i in I by A1,PBOOLE:def 3; 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 13; i in dom J by A3,PBOOLE:def 3; then A6: R in rng J by A4,FUNCT_1:def 5; R is empty by A2,A5,STRUCT_0:def 1; hence contradiction by A6,Def4; end; end; theorem Th10: for T being non empty 1-sorted, S being Subset of T, p being Element of T holds not p in S iff p in S` proof let T be non empty 1-sorted, S be Subset of T; let p be Element of T; thus not p in S iff p in S` by SUBSET_1:50,54; end; begin :: Preliminaries to Relational Structures definition 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,Th10; then not y in A by A2,WAYBEL_0:def 19; hence y in A` by Th10; end; end; definition 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,Th10; then not y in A by A2,WAYBEL_0:def 20; hence y in A` by Th10; end; end; definition let N be non empty RelStr; redefine attr N is directed means :Def5: for x,y being Element of N ex z being Element of N st x <= z & y <= z; compatibility proof hereby assume N is directed; then A1: [#]N is directed by WAYBEL_0:def 6; let x,y be Element of N; x in the carrier of N & y in the carrier of N; then x in [#]N & y in [#]N by PRE_TOPC:12; then ex z being Element of N st z in [#]N & x <= z & y <= z by A1,WAYBEL_0:def 1; 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 & y in [#]N; consider z being Element of N such that A3: x <= z & y <= z by A2; take z; z in the carrier of N; hence z in [#]N by PRE_TOPC:12; thus x <= z & y <= z by A3; end; end; definition let X be set; cluster BoolePoset X -> directed; coherence proof let x,y be Element of BoolePoset X; take x "\/" y; A1: x "\/" y = x \/ y by YELLOW_1:17; x c= x \/ y & y c= x \/ y by XBOOLE_1:7; hence x <= x "\/" y & y <= x "\/" y by A1,YELLOW_1:2; end; end; definition cluster non empty directed transitive strict RelStr; existence proof take BoolePoset {}; thus thesis; end; end; Lm1: :: WAYBEL_0:3 ? 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 x' = x, y' = y as Element of N; consider z' being Element of N such that A2: x' <= z' & y' <= z' by A1,Def5; reconsider z = z' 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_1:def 9; hence x <= z & y <= z by ORDERS_1:def 9; end; assume A3: the RelStr of N is directed; let x,y be Element of N; reconsider x' = x, y' = y as Element of the RelStr of N; consider z' being Element of the RelStr of N such that A4: x' <= z' & y' <= z' by A3,Def5; reconsider z = z' as Element of N; take z; [x',z'] in the InternalRel of the RelStr of N & [y',z'] in the InternalRel of the RelStr of N by A4,ORDERS_1:def 9; hence x <= z & y <= z by ORDERS_1:def 9; 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 x' = x, y' = y, z' = z as Element of N; [x,y] in the InternalRel of the RelStr of N & [y,z] in the InternalRel of the RelStr of N by A2,A3,ORDERS_1:def 9; then x' <= y' & y' <= z' by ORDERS_1:def 9; then x' <= z' by A1,YELLOW_0:def 2; then [x',z'] in the InternalRel of N by ORDERS_1:def 9; hence x <= z by ORDERS_1:def 9; end; assume A4: the RelStr of N is transitive; let x,y,z be Element of N such that A5: x <= y and A6: y <= z; reconsider x' = x, y' = y, z' = z as Element of the RelStr of N ; [x',y'] in the InternalRel of the RelStr of N & [y',z'] in the InternalRel of the RelStr of N by A5,A6,ORDERS_1:def 9; then x' <= y' & y' <= z' by ORDERS_1:def 9; then x' <= z' by A4,YELLOW_0:def 2; then [x,z] in the InternalRel of N by ORDERS_1:def 9; hence x <= z by ORDERS_1:def 9; end; definition let M be non empty set, N be non empty RelStr, f be Function of M, the carrier of N, m be Element of M; redefine func f.m -> Element of N; coherence proof f.m is Element of N; hence thesis; end; end; definition let I be set; cluster yielding_non-empty_carriers (RelStr-yielding ManySortedSet of I); existence proof consider R being non empty RelStr; take I --> R; let i be set; A1: rng(I --> R) c= {R} by FUNCOP_1:19; assume i in rng(I --> R); hence i is non empty 1-sorted by A1,TARSKI:def 1; end; end; definition let I be non empty set; let J be yielding_non-empty_carriers (RelStr-yielding ManySortedSet of I); cluster product J -> non empty; coherence proof the carrier of product J = product Carrier J by YELLOW_1:def 4; hence the carrier of product J is non empty; end; end; theorem Th11: for R1,R2 being RelStr holds [#][:R1,R2:] = [:[#]R1,[#]R2:] proof let R1,R2 be RelStr; A1: [#]R1 = the carrier of R1 & [#]R2 = the carrier of R2 by PRE_TOPC:12; thus [#][:R1,R2:] = the carrier of [:R1,R2:] by PRE_TOPC:12 .= [:[#]R1,[#]R2:] by A1,YELLOW_3:def 2; end; definition let Y1,Y2 be directed RelStr; cluster [:Y1,Y2:] -> directed; coherence proof reconsider S1 = [#]Y1 as directed Subset of Y1 by WAYBEL_0:def 6; reconsider S2 = [#]Y2 as directed Subset of Y2 by WAYBEL_0:def 6; [:S1,S2:] is directed; then [#][:Y1,Y2:] is directed by Th11; hence thesis by WAYBEL_0:def 6; end; end; theorem Th12: 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 the carrier of R = the carrier of R~; end; Lm3: for R,S being RelStr, p,q being Element of R, p',q' being Element of S st p = p' & q = q' & the RelStr of R = the RelStr of S holds p <= q implies p' <= q' proof let R,S be RelStr, p,q be Element of R, p',q' be Element of S such that A1: p = p' & q = q' & the RelStr of R = the RelStr of S; assume p <= q; then [p',q'] in the InternalRel of S by A1,ORDERS_1:def 9; hence p' <= q' by ORDERS_1:def 9; end; definition let S be 1-sorted, N be NetStr over S; attr N is constant means :Def6: the mapping of N is constant; end; definition let R be RelStr, T be non empty 1-sorted, p be Element of T; func R --> p -> strict NetStr over T means :Def7: 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 the carrier of R, the carrier of T by FUNCOP_1:58; take NetStr(#the carrier of R, the InternalRel of R,f#); thus thesis; end; correctness; end; definition let R be RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> constant; coherence proof (the carrier of R --> p) --> p is constant; hence the mapping of R --> p is constant by Def7; end; end; definition let R be non empty RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> non empty; coherence proof the RelStr of R --> p = the RelStr of R by Def7; hence the carrier of R --> p is non empty; end; end; definition let R be non empty directed RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> directed; coherence proof A1: the RelStr of R --> p = the RelStr of R by Def7; the RelStr of R is directed by Lm1; hence thesis by A1,Lm1; end; end; definition let R be non empty transitive RelStr, T be non empty 1-sorted, p be Element of T; cluster R --> p -> transitive; coherence proof A1: the RelStr of R --> p = the RelStr of R by Def7; the RelStr of R is transitive by Lm2; hence thesis by A1,Lm2; end; end; theorem Th13: for R be RelStr, T be non empty 1-sorted, p be Element of T holds the carrier of 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 R --> p = the RelStr of R by Def7; hence the carrier of R --> p = the carrier of R; end; theorem Th14: for R be non empty RelStr, T be non empty 1-sorted, p be Element of T, q be Element of (R-->p) holds (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 R-->p; thus (R --> p).q = (the mapping of R --> p).q by WAYBEL_0:def 8 .= ((the carrier of R --> p) --> p).q by Def7 .= p by FUNCOP_1:13; end; definition let T be non empty 1-sorted, N be non empty NetStr over T; cluster the mapping of N -> non empty; coherence by FUNCT_2:def 1,RELAT_1:60; end; begin :: Substructures of Nets theorem Th15: for R being RelStr holds R is full SubRelStr of R proof let R be RelStr; the carrier of R c= the carrier of R & the InternalRel of R c= the InternalRel of R; then reconsider R' = R as SubRelStr of R by YELLOW_0:def 13; the InternalRel of R' = (the InternalRel of R)|_2 the carrier of R' by YELLOW_0:56; hence thesis by YELLOW_0:def 14; end; theorem Th16: 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; A1: the carrier of S c= the carrier of R & the InternalRel of S c= the InternalRel of R by YELLOW_0:def 13; the carrier of T c= the carrier of S & the InternalRel of T c= the InternalRel of S by YELLOW_0:def 13; then the carrier of T c= the carrier of R & the InternalRel of T c= the InternalRel of R by A1,XBOOLE_1:1; hence T is SubRelStr of R by YELLOW_0:def 13; end; definition let S be 1-sorted, N be NetStr over S; mode SubNetStr of N -> NetStr over S means :Def8: 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 Th15; thus the mapping of N = (the mapping of N)|the carrier of N by FUNCT_2:40; 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; A1: N is SubRelStr of N by Th15; the mapping of N = (the mapping of N)|the carrier of N by FUNCT_2:40; hence N is SubNetStr of N by A1,Def8; 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 Def8; S is SubRelStr of R by Def8; then A2: T is SubRelStr of R by A1,Th16; A3: the carrier of T c= the carrier of S by A1,YELLOW_0:def 13; the mapping of T = (the mapping of S)|the carrier of T by Def8 .= (the mapping of R)|(the carrier of S)|the carrier of T by Def8 .= (the mapping of R)|((the carrier of S) /\ the carrier of T) by RELAT_1:100 .= (the mapping of R)|the carrier of T by A3,XBOOLE_1:28; hence T is SubNetStr of R by A2,Def8; 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; A1: the NetStr of N is SubRelStr of N by YELLOW_0:def 13; the mapping of the NetStr of N = (the mapping of N)|the carrier of the NetStr of N by FUNCT_2:40; hence the NetStr of N is SubNetStr of N by A1,Def8; end; definition let S be 1-sorted, N be NetStr over S, M be SubNetStr of N; attr M is full means :Def9: 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 R' = the NetStr of R as SubRelStr of R by YELLOW_0:def 13; the InternalRel of R' = (the InternalRel of R)|_2 the carrier of R' by YELLOW_0:56; hence thesis by YELLOW_0:def 14; end; definition let S be 1-sorted, N be NetStr over S; cluster full strict 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; definition let S be 1-sorted, N be non empty NetStr over S; cluster full non empty strict 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 Th19: 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 Def8; hence the carrier of M c= the carrier of N by YELLOW_0:def 13; end; theorem Th20: 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 Def8; reconsider i' = i, j' = j as Element of M; i' <= j' by A2; hence x <= y by A1,YELLOW_0:60; end; theorem Th21: 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 and A2: x <= y; reconsider M as full non empty SubRelStr of N by Def9; reconsider i' = i, j' = j as Element of M; i' <= j' by A1,A2,YELLOW_0:61; hence i <= j; end; begin :: More about Nets definition let T be non empty 1-sorted; cluster constant strict net of T; existence proof consider R being non empty directed transitive RelStr, p being Element of T; take R --> p; thus thesis; end; end; definition let T be non empty 1-sorted, N be constant NetStr over T; cluster the mapping of N -> constant; coherence by Def6; 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 :Def10: 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; A2: rng f c= the carrier of T by RELSET_1:12; ex x being set st x in dom f & the_value_of f = f.x by Def1; then the_value_of f in rng f by FUNCT_1:def 5; hence thesis by A2; end; end; theorem Th22: for R be non empty RelStr, T be non empty 1-sorted, p be Element of T holds the_value_of (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 (R --> p) = the_value_of the mapping of R --> p by Def10 .= the_value_of ((the carrier of R --> p) --> p) by Def7 .= p by Th2; end; definition let T be non empty 1-sorted, N be net of T; canceled; mode subnet of N -> net of T means :Def12: ex f being map 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 TMAP_1:93; let m be Element of N; take n = m; let p be Element of N; assume n <= p; hence m <= (id N).p by TMAP_1:91; 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 TMAP_1:93; let m be Element of N; take n = m; let p be Element of N; assume n <= p; hence m <= (id N).p by TMAP_1:91; 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 map 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 map 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:55; 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 m1 <= f.p by A6; then m <= g.(f.p) by A5; hence m <= (g*f).p by FUNCT_2:21; end; theorem Th25: 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; A1: dom the mapping of N = the carrier of N by FUNCT_2:def 1; thus N.i = (the mapping of N).i by WAYBEL_0:def 8 .= the_value_of the mapping of N by A1,Def1 .= the_value_of N by Def10; end; theorem Th26: 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 by WAYBEL_0:def 11; 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 by WAYBEL_0:def 11; consider i being Element of N such that A3: i1 <= i and A4: i2 <= i by Def5; N.i in X & N.i in Y by A1,A2,A3,A4; hence X meets Y by XBOOLE_0:3; end; theorem Th27: 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; consider f being map 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 Def12; let i be Element of N; 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,WAYBEL_0:def 12; take f.m; thus i <= f.m by A4,A5; N.(f.m) = (the mapping of N).(f.m) by WAYBEL_0:def 8 .= ((the mapping of N)*f).m by FUNCT_2:21 .= M.m by A2,WAYBEL_0:def 8; hence N.(f.m) in X by A6; end; theorem Th28: 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 and A3: j <= z by Def5; take z; thus j <= z & N.z in X by A1,A2,A3; end; theorem Th29: 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; consider i being Element of N; take i; let j be Element of N; assume i <= j; thus N.j in the carrier of S; 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 :Def13: 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, the carrier of S by FUNCT_2:38; set S = NetStr(#c,i,m#); A1: i c= the InternalRel of N by WELLORD1:15; then S is SubRelStr of N by YELLOW_0:def 13; then reconsider S as strict SubNetStr of N by Def8; take S; thus thesis by A1,YELLOW_0:def 13,def 14; suppose S is empty; then the carrier of S = {} by STRUCT_0:def 1; then the mapping of N = {} by PARTFUN1:64; then A2: c = {} by RELAT_1:172; then reconsider m = {} as Function of c, the carrier of S by FUNCT_2:55,RELAT_1:60; set S = NetStr(#c,i,m#); A3: i c= the InternalRel of N by WELLORD1:15; then A4: S is SubRelStr of N by YELLOW_0:def 13; the mapping of S = (the mapping of N)|the carrier of S by A2,RELAT_1:110; then reconsider S as strict SubNetStr of N by A4,Def8; take S; thus thesis by A3,YELLOW_0:def 13,def 14; 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 RelStr of it1 = the RelStr of it2 by A5,A6,A7,A8,YELLOW_0:58; the mapping of it1 = (the mapping of N)|the carrier of it2 by A6,A8,Def8 .= the mapping of it2 by Def8; hence it1 = it2 by A9; end; end; definition 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 Def13; M is transitive; hence thesis by Def9; end; end; theorem Th30: 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; consider i being Element of N; consider j being Element of N such that i <= j and A2: N.j in X by A1,WAYBEL_0:def 12; (the mapping of N).j in X by A2,WAYBEL_0:def 8; then j in (the mapping of N)"X by FUNCT_2:46; hence the carrier of N"X is non empty by Def13; then reconsider M = N"X as non empty full SubNetStr of N by STRUCT_0:def 1; M is directed proof let i,j be Element of M; A3: i in the carrier of M & j in the carrier of M; the carrier of M c= the carrier of N by Th19; then reconsider x = i, y = j as Element of N by A3; consider z being Element of N such that A4: x <= z & y <= z by Def5; consider e being Element of N such that A5: z <= e and A6: N.e in X by A1,WAYBEL_0:def 12; (the mapping of N).e in X by A6,WAYBEL_0:def 8; then e in (the mapping of N)"X by FUNCT_2:46; then e in the carrier of N"X by Def13; then reconsider k = e as Element of M; take k; x <= e & y <= e by A4,A5,YELLOW_0:def 2; hence i <= k & j <= k by Th21; end; hence thesis; end; theorem Th31: 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 Th30; M is subnet of N proof set f = id M; the carrier of M c= the carrier of N by Th19; then f is Function of the carrier of M, the carrier of N by FUNCT_2:9; then reconsider f as map of M,N; take f; A2: id M = id the carrier of M by GRCAT_1:def 11; the mapping of M = (the mapping of N)|the carrier of M by Def8; hence the mapping of M = (the mapping of N)*f by A2,RELAT_1:94; let m be Element of N; consider j being Element of N such that A3: m <= j and A4: N.j in X by A1,WAYBEL_0:def 12; (the mapping of N).j in X by A4,WAYBEL_0:def 8; then j in (the mapping of N)"X by FUNCT_2:46; then j in the carrier of M by Def13; then reconsider n = j as Element of M; take n; let p be Element of M such that A5: n <= p; f.p = p by TMAP_1:91; then j <= f.p by A5,Th20; hence m <= f.p by A3,YELLOW_0:def 2; end; hence thesis; end; theorem Th32: 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; consider i being 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,Def13; then A2: (the mapping of N).j in X by FUNCT_1:def 13; the mapping of M = (the mapping of N)|the carrier of M by A1,Def8; then (the mapping of M).j in X by A2,FUNCT_1:72; hence M.j in X by WAYBEL_0:def 8; end; begin :: The Universe of Nets definition let X be non empty 1-sorted; func NetUniv X means :Def14: for x 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 set I = the_universe_of the carrier of X; 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 }; consider M being ManySortedSet of I such that A1: for i being set st i in I holds M.i = f(i) from MSSLambda; A2: Union M = union rng M by PROB_1:def 3; take IT = Union M; let x; 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 such that A5: z in dom M and A6: M.z = y by A4,FUNCT_1:def 5; z in I by A5,PBOOLE:def 3; 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,PBOOLE:def 3; 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,PBOOLE:def 3; then A11: M.i in rng M by FUNCT_1:def 5; A12: 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; the mapping of N in Funcs(i, the carrier of X) by FUNCT_2:11; then N in M.i by A12; hence x in IT by A2,A9,A11,TARSKI:def 4; end; uniqueness proof defpred P[set] 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 set holds x in X1 iff P[x]) & (for x being set holds x in X2 iff P[x]) holds X1 = X2 from SetEq; end; end; definition let X be non empty 1-sorted; cluster NetUniv X -> non empty; coherence proof set V = the_universe_of the carrier of X; {} in {{}} by TARSKI:def 1; then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:8; 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_1:def 9; end; A2: R is transitive proof let x,y,z be Element of R; thus thesis by A1; end; 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; consider q being Element of X; set N = R --> q; A3: the RelStr of N = the RelStr of R by Def7; {} in V by CLASSES2:62; then the carrier of N in V by A3,CLASSES2:3; hence thesis by Def14; 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 N is constant net of S2 by Def6; end; Lm7: for S1,S2 being non empty 1-sorted st the carrier of S1 = the carrier of S2 for N being strict net of S1 holds N is strict 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 strict net of S1; reconsider M = N as net of S2 by A1; A2: the carrier of N = the carrier of M & the InternalRel of N = the InternalRel of M & the mapping of N = the mapping of M; M = the NetStr of N .= the NetStr of M by A2; hence N is strict net of S2; end; Lm8: 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; assume A1: the carrier of S1 = the carrier of S2; defpred P[set] means ex N being strict net of S2 st N = $1 & the carrier of N in the_universe_of the carrier of S2; A2: now let x; 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 Def14; reconsider N as strict net of S2 by A1,Lm7; 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,Lm7; 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 Def14; end; A5: for x holds x in NetUniv S2 iff P[x] by Def14; thus NetUniv S1 = NetUniv S2 from Extensionality(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 :Def15: for i being set st i in rng it holds i is net of T; existence proof consider N being net of T; take X --> N; let i be set; assume A1: i in rng(X --> N); then dom(X --> N) <> {} by RELAT_1:65; then X <> {} by PBOOLE:def 3; then rng(X --> N) = {N} by FUNCOP_1:14; hence thesis by A1,TARSKI:def 1; end; end; theorem Th33: 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 PBOOLE:def 3; then F.i in rng F by FUNCT_1:def 5; hence F.i is net of T by A1,Def15; 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 A3: ex i being set st i in dom F & x = F.i by FUNCT_1:def 5; dom F = X by PBOOLE:def 3; hence x is net of T by A2,A3; 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; coherence by Th33; end; definition let X be set, T be 1-sorted; cluster -> RelStr-yielding 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 v is RelStr by Def15; end; end; definition let T be 1-sorted, Y be net of T; cluster -> yielding_non-empty_carriers net_set of the carrier of Y,T; coherence proof let J be net_set of the carrier of Y,T; let i be set; assume i in rng J; hence i is non empty 1-sorted by Def15; 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; 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,set] 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 Def5; reconsider z = zi as set; take z; thus P[i,z] by A3,ORDERS_1:def 9; 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 MSSExD(A2); A5: dom z = the carrier of Y by PBOOLE:def 3 .= dom Carrier J by PBOOLE:def 3; now let i be set; assume i in dom Carrier J; then i in the carrier of Y by PBOOLE:def 3; 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:106; hence z.i in (Carrier J).i by Th9; end; then z in product Carrier J by A5,CARD_3:18; then reconsider z as Element of product J by A1; take z; for i be set 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 set; 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 xi <= zi by ORDERS_1:def 9; end; hence x <= z by A1,YELLOW_1:def 4; for i be set 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 set; 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 yi <= zi by ORDERS_1:def 9; end; hence y <= z 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; consider fx,gy being Function such that A8: fx = x & gy = y and A9: for i be set 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; consider fy,gz being Function such that A10: fy = y & gz = z and A11: for i be set 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; for i be set 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 set; assume A12: 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 A13: R1 = J.i & xi = x .i & yi = y.i & xi <= yi by A8,A9,A12; consider R2 being RelStr, yi',zi being Element of R2 such that A14: R2 = J.i & yi' = y.i & zi = z.i & yi' <= zi by A10,A11,A12; reconsider xi, zi as Element of J.j by A13,A14; take J.j, xi, zi; thus J.j = J.i & xi = x .i & zi = z.i by A13,A14; thus xi <= zi by A13,A14,YELLOW_0:def 2; end; hence x <= z by A1,YELLOW_1:def 4; end; end; definition let X be set, T be 1-sorted; cluster -> yielding_non-empty_carriers 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 v is non empty 1-sorted by Def15; end; end; definition let X be set, T be 1-sorted; cluster yielding_non-empty_carriers net_set of X,T; existence proof consider F being 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 :Def16: 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 set R = [:Y, product J:]; deffunc F(Element of Y, Element of product J) = (the mapping of J.$1).($2.$1); 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:], the carrier of T such that A2: for i being Element of Y, f being Element of product J holds F. [i,f] = F(i,f) from Kappa2D(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 the carrier of R, the carrier of 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 (the mapping of N).(i,f) = F. [i,f] by BINOP_1:def 1 .=(the mapping of J.i).(f.i) 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:], the carrier of 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:9; reconsider d = c2 as Element of product Carrier J by YELLOW_1:def 4; thus m1.c = m1.(c1,d) by A8,BINOP_1:def 1 .= (the mapping of J.c1).(d.c1) by A5 .= m2.(c1,d) by A7 .= m2.c by A8,BINOP_1:def 1; end; hence IT1 = IT2 by A4,A6,FUNCT_2:113; end; end; theorem Th34: 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; the RelStr of Iterated J = [:Y, product J:] by Def16; then A3: the carrier of Iterated J = [:the carrier of Y, the carrier of product J:] by YELLOW_3:def 2; A4: ex N being strict net of T st N = Y & the carrier of N in the_universe_of the carrier of T by A1,Def14; then A5: dom Carrier J in the_universe_of the carrier of T by PBOOLE:def 3; rng Carrier J c= the_universe_of the carrier of T proof let x; assume x in rng Carrier J; then consider y such that A6: y in dom Carrier J and A7: (Carrier J).y = x by FUNCT_1:def 5; reconsider i = y as Element of Y by A6,PBOOLE:def 3; 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 Def14; hence x in the_universe_of the carrier of T by A7,Th9; end; then product Carrier J in the_universe_of the carrier of T by A5,Th5; 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 A3,A4,CLASSES2:67; hence Iterated J in NetUniv T by Def14; end; theorem Th35: 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 Def16; 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 Th36: 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] by WAYBEL_0:def 8 .= (the mapping of Iterated J).(i,f) by BINOP_1:def 1 .= (the mapping of J.i).(f.i) by Def16; end; theorem Th37: 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 { rng the mapping of J.i where i is Element of Y: not contradiction } 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 set; set X = { rng the mapping of J.i where i is Element of Y: not contradiction }; assume x in rng the mapping of Iterated J; then consider y being set such that A1: y in dom the mapping of Iterated J and A2: (the mapping of Iterated J).y = x by FUNCT_1:def 5; y in the carrier of Iterated J by A1; then y in [:the carrier of Y, product Carrier J:] by Th35; then consider y1 being Element of Y, y2 being Element of product Carrier J such that A3: y = [y1,y2] by DOMAIN_1:9; A4: y1 in the carrier of Y; y2 in product Carrier J; then A5: y2 in the carrier of product J by YELLOW_1:def 4; y1 in dom Carrier J by A4,PBOOLE:def 3; then y2.y1 in (Carrier J).y1 by CARD_3:18; then y2.y1 in the carrier of J.y1 by Th9; then A6: y2.y1 in dom the mapping of J.y1 by FUNCT_2:def 1; x = (the mapping of Iterated J).(y1,y2) by A2,A3,BINOP_1:def 1 .= (the mapping of J.y1).(y2.y1) by A5,Def16; then A7: x in rng the mapping of J.y1 by A6,FUNCT_1:def 5; reconsider y1 as Element of Y; rng the mapping of J.y1 in X; hence x in union X by A7,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 :Def17: (InclPoset { V where V is Subset of T: p in V & V is open })~; correctness; end; definition 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 }; p in [#]T & [#]T is open by PRE_TOPC:13,TOPS_1:53; then [#]T in Xp; then [#]T in the carrier of InclPoset Xp by YELLOW_1:1; then [#]T in the carrier of (InclPoset Xp)~ by Th12; hence the carrier of OpenNeighborhoods p is non empty by Def17; end; end; theorem Th38: 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 OpenNeighborhoods p; then x in the carrier of (InclPoset X)~ by Def17; then x in the carrier of InclPoset X by Th12; then x in X by YELLOW_1:1; hence thesis; end; theorem Th39: 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 Th38; hence thesis; end; assume that A1: p in x and A2: x is open; i in Xp by A1,A2; then x in the carrier of InclPoset Xp by YELLOW_1:1; then x in the carrier of (InclPoset Xp)~ by Th12; hence x in the carrier of OpenNeighborhoods p by Def17; end; theorem Th40: 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; let x,y be Element of OpenNeighborhoods p; set X = { V where V is Subset of T: p in V & V is open }; p in [#]T & [#]T is open by PRE_TOPC:13,TOPS_1:53; then [#]T in X; then reconsider X as non empty set; A1: OpenNeighborhoods p = (InclPoset X)~ by Def17; (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 by A1; A2: x = a~ & y = b~ by LATTICE3:def 6; b <= a iff y c= x by YELLOW_1:3; hence x <= y iff y c= x by A1,A2,LATTICE3:9; end; definition let T be non empty TopSpace, p be Point of T; cluster OpenNeighborhoods p -> transitive directed; coherence proof set X = { V where V is Subset of T: p in V & V is open }; A1: OpenNeighborhoods p = (InclPoset X)~ by Def17; hence OpenNeighborhoods p is transitive; let x,y be Element of OpenNeighborhoods p; consider V being Subset of T such that A2: x = V & p in V & V is open by Th38; consider W being Subset of T such that A3: y = W & p in W & W is open by Th38; set z = V /\ W; p in z & z is open by A2,A3,TOPS_1:38,XBOOLE_0:def 3; then z in X; then z in the carrier of InclPoset X by YELLOW_1:1; then z in the carrier of (InclPoset X)~ by Th12; then reconsider z as Element of OpenNeighborhoods p by A1; take z; z c= x & z c= y by A2,A3,XBOOLE_1:17; hence x <= z & y <= z by Th40; 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 :Def18: 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 SubsetEx; 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 SubsetEq(A2,A3); end; end; theorem Th41: 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; consider f being map 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 Def12; let x; 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,Def18; then consider ii being Element of N such that A4: for j being Element of N st ii <= j holds N.j in V by WAYBEL_0:def 11; 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 n <= j; then A6: ii <= f.j by A5; N.(f.j) = (the mapping of N).(f.j) by WAYBEL_0:def 8 .= ((the mapping of N)*f).j by FUNCT_2:21 .= Y.j by A1,WAYBEL_0:def 8; hence Y.j in V by A4,A6; end; hence x in Lim Y by Def18; end; theorem Th42: 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 let S be a_neighborhood of p; consider i being Element of N; take i; let j be Element of N such that i <= j; N.j = p by Th25; hence N.j in S by CONNSP_2:6; end; hence p in Lim N by Def18; end; theorem Th43: 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 set; 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,Def18; then consider i being Element of N such that A2: for j being Element of N st i <= j holds N.j in G by WAYBEL_0:def 11; consider e being Element of N such that A3: d <= e and A4: i <= e by Def5; A5: N.e in G by A2,A4; N.e in S by A3; hence G meets S by A5,XBOOLE_0:3; end; hence p in Cl S by Th6; end; theorem Th44: 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,COMPTS_1:def 4; W is a_neighborhood of p1 by A5,A7,CONNSP_2:5; then A10: N is_eventually_in W by A2,Def18; V is a_neighborhood of p2 by A6,A8,CONNSP_2:5; then N is_eventually_in V by A3,Def18; hence contradiction by A9,A10,Th26; 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; A14: cpN = [:the carrier of OpenNeighborhoods p, the carrier of OpenNeighborhoods q:] by YELLOW_3:def 2; deffunc F(Element of cpN) = $1`1 /\ $1`2; A15: 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 A16: W = i`1 & p in W & W is open by Th38; consider V being Subset of T such that A17: V = i`2 & q in V & V is open by Th38; A18: W /\ V c= cT; i`1 meets i`2 by A13,A16,A17; then i`1 /\ i`2 <> {} by XBOOLE_0:def 7; then cT /\ (i`1 /\ i`2) <> {} by A16,A17,A18,XBOOLE_1:28; hence cT meets i`1 /\ i`2 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 M_Choice(A15); reconsider N = NetStr(#the carrier of pN, the InternalRel of pN, f#) as net of T by Lm1,Lm2; now let V be a_neighborhood of p; A20: Int V c= V by TOPS_1:44; N is_eventually_in Int V proof p in Int V & Int V is open by CONNSP_2:def 1,TOPS_1:51; then A21: Int V in the carrier of OpenNeighborhoods p by Th39; q in [#]T & [#]T is open by PRE_TOPC:13,TOPS_1:53; then [#]T in the carrier of OpenNeighborhoods q by Th39; then [Int V,[#]T] in cpN by A14,A21,ZFMISC_1:106; then reconsider i = [Int V,[#]T] as Element of N; take i; let j be Element of N; consider j1 being Element of OpenNeighborhoods p, j2 being Element of OpenNeighborhoods q such that A22: j = [j1,j2] by A14,DOMAIN_1:9; A23: j`1 = j1 & j`2 = j2 by A22,MCART_1:7; consider W1 being Subset of T such that A24: j1 = W1 & p in W1 & W1 is open by Th38; consider W2 being Subset of T such that A25: j2 = W2 & q in W2 & W2 is open by Th38; reconsider j'=j, i'=i as Element of pN; A26: i'`1 = Int V & i'`2 = [#]T by MCART_1:7; assume i <= j; then [i,j] in the InternalRel of pN by ORDERS_1:def 9; then i' <= j' by ORDERS_1:def 9; then i'`1 <= j'`1 & i'`2 <= j'`2 by YELLOW_3:12; then A27: W1 c= Int V & W2 c= [#]T by A23,A24,A25,A26,Th40; A28: f.j in W1 /\ W2 by A19,A23,A24,A25; W1 /\ W2 c= (Int V) /\ [#]T by A27,XBOOLE_1:27; then f.j in (Int V) /\ [#]T by A28; then f.j in Int V by PRE_TOPC:15; hence N.j in Int V by WAYBEL_0:def 8; end; hence N is_eventually_in V by A20,WAYBEL_0:8; end; then A29: p in Lim N by Def18; now let V be a_neighborhood of q; A30: Int V c= V by TOPS_1:44; N is_eventually_in Int V proof q in Int V & Int V is open by CONNSP_2:def 1,TOPS_1:51; then A31: Int V in the carrier of OpenNeighborhoods q by Th39; p in [#]T & [#]T is open by PRE_TOPC:13,TOPS_1:53; then [#]T in the carrier of OpenNeighborhoods p by Th39; then [[#]T,Int V] in cpN by A14,A31,ZFMISC_1:106; then reconsider i = [[#]T,Int V] as Element of N; take i; let j be Element of N; consider j1 being Element of OpenNeighborhoods p, j2 being Element of OpenNeighborhoods q such that A32: j = [j1,j2] by A14,DOMAIN_1:9; A33: j`1 = j1 & j`2 = j2 by A32,MCART_1:7; consider W1 being Subset of T such that A34: j1 = W1 & p in W1 & W1 is open by Th38; consider W2 being Subset of T such that A35: j2 = W2 & q in W2 & W2 is open by Th38; reconsider j'=j, i'=i as Element of pN; A36: i'`1 = [#]T & i'`2 = Int V by MCART_1:7; assume i <= j; then [i,j] in the InternalRel of pN by ORDERS_1:def 9; then i' <= j' by ORDERS_1:def 9; then i'`1 <= j'`1 & i'`2 <= j'`2 by YELLOW_3:12; then A37: W1 c= [#]T & W2 c= Int V by A33,A34,A35,A36,Th40; A38: f.j in W1 /\ W2 by A19,A33,A34,A35; W1 /\ W2 c= (Int V) /\ [#]T by A37,XBOOLE_1:27; then f.j in (Int V) /\ [#]T by A38; then f.j in Int V by PRE_TOPC:15; hence N.j in Int V by WAYBEL_0:def 8; end; hence N is_eventually_in V by A30,WAYBEL_0:8; end; then q in Lim N by Def18; hence contradiction by A11,A12,A29; end; definition 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 Th44; hence thesis by SPPOL_1:4; end; end; definition let T be non empty TopSpace, N be net of T; attr N is convergent means :Def19: Lim N <> {}; end; definition let T be non empty TopSpace; cluster constant -> convergent net of T; coherence proof let N be net of T; assume N is constant; hence Lim N <> {} by Th42; end; end; definition let T be non empty TopSpace; cluster convergent strict net of T; existence proof consider R being non empty transitive directed RelStr, p being Point of T; take 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 :Def20: it in Lim N; existence proof Lim N <> {} by Def19; then consider p being Point of T such that A1: p in Lim N by SUBSET_1:10; take p; thus thesis by A1; end; correctness by SPPOL_1:4; 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 Th42; hence lim N = the_value_of N by Def20; 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 Def18; 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 Th31; A2: Y is_eventually_in (the carrier of T) \ V by Th32; take Y; let Z be subnet of Y; assume p in Lim Z; then Z is_eventually_in V by Def18; then Z is_often_in V by Th28; then Y is_often_in V by Th27; hence contradiction by A2,WAYBEL_0:10; end; theorem Th47: 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 A1: N in NetUniv T; 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 Def18; 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 Th31; A3: ex M being strict net of T st M = N & the carrier of M in the_universe_of the carrier of T by A1,Def14; A4: Y is_eventually_in (the carrier of T) \ V by Th32; take Y; the carrier of Y = (the mapping of N)"((the carrier of T) \ V) by Def13; then the carrier of Y in the_universe_of the carrier of T by A3,CLASSES1:def 1; hence Y in NetUniv T by Def14; let Z be subnet of Y; assume p in Lim Z; then Z is_eventually_in V by Def18; then Z is_often_in V by Th28; then Y is_often_in V by Th27; hence contradiction by A4,WAYBEL_0:10; end; theorem Th48: 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; A3: Int V = Int Int V by TOPS_1:45; then 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,Def18; then consider i being Element of N such that A4: for j being Element of N st i <= j holds N.j in W by WAYBEL_0:def 11; defpred P[Element of N,set] 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); A5: for j being Element of N ex e being set st P[j, e] proof let j be Element of N; reconsider j' = j as Element of N; per cases; suppose i <= j; then A6: N.j' in W by A4; A7: N.j in Lim(J.j) by A2; W is a_neighborhood of N.j by A3,A6,CONNSP_2:def 1; then J.j is_eventually_in W by A7,Def18; then consider e being Element of J.j such that A8: for u being Element of J.j st e <= u holds J.j.u in W by WAYBEL_0:def 11; take e,e; thus e = e; assume i <= j; thus for n being Element of J.j st e <= n holds J.j.n in W by A8; suppose A9: not i <= j; consider e being Element of J.j; take e,e; thus e = e & (i <= j implies for n being Element of J.j st e <= n holds J.j.n in W) by A9; end; consider f being ManySortedSet of the carrier of N such that A10: for j being Element of N holds P[j, f.j] from MSSExD(A5); A11: the carrier of Iterated J = [:the carrier of N, product Carrier J:] by Th35; dom Carrier J = the carrier of N by PBOOLE:def 3; then A12: dom f = dom Carrier J by PBOOLE:def 3; for x st x in dom Carrier J holds f.x in (Carrier J).x proof let x; assume x in dom Carrier J; then reconsider j = x as Element of N by PBOOLE:def 3; 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 A10; then f.x in the carrier of J.j; hence f.x in (Carrier J).x by Th9; end; then A13: f in product Carrier J by A12,CARD_3:18; then [i,f] in the carrier of Iterated J by A11,ZFMISC_1:106; then reconsider x = [i,f] as Element of Iterated J; take x; let j be Element of Iterated J such that A14: x <= j; consider j1 being Element of N, j2 being Element of product Carrier J such that A15: j = [j1,j2] by A11,DOMAIN_1:9; product Carrier J = the carrier of product J by YELLOW_1:def 4; then reconsider j2, i2 = f as Element of product J by A13; reconsider i1 = i, j1 as Element of N; the RelStr of Iterated J = [:N, product J:] by Def16; then A16: [i1,i2] <= [j1,j2] by A14,A15,YELLOW_0:1; then A17: i1 <= j1 & i2 <= j2 by YELLOW_3:11; consider m being Element of J.j1 such that A18: m = f.j1 and A19: i <= j1 implies for n being Element of J.j1 st m <= n holds J.j1.n in W by A10; i2 in the carrier of product J; then i2 in product Carrier J by YELLOW_1:def 4; then ex f,g being Function st f = i2 & g = j2 & for i be set 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 A17,YELLOW_1:def 4; then ex R being RelStr, xi,yi being Element of R st R = J.j1 & xi = i2.j1 & yi = j2.j1 & xi <= yi; then (J.j1).(j2.j1) in W by A16,A18,A19,YELLOW_3:11; then (the mapping of J.j1).(j2.j1) in W by WAYBEL_0:def 8; then A20: (Iterated J).j in W by A15,Th36; W c= V by TOPS_1:44; hence (Iterated J).j in V by A20; end; hence p in Lim Iterated J by Def18; end; begin :: Convergence Classes definition let S be non empty 1-sorted; mode Convergence-Class of S means :Def21: it c= [:NetUniv S,the carrier of S:]; existence; end; definition let S be non empty 1-sorted; cluster -> Relation-like Convergence-Class of S; coherence proof let C be Convergence-Class of S; C is Subset of [:NetUniv S,the carrier of S:] by Def21; hence thesis; end; end; definition let T be non empty TopSpace; func Convergence T -> Convergence-Class of T means :Def22: 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[set,set] 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 holds [x,y] in R iff x in NetUniv T & y in the carrier of T & P[x,y] from Rel_On_Set_Ex; reconsider R as Convergence-Class of T by Def21; 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 N' being net of T, p' being Point of T st N' = N & p' = p & p' in Lim N' 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; A5: it1 c= [:NetUniv T,the carrier of T:] by Def21; A6: it2 c= [:NetUniv T,the carrier of T:] by Def21; let x,y; thus [x,y] in it1 implies [x,y] in it2 proof assume A7: [x,y] in it1; then x in NetUniv T by A5,ZFMISC_1:106; then consider N being strict net of T such that A8: N = x and the carrier of N in the_universe_of the carrier of T by Def14 ; reconsider p = y as Point of T by A5,A7,ZFMISC_1:106; [N,p] in it1 by A7,A8; then N in NetUniv T & p in Lim N by A3; hence [x,y] in it2 by A4,A8; end; assume A9: [x,y] in it2; then x in NetUniv T by A6,ZFMISC_1:106; then consider N being strict net of T such that A10: N = x and the carrier of N in the_universe_of the carrier of T by Def14 ; reconsider p = y as Point of T by A6,A9,ZFMISC_1:106; [N,p] in it2 by A9,A10; then N in NetUniv T & p in Lim N by A4; hence [x,y] in it1 by A3,A10; end; end; definition let T be non empty 1-sorted, C be Convergence-Class of T; attr C is (CONSTANTS) means :Def23: 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 :Def24: 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 :Def25: 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 :Def26: 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; definition 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 Th42; hence [N,the_value_of N] in C by A1,Def22; 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; A3: Lim N c= Lim Y by Th41; assume [N,p] in C; then p in Lim N by Def22; hence [Y,p] in C by A2,A3,Def22; 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,Def22; 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,Th47; take Y; thus Y in NetUniv T by A5; let Z be subnet of Y; not p in Lim Z by A6; hence not [Z,p] in C by Def22; end; let X be net of T, p be Element of T; assume [X,p] in C; then A7: p in Lim X & X in NetUniv T by Def22; 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 Def22; end; then A10: p in Lim Iterated J by A7,Th48; Iterated J in NetUniv T by A7,A9,Th34; hence [Iterated J,p] in C by A10,Def22; end; end; definition let S be non empty 1-sorted, C be Convergence-Class of S; func ConvergenceSpace C -> strict TopStruct means :Def27: 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 of bool the carrier of S from SubsetD; reconsider X as Subset-Family of S by SETFAM_1:def 7; take TopStruct(#the carrier of S,X#); thus thesis; end; correctness; end; definition 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 Def27; hence the carrier of ConvergenceSpace C is non empty; end; end; definition 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 Def27 ; reconsider V = [#]IT as Subset of S by Def27; V = the carrier of IT by PRE_TOPC:12 .= the carrier of S by Def27; 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 Th29; then V in the topology of IT by A1; hence the carrier of IT in the topology of IT by PRE_TOPC:12; 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 Def27; 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; let N be net of S such that A5: [N,p] in C; X in the topology of IT by A2,A4; then consider W being Subset of S such that A6: X = W and A7: 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; A8: N is_eventually_in X by A3,A5,A6,A7; X c= V by A4,ZFMISC_1:92; hence N is_eventually_in V by A8,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 A9: a = Va and A10: 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; assume b in the topology of IT; then consider Vb being Subset of S such that A11: b = Vb and A12: 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; reconsider V = a /\ b as Subset of S by Def27; now let p be Element of S such that A13: p in V; let N be net of S; assume A14: [N,p] in C; p in a by A13,XBOOLE_0:def 3; then N is_eventually_in Va by A9,A10,A14; then consider i1 being Element of N such that A15: for j being Element of N st i1 <= j holds N.j in Va by WAYBEL_0:def 11; p in b by A13,XBOOLE_0:def 3; then N is_eventually_in Vb by A11,A12,A14; then consider i2 being Element of N such that A16: for j being Element of N st i2 <= j holds N.j in Vb by WAYBEL_0:def 11; consider i being Element of N such that A17: i1 <= i and A18: i2 <= i by Def5; thus N is_eventually_in V proof take i; let j be Element of N; assume A19: i <= j; then i1 <= j by A17,YELLOW_0:def 2; then A20: N.j in Va by A15; i2 <= j by A18,A19,YELLOW_0:def 2; then N.j in Vb by A16; hence N.j in V by A9,A11,A20,XBOOLE_0:def 3; end; end; hence a /\ b in the topology of IT by A1; end; end; theorem Th49: 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; A1: C c= [:NetUniv S,the carrier of S:] by Def21; A2: the carrier of S = the carrier of T by Def27; assume A3: [x,y] in C; then consider M being Element of NetUniv S, p being Element of S such that A4: [x,y] = [M,p] by A1,DOMAIN_1:9; A5: M in NetUniv S; ex N being strict net of S st N = M & the carrier of N in the_universe_of the carrier of S by Def14; then reconsider M as net of S; reconsider N = M as net of T by Def27; A6: N in NetUniv T by A2,A5,Lm8; reconsider q = p as Point of T by Def27; A7: 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 Def27; now let V be a_neighborhood of q; A8: Int V c= V by TOPS_1:44; A9: p in Int V by CONNSP_2:def 1; Int V is open by TOPS_1:51; then Int V in the topology of T by PRE_TOPC:def 5; then 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 A7; then M is_eventually_in Int V by A3,A4,A9; then consider ii being Element of M such that A10: for j being Element of M st ii <= j holds M.j in Int V by WAYBEL_0:def 11; reconsider i = ii as Element of N; now let j be Element of N such that A11: i <= j; reconsider jj = j as Element of M; M.jj = (the mapping of M).jj by WAYBEL_0:def 8 .= (the mapping of N).jj .= N.j by WAYBEL_0:def 8; hence N.j in Int V by A10,A11; end; then N is_eventually_in Int V by WAYBEL_0:def 11; hence N is_eventually_in V by A8,WAYBEL_0:8; end; then p in Lim N by Def18; hence [x,y] in Convergence T by A4,A6,Def22; end; definition let T be non empty 1-sorted, C be Convergence-Class of T; attr C is topological means :Def28: C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS); end; definition let T be non empty 1-sorted; cluster non empty topological Convergence-Class of T; existence proof reconsider C = [:NetUniv T, the carrier of T:] as Convergence-Class of T by Def21; take C; thus C is non empty; thus C is topological proof thus C is (CONSTANTS) proof let N be constant net of T; thus thesis by ZFMISC_1:106; end; thus C is (SUBNETS) proof let N be net of T, Y be subnet of N; thus thesis by ZFMISC_1:106; end; thus C is (DIVERGENCE) proof let X be net of T, p be Element of T; thus thesis by ZFMISC_1:106; end; 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:106; 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:106; end; then Iterated J in NetUniv T by A1,Th34; hence [Iterated J,p] in C by ZFMISC_1:106; end; end; end; definition let T be non empty 1-sorted; cluster topological -> (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) Convergence-Class of T; coherence by Def28; cluster (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS) -> topological Convergence-Class of T; coherence by Def28; end; theorem Th50: 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 carrier of ConvergenceSpace C = the carrier of T by Def27; A2: 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 Def27; then A3: (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; 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 by A2; hence thesis by A3,PRE_TOPC:def 5; end; theorem Th51: 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 Def27; hereby assume A2: S is closed; let p be Element of T; let N be net of T such that A3: [N,p] in C; A4: S` is open by A2,TOPS_1:29; assume N is_often_in S; then not N is_eventually_in (the carrier of T)\S by WAYBEL_0:10; then not N is_eventually_in [#]CC\S by A1,PRE_TOPC:12; then not N is_eventually_in S` by PRE_TOPC:17; then not p in S` by A3,A4,Th50; hence p in S by A1,Th10; end; assume A5: 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 A6: not p in S by Th10; let N be net of T; assume [N,p] in C; then not N is_often_in S by A5,A6; then N is_eventually_in (the carrier of CC)\S by A1,WAYBEL_0:10; then N is_eventually_in [#]CC\S by PRE_TOPC:12; hence N is_eventually_in S` by PRE_TOPC:17; end; then S` is open by Th50; hence S is closed by TOPS_1:29; end; theorem Th52: 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 SubsetD; 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; 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 Def21; then A4: N in NetUniv T by A2,ZFMISC_1:106; reconsider M = N"F as subnet of N by A3,Th31; defpred P[Element of M, set] 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; A6: the mapping of M = (the mapping of N)|the carrier of M by Def8; i in the carrier of M; then i in (the mapping of N)"F by Def13; then (the mapping of N).i in F by FUNCT_2:46; then (the mapping of M).i in F by A6,FUNCT_1:72; then M.i in F by WAYBEL_0:def 8; 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 set; take x; thus P[i, x] proof thus [x,M.i] in C by A7,A9; reconsider X = N as net of T by Def27; take X; thus X = x; thus rng the mapping of X c= S 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 MSSExD(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 Th33; 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; reconsider I = Iterated J as net of CC by Def27; A13: ex N0 being strict net of T st N0 = N & the carrier of N0 in the_universe_of the carrier of T by A4,Def14; the carrier of M = (the mapping of N)"F by Def13; then the carrier of M in the_universe_of the carrier of T by A13,CLASSES1:def 1; then M in NetUniv T by Def14; then [M,p] in C by A2,Def24; then A14: [I,p] in C by A12,Def26; set XX = { rng the mapping of J.i where i is Element of M: not contradiction }; A15: rng the mapping of I c= union XX by Th37; 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 x c= S by A12; end; then union XX c= S by ZFMISC_1:94; then A16: rng the mapping of I c= S by A15,XBOOLE_1:1; reconsider q = p as Point of CC by Def27; C c= Convergence CC by Th49; then q in Lim I by A14,Def22; hence p in F by A14,A16; end; then A17: F is closed by Th51; S c= F proof let x; assume A18: x in S; then reconsider q = x as Point of CC; {} in {{}} by TARSKI:def 1; then reconsider r = {[{},{}]} as Relation of {{}} by RELSET_1:8; set R = RelStr(#{{}},r#); A19: 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_1:def 9; end; A20: R is transitive proof let x,y,z be Element of R; thus thesis by A19; end; R is directed proof let x,y be Element of R; take x; thus thesis by A19; end; then reconsider R as transitive directed non empty RelStr by A20; set N = R --> q; A21: the_value_of N = q by Th22; the carrier of CC = the carrier of T by Def27; then reconsider M = N as constant strict net of T by Lm6,Lm7; the_value_of the mapping of M = q by A21,Def10; then A22: the_value_of M = q by Def10; set V = the_universe_of the carrier of T; A23: the RelStr of N = the RelStr of R by Def7; {} in V by CLASSES2:62; then the carrier of R in V by CLASSES2:3; then M in NetUniv T by A23,Def14; then A24: [M,q] in C by A22,Def23; the mapping of N = (the carrier of N) --> q by Def7; then rng the mapping of N = {q} by FUNCOP_1:14; then A25: rng the mapping of N c= S by A18,ZFMISC_1:37; q in Lim N by A21,Th42; hence x in F by A24,A25; end; then Cl S c= F by A17,TOPS_1:31; 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 Def27; A2: for N being net of T holds N is net of CC by Def27; A3: 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 A4: N = n; let X be subnet of N; consider f being map of X, N such that A5: the mapping of X = (the mapping of N)*f & 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 Def12; reconsider x = X as net of CC by Def27; reconsider f as map of x, n by A4; the mapping of x = (the mapping of n)*f by A4,A5; hence X is subnet of n by A4,A5,Def12; 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; consider f being map of X, n such that A8: the mapping of X = (the mapping of n)*f & 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 Def12; reconsider x = X as net of T by Def27; reconsider f as map of x, N by A7; the mapping of x = (the mapping of N)*f by A7,A8; hence X is subnet of N by A7,A8,Def12; end; hereby assume A9: CCC = C; thus C is topological proof thus C is (CONSTANTS) proof let N be constant net of T; reconsider M = N as net of CC by Def27; the mapping of N is constant; then the mapping of M is constant; then reconsider M as constant net of CC by Def6; A10: the_value_of M = the_value_of the mapping of M by Def10 .= the_value_of the mapping of N .= the_value_of N by Def10; assume N in NetUniv T; then M in NetUniv CC by A1,Lm8; hence [N,the_value_of N] in C by A9,A10,Def23; end; thus C is (SUBNETS) proof let N be net of T, Y be subnet of N; reconsider M = N as net of CC by Def27; reconsider X = Y as subnet of M by A3; assume Y in NetUniv T; then A11: X in NetUniv CC by A1,Lm8; let p be Element of T; reconsider q = p as Element of CC by Def27; assume [N,p] in C; then [M,q] in CCC by A9; hence [Y,p] in C by A9,A11,Def24; end; thus C is (DIVERGENCE) proof let X be net of T, p be Element of T; reconsider x = X as net of CC by Def27; reconsider q = p as Element of CC by Def27; assume X in NetUniv T; then A12: x in NetUniv CC by A1,Lm8; assume not [X,p] in C; then consider y being subnet of x such that A13: y in NetUniv CC and A14: not ex z being subnet of y st [z,q] in CCC by A9,A12,Def25; reconsider Y = y as subnet of X by A6; take Y; thus Y in NetUniv T by A1,A13,Lm8; let Z be subnet of Y; reconsider z = Z as subnet of y by A3; not [z,q] in CCC by A14; hence not [Z,p] in C by A9; end; thus C is (ITERATED_LIMITS) proof let X be net of T, p be Element of T; reconsider x = X as net of CC by Def27; reconsider q = p as Element of CC by Def27; 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 Def15; hence i is net of CC by A2; 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 = (the mapping of X).j by WAYBEL_0:def 8 .= (the mapping of x).i .= x .i by WAYBEL_0:def 8; hence [I.i,x .i] in CCC by A9,A16; end; then A17: [Iterated I,q] in CCC by A9,A15,Def26; A18: the RelStr of Iterated I = [:X, product J:] by Def16 .= the RelStr of Iterated J by Def16; then A19: the carrier of Iterated I = the carrier of Iterated J; A20: the InternalRel of Iterated I = the InternalRel of Iterated J by A18; dom the mapping of Iterated I = the carrier of Iterated I by FUNCT_2:def 1; then A21: dom the mapping of Iterated I = dom the mapping of Iterated J by A18,FUNCT_2:def 1; now let j be set; A22: the carrier of Iterated I = [:the carrier of x, product Carrier I:] by Th35; A23: the carrier of Iterated J = [:the carrier of X, product Carrier J:] by Th35; assume j in dom the mapping of Iterated I; then reconsider jj = j as Element of Iterated I; consider j1 being Element of x, j2 being Element of product Carrier I such that A24: jj = [j1,j2] by A22,DOMAIN_1:9; reconsider j2 as Element of product I by YELLOW_1:def 4; reconsider i1 = j1 as Element of X; set i2 = j2; reconsider i = [i1,i2] as Element of Iterated J by A23,ZFMISC_1:106; thus (the mapping of Iterated I).j = (Iterated I).jj by WAYBEL_0:def 8 .= (the mapping of I.j1).(j2.j1) by A24,Th36 .= (the mapping of J.i1).(i2.i1) .= (Iterated J).i by Th36 .= (the mapping of Iterated J).j by A24,WAYBEL_0:def 8; end; then A25: the mapping of Iterated I = the mapping of Iterated J by A21, FUNCT_1:9; Iterated I = NetStr(#the carrier of Iterated I, the InternalRel of Iterated I, the mapping of Iterated I#) .= NetStr(#the carrier of Iterated J, the InternalRel of Iterated J, the mapping of Iterated J#) by A19,A20, A25 .= Iterated J; hence [Iterated J,p] in C by A9,A17; end; end; end; assume A26: C is (CONSTANTS) (SUBNETS) (DIVERGENCE) (ITERATED_LIMITS); then reconsider C' = C as topological Convergence-Class of T by Def28; A27: Convergence ConvergenceSpace C c= C proof let x,y; A28: Convergence CC c= [:NetUniv CC,the carrier of CC:] by Def21; assume A29: [x,y] in Convergence CC; then consider M being Element of NetUniv CC, p being Element of CC such that A30: [x,y] = [M,p] by A28,DOMAIN_1:9; A31: M in NetUniv CC; ex N being strict net of CC st N = M & the carrier of N in the_universe_of the carrier of CC by Def14; then reconsider M as net of CC; reconsider N = M as net of T by Def27; reconsider q = p as Point of T by Def27; A32: N in NetUniv T by A1,A31,Lm8; assume not [x,y] in C; 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,A30,A32,Def25; reconsider YY = the RelStr of Y as transitive directed non empty RelStr by Lm1,Lm2; set X = YY --> q; A35: the RelStr of X = YY by Def7; reconsider X as constant non empty strict net of T; A36: ex N0 being strict net of T st N0 = Y & the carrier of N0 in the_universe_of the carrier of T by A33,Def14; the RelStr of X = the RelStr of Y by Def7; then A37: X in NetUniv T by A36,Def14; reconsider X' = X as net of CC by Def27; the mapping of X is constant; then the mapping of X' is constant; then reconsider X' as constant net of CC by Def6; the_value_of X = q by Th22; then A38: [X,q] in C by A26,A37,Def23; A39: p in Lim M by A29,A30,Def22; reconsider Y' = Y as subnet of M by A3; defpred P[set,set] 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 }; A40: for x being set st x in the carrier of X ex j being set st P[x, j] proof let x be set; assume x in the carrier of X; then x in the carrier of Y by Th13; then reconsider i' = x as Element of Y'; Lim M c= Lim Y' by Th41; then consider S being Subset of CC such that A41: S = { Y'.c where c is Element of Y' : i' <= c } and A42: p in Cl S by A39,Th43; consider Go being net of ConvergenceSpace C' such that A43: [Go,p] in C' and A44: rng the mapping of Go c= S and p in Lim Go by A42,Th52; reconsider Ji = Go as net of T by Def27; reconsider i = i' as Element of Y; take Ji,i,Ji; thus x = i & Ji = Ji & [Ji,p] in C by A43; let e be set; assume e in rng the mapping of Ji; then e in S by A44; then consider c' being Element of Y' such that A45: e = Y'.c' and A46: i' <= c' by A41; reconsider cc = c' as Element of Y; e = (the mapping of Y').c' by A45,WAYBEL_0:def 8 .= (the mapping of Y).cc .= Y.cc by WAYBEL_0:def 8; hence e in { Y.c where c is Element of Y : i <= c } by A46; end; consider J being ManySortedSet of the carrier of X such that A47: for x being set st x in the carrier of X holds P[x, J.x] from MSSEx(A40); A48: now let y be set; assume y in rng J; then consider x being set such that A49: x in dom J and A50: y = J.x by FUNCT_1:def 5; x in the carrier of X by A49,PBOOLE:def 3; 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 A47; hence y is non empty 1-sorted by A50; end; A51: 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 A47; hence J.x is net of T; end; now let x be set; assume x in dom J; then x in the carrier of X by PBOOLE:def 3; 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 A47; hence J.x is 1-sorted; end; then J is 1-sorted-yielding by PRALG_1:def 11; then reconsider J as yielding_non-empty_carriers net_set of the carrier of X,T by A48,A51,Def4,Th33; 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 A47; hence [J.i,X.i] in C by Th14; end; then A52: [Iterated J,q] in C by A26,A38,Def26; A53: the RelStr of Iterated J = [:X, product J:] by Def16; then A54: the carrier of Iterated J = [:the carrier of X, the carrier of product J:] by YELLOW_3:def 2; Iterated J is subnet of Y proof 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 A55: for i being Element of Y holds B.i = F(i) from LambdaDMS; now assume {} in rng B; then consider i be set such that A56: i in dom B and A57: B.i = {} by FUNCT_1:def 5; i is Element of Y by A56,PBOOLE:def 3; then reconsider i as Element of Y; consider j being Element of Y such that A58: i <= j and i <= j by Def5; j in { c where c is Element of Y : i <= c } by A58; hence contradiction by A55,A57; end; then reconsider B as non-empty ManySortedSet of the carrier of Y by RELAT_1:def 9; reconsider B' = B as non-empty ManySortedSet of the carrier of X by A35; deffunc F(Element of X) = the carrier of J.$1; consider M being ManySortedSet of the carrier of X such that A59: for x being Element of X holds M.x = F(x) from LambdaDMS; defpred P[set,set,set] 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; A60: for i be set st i in the carrier of X holds for x be set st x in M.i ex y be set st y in B'.i & P[y,x,i] proof let i be set such that A61: i in the carrier of X; let x be set such that A62: x in M.i; consider e being Element of Y, Ji being net of T such that A63: i = e and A64: Ji = J.i and [Ji,p] in C and A65: rng the mapping of Ji c= { Y.c where c is Element of Y : e <= c } by A47,A61; reconsider i' = i as Element of X by A61; defpred P[set,set] means (the mapping of Ji).$1 = (the mapping of Y).$2; A66: for ji being Element of Ji ex u being Element of B'.i' 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 5; then (the mapping of Ji).ji in { Y.c where c is Element of Y : e <= c } by A65; then consider c being Element of Y such that A67: (the mapping of Ji).ji = Y.c and A68: e <= c; c in { cc where cc is Element of Y : e <= cc } by A68; then reconsider c as Element of B'.i' by A55,A63; take c; thus (the mapping of Ji).ji = (the mapping of Y).c by A67,WAYBEL_0:def 8; end; consider f being Function of the carrier of Ji, B'.i' such that A69: for ji being Element of Ji holds P[ji, f.ji] from FuncExD(A66); reconsider f as Function of the carrier of Ji, B.i; reconsider ji = x as Element of Ji by A59,A61,A62,A64; take f.x; f.ji in B.i; hence f.x in B'.i; take f,i'; thus f.x = f.x & i' = i; thus (the mapping of J.i').x = (the mapping of Ji).ji by A64 .= (the mapping of Y).(f.x) by A69; end; consider u be ManySortedFunction of M, B' such that A70: for i be set st i in the carrier of X holds ex f be Function of M.i, B'.i st f = u.i & for x be set st x in M.i holds P[f.x,x,i] from MSFExFunc(A60); 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, B'.i such that A72: f = u.i and A73: for x be set st x in M.i holds P[f.x,x,i] by A70; M.i = the carrier of J.i by A59; then P[f.j,j,i] by A73; hence (the mapping of J.i).j = (the mapping of Y).(u.i.j) by A72; end; deffunc F(Element of X, Element of product J) = u.$1 .($2.$1); A74: 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 k = x as Element of Y by A35; A75: u.k is Function of M.k, B.k by MSUALG_1:def 2; defpred P[Element of Y] means k <= $1; set ZZ = { c where c is Element of Y : P[c] }; A76: ZZ is Subset of Y from SubsetD; A77: B.k = ZZ by A55; reconsider x' = x as Element of X'; y in the carrier of product J; then A78: y in product Carrier J by YELLOW_1:def 4; x' in the carrier of X'; then x' in dom Carrier J by PBOOLE:def 3; then y.x' in (Carrier J).x' by A78,CARD_3:18; then y.x' in the carrier of J.x by Th9; then y.x in M.k by A59; then u.k.(y.x) in B.k by A75,FUNCT_2:7; hence u.x .(y.x) in the carrier of Y by A76,A77; end; consider f being Function of [:the carrier of X, the carrier of product J:], the carrier of Y such that A79: for x being Element of X, y being Element of product J holds f. [x,y] = F(x,y) from Kappa2D(A74); reconsider f as map of Iterated J,Y by A54; take f; set h = the mapping of Iterated J, g = the mapping of Y'; A80: for x holds x in dom h iff x in dom f & f.x in dom g proof let x; hereby assume x in dom h; then x in the carrier of Iterated J; then x in [:the carrier of X',product Carrier J:] by Th35; then A81: x in [:the carrier of X',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 A81,FUNCT_2:7; hence f.x in dom g by FUNCT_2:def 1; end; assume x in dom f & f.x in dom g; then x in [:the carrier of X',the carrier of product J:] by FUNCT_2:def 1; then x in [:the carrier of X',product Carrier J:] by YELLOW_1:def 4; then x in the carrier of Iterated J by Th35; hence x in dom h by FUNCT_2:def 1; end; for x st x in dom h holds h.x = g.(f.x) proof let x; assume x in dom h; then x in the carrier of Iterated J; then x in [:the carrier of X',product Carrier J:] by Th35; then x in [:the carrier of X',the carrier of product J:] by YELLOW_1:def 4; then consider x1 being Element of X', x2 being Element of product J such that A82: x = [x1,x2] by DOMAIN_1:9; reconsider x' = x1 as Element of X; A83: dom Carrier J = the carrier of X' by PBOOLE:def 3; x2 in the carrier of product J; then A84: x2 in product Carrier J by YELLOW_1:def 4; the carrier of J.x' = (Carrier J).x1 by Th9; then x2.x1 in the carrier of J.x' by A83,A84,CARD_3:18; then reconsider j = x2.x1 as Element of M.x' by A59; thus h.x = h.(x1,x2) by A82,BINOP_1:def 1 .= (the mapping of J.x').(x2.x1) by Def16 .= g.(u.x'.j) by A71 .= g.(f.x) by A79,A82; end; hence the mapping of Iterated J = (the mapping of Y)*f by A80,FUNCT_1:20 ; let m be Element of Y; consider F being Element of product J; [m,F] in the carrier of Iterated J by A35,A54,ZFMISC_1:106; then reconsider n = [m,F] as Element of Iterated J; reconsider F as Element of product J; reconsider m' = m as Element of X by A35; take n; let p be Element of Iterated J; consider k' being Element of X, G being Element of product J such that A85: p = [k',G] by A54,DOMAIN_1:9; reconsider k = k' as Element of Y by A35; reconsider k'' = k' as Element of X'; A86: f.p = u.k.(G.k) by A79,A85; A87: u.k is Function of M.k, B.k by MSUALG_1:def 2; then A88: dom(u.k) = M.k by FUNCT_2:def 1 .= the carrier of J.k' by A59 .= (Carrier J).k'' by Th9; A89: dom Carrier J = the carrier of X' by PBOOLE:def 3; G in the carrier of product J; then G in product Carrier J by YELLOW_1:def 4; then G.k'' in dom(u.k) by A88,A89,CARD_3:18; then A90: f.p in rng(u.k) by A86,FUNCT_1:def 5; rng(u.k) c= B.k by A87,RELSET_1:12; then f.p in B.k by A90; then f.p in { c where c is Element of Y : k <= c } by A55; then consider c being Element of Y such that A91: c = f.p and A92: k <= c; reconsider G as Element of product J; reconsider k' = k as Element of X; assume n <= p; then [m',F] <= [k',G] by A53,A85,Lm3; then m' <= k' by YELLOW_3:11; then m <= k by A35,Lm3; hence m <= f.p by A91,A92,YELLOW_0:def 2; end; hence contradiction by A34,A52; end; C c= Convergence ConvergenceSpace C by Th49; hence thesis by A27,XBOOLE_0:def 10; end;

Back to top