:: YELLOW19 semantic presentation begin theorem Th1: :: YELLOW19:1 for X being non empty set for F being proper Filter of (BoolePoset X) for A being set st A in F holds not A is empty proof let X be non empty set ; ::_thesis: for F being proper Filter of (BoolePoset X) for A being set st A in F holds not A is empty Bottom (BoolePoset X) = {} by YELLOW_1:18; hence for F being proper Filter of (BoolePoset X) for A being set st A in F holds not A is empty by WAYBEL_7:4; ::_thesis: verum end; definition let T be non empty TopSpace; let x be Point of T; func NeighborhoodSystem x -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 1 { A where A is a_neighborhood of x : verum } ; coherence { A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T)) proof set Y = { A where A is a_neighborhood of x : verum } ; set X = the carrier of T; { A where A is a_neighborhood of x : verum } c= bool the carrier of T proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { A where A is a_neighborhood of x : verum } or y in bool the carrier of T ) assume y in { A where A is a_neighborhood of x : verum } ; ::_thesis: y in bool the carrier of T then ex A being a_neighborhood of x st y = A ; hence y in bool the carrier of T ; ::_thesis: verum end; hence { A where A is a_neighborhood of x : verum } is Subset of (BoolePoset ([#] T)) by WAYBEL_7:2; ::_thesis: verum end; end; :: deftheorem defines NeighborhoodSystem YELLOW19:def_1_:_ for T being non empty TopSpace for x being Point of T holds NeighborhoodSystem x = { A where A is a_neighborhood of x : verum } ; theorem Th2: :: YELLOW19:2 for T being non empty TopSpace for x being Point of T for A being set holds ( A in NeighborhoodSystem x iff A is a_neighborhood of x ) proof let T be non empty TopSpace; ::_thesis: for x being Point of T for A being set holds ( A in NeighborhoodSystem x iff A is a_neighborhood of x ) let x be Point of T; ::_thesis: for A being set holds ( A in NeighborhoodSystem x iff A is a_neighborhood of x ) let B be set ; ::_thesis: ( B in NeighborhoodSystem x iff B is a_neighborhood of x ) ( B in NeighborhoodSystem x iff ex A being a_neighborhood of x st B = A ) ; hence ( B in NeighborhoodSystem x iff B is a_neighborhood of x ) ; ::_thesis: verum end; registration let T be non empty TopSpace; let x be Point of T; cluster NeighborhoodSystem x -> non empty proper filtered upper ; coherence ( not NeighborhoodSystem x is empty & NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered ) proof set Y = NeighborhoodSystem x; set X = the carrier of T; set L = BoolePoset ([#] T); set A0 = the a_neighborhood of x; the a_neighborhood of x in NeighborhoodSystem x ; hence not NeighborhoodSystem x is empty ; ::_thesis: ( NeighborhoodSystem x is proper & NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered ) {} c= the carrier of T by XBOOLE_1:2; then A1: {} in bool the carrier of T ; {} is not a_neighborhood of x by CONNSP_2:4; then A2: not {} in NeighborhoodSystem x by Th2; the carrier of (BoolePoset the carrier of T) = bool the carrier of T by WAYBEL_7:2; hence NeighborhoodSystem x is proper by A1, A2, SUBSET_1:def_6; ::_thesis: ( NeighborhoodSystem x is upper & NeighborhoodSystem x is filtered ) thus NeighborhoodSystem x is upper ::_thesis: NeighborhoodSystem x is filtered proof let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in NeighborhoodSystem x or not a <= b or b in NeighborhoodSystem x ) reconsider B = b as Subset of T by WAYBEL_7:2; assume a in NeighborhoodSystem x ; ::_thesis: ( not a <= b or b in NeighborhoodSystem x ) then reconsider A = a as a_neighborhood of x by Th2; assume a <= b ; ::_thesis: b in NeighborhoodSystem x then A c= B by YELLOW_1:2; then A3: Int A c= Int B by TOPS_1:19; x in Int A by CONNSP_2:def_1; then b is a_neighborhood of x by A3, CONNSP_2:def_1; hence b in NeighborhoodSystem x ; ::_thesis: verum end; let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_2 ::_thesis: ( not a in NeighborhoodSystem x or not b in NeighborhoodSystem x or ex b1 being Element of the carrier of (BoolePoset ([#] T)) st ( b1 in NeighborhoodSystem x & b1 <= a & b1 <= b ) ) assume that A4: a in NeighborhoodSystem x and A5: b in NeighborhoodSystem x ; ::_thesis: ex b1 being Element of the carrier of (BoolePoset ([#] T)) st ( b1 in NeighborhoodSystem x & b1 <= a & b1 <= b ) reconsider A = a, B = b as a_neighborhood of x by A4, A5, Th2; A6: A /\ B is a_neighborhood of x by CONNSP_2:2; then A /\ B in NeighborhoodSystem x ; then reconsider z = A /\ B as Element of (BoolePoset ([#] T)) ; take z ; ::_thesis: ( z in NeighborhoodSystem x & z <= a & z <= b ) A7: z c= B by XBOOLE_1:17; z c= A by XBOOLE_1:17; hence ( z in NeighborhoodSystem x & z <= a & z <= b ) by A6, A7, YELLOW_1:2; ::_thesis: verum end; end; theorem Th3: :: YELLOW19:3 for T being non empty TopSpace for x being Point of T for F being upper Subset of (BoolePoset ([#] T)) holds ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F ) proof let T be non empty TopSpace; ::_thesis: for x being Point of T for F being upper Subset of (BoolePoset ([#] T)) holds ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F ) let x be Point of T; ::_thesis: for F being upper Subset of (BoolePoset ([#] T)) holds ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F ) let F be upper Subset of (BoolePoset ([#] T)); ::_thesis: ( x is_a_convergence_point_of F,T iff NeighborhoodSystem x c= F ) hereby ::_thesis: ( NeighborhoodSystem x c= F implies x is_a_convergence_point_of F,T ) assume A1: x is_a_convergence_point_of F,T ; ::_thesis: NeighborhoodSystem x c= F thus NeighborhoodSystem x c= F ::_thesis: verum proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in NeighborhoodSystem x or y in F ) assume y in NeighborhoodSystem x ; ::_thesis: y in F then reconsider y = y as a_neighborhood of x by Th2; x in Int y by CONNSP_2:def_1; then A2: Int y in F by A1, WAYBEL_7:def_5; Int y c= y by TOPS_1:16; hence y in F by A2, WAYBEL_7:7; ::_thesis: verum end; end; assume A3: NeighborhoodSystem x c= F ; ::_thesis: x is_a_convergence_point_of F,T let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in F ) assume that A4: A is open and A5: x in A ; ::_thesis: A in F A is a_neighborhood of x by A4, A5, CONNSP_2:3; then A in NeighborhoodSystem x ; hence A in F by A3; ::_thesis: verum end; theorem :: YELLOW19:4 for T being non empty TopSpace for x being Point of T holds x is_a_convergence_point_of NeighborhoodSystem x,T by Th3; theorem :: YELLOW19:5 for T being non empty TopSpace for A being Subset of T holds ( A is open iff for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is open iff for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ) let A be Subset of T; ::_thesis: ( A is open iff for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ) thus ( A is open implies for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ) by WAYBEL_7:def_5; ::_thesis: ( ( for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ) implies A is open ) assume A1: for x being Point of T st x in A holds for F being Filter of (BoolePoset ([#] T)) st x is_a_convergence_point_of F,T holds A in F ; ::_thesis: A is open set x = the Element of A \ (Int A); A2: Int A c= A by TOPS_1:16; assume not A is open ; ::_thesis: contradiction then not A c= Int A by A2, XBOOLE_0:def_10; then A3: A \ (Int A) <> {} by XBOOLE_1:37; then the Element of A \ (Int A) in A \ (Int A) ; then reconsider x = the Element of A \ (Int A) as Point of T ; A4: x in A by A3, XBOOLE_0:def_5; x is_a_convergence_point_of NeighborhoodSystem x,T by Th3; then A in NeighborhoodSystem x by A1, A4; then A is a_neighborhood of x by Th2; then x in Int A by CONNSP_2:def_1; hence contradiction by A3, XBOOLE_0:def_5; ::_thesis: verum end; definition let S be non empty 1-sorted ; let N be non empty NetStr over S; mode Subset of S,N -> Subset of S means :Def2: :: YELLOW19:def 2 ex i being Element of N st it = rng the mapping of (N | i); existence ex b1 being Subset of S ex i being Element of N st b1 = rng the mapping of (N | i) proof set i = the Element of N; reconsider A = rng the mapping of (N | the Element of N) as Subset of S ; take A ; ::_thesis: ex i being Element of N st A = rng the mapping of (N | i) take the Element of N ; ::_thesis: A = rng the mapping of (N | the Element of N) thus A = rng the mapping of (N | the Element of N) ; ::_thesis: verum end; end; :: deftheorem Def2 defines Subset YELLOW19:def_2_:_ for S being non empty 1-sorted for N being non empty NetStr over S for b3 being Subset of S holds ( b3 is Subset of S,N iff ex i being Element of N st b3 = rng the mapping of (N | i) ); theorem :: YELLOW19:6 for S being non empty 1-sorted for N being non empty NetStr over S for i being Element of N holds rng the mapping of (N | i) is Subset of S,N by Def2; registration let S be non empty 1-sorted ; let N be non empty reflexive NetStr over S; cluster -> non empty for Subset of S,N; coherence for b1 being Subset of S,N holds not b1 is empty proof let A be Subset of S,N; ::_thesis: not A is empty ex i being Element of N st A = rng the mapping of (N | i) by Def2; hence not A is empty ; ::_thesis: verum end; end; theorem Th7: :: YELLOW19:7 for S being non empty 1-sorted for N being net of S for i being Element of N for x being set holds ( x in rng the mapping of (N | i) iff ex j being Element of N st ( i <= j & x = N . j ) ) proof let S be non empty 1-sorted ; ::_thesis: for N being net of S for i being Element of N for x being set holds ( x in rng the mapping of (N | i) iff ex j being Element of N st ( i <= j & x = N . j ) ) let N be net of S; ::_thesis: for i being Element of N for x being set holds ( x in rng the mapping of (N | i) iff ex j being Element of N st ( i <= j & x = N . j ) ) let i be Element of N; ::_thesis: for x being set holds ( x in rng the mapping of (N | i) iff ex j being Element of N st ( i <= j & x = N . j ) ) let x be set ; ::_thesis: ( x in rng the mapping of (N | i) iff ex j being Element of N st ( i <= j & x = N . j ) ) A1: dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1; hereby ::_thesis: ( ex j being Element of N st ( i <= j & x = N . j ) implies x in rng the mapping of (N | i) ) assume x in rng the mapping of (N | i) ; ::_thesis: ex j being Element of N st ( i <= j & x = N . j ) then consider y being set such that A2: y in the carrier of (N | i) and A3: x = the mapping of (N | i) . y by A1, FUNCT_1:def_3; reconsider y = y as Element of (N | i) by A2; consider j being Element of N such that A4: j = y and A5: i <= j by WAYBEL_9:def_7; take j = j; ::_thesis: ( i <= j & x = N . j ) thus i <= j by A5; ::_thesis: x = N . j thus x = (N | i) . y by A3 .= N . j by A4, WAYBEL_9:16 ; ::_thesis: verum end; given j being Element of N such that A6: i <= j and A7: x = N . j ; ::_thesis: x in rng the mapping of (N | i) reconsider k = j as Element of (N | i) by A6, WAYBEL_9:def_7; A8: x = (N | i) . k by A7, WAYBEL_9:16 .= the mapping of (N | i) . j ; j in the carrier of (N | i) by A6, WAYBEL_9:def_7; hence x in rng the mapping of (N | i) by A1, A8, FUNCT_1:def_3; ::_thesis: verum end; theorem Th8: :: YELLOW19:8 for S being non empty 1-sorted for N being net of S for A being Subset of S,N holds N is_eventually_in A proof let S be non empty 1-sorted ; ::_thesis: for N being net of S for A being Subset of S,N holds N is_eventually_in A let N be net of S; ::_thesis: for A being Subset of S,N holds N is_eventually_in A let A be Subset of S,N; ::_thesis: N is_eventually_in A consider i being Element of N such that A1: A = rng the mapping of (N | i) by Def2; take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not i <= b1 or N . b1 in A ) let j be Element of N; ::_thesis: ( not i <= j or N . j in A ) assume i <= j ; ::_thesis: N . j in A then reconsider j9 = j as Element of (N | i) by WAYBEL_9:def_7; N . j = (N | i) . j9 by WAYBEL_9:16 .= the mapping of (N | i) . j9 ; hence N . j in A by A1, FUNCT_2:4; ::_thesis: verum end; theorem :: YELLOW19:9 for S being non empty 1-sorted for N being net of S for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds ex B being Subset of S,N st B c= meet F proof let S be non empty 1-sorted ; ::_thesis: for N being net of S for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds ex B being Subset of S,N st B c= meet F let N be net of S; ::_thesis: for F being non empty finite set st ( for A being Element of F holds A is Subset of S,N ) holds ex B being Subset of S,N st B c= meet F defpred S1[ set , set ] means ex i being Element of N st ( \$2 = i & \$1 = rng the mapping of (N | i) ); let F be non empty finite set ; ::_thesis: ( ( for A being Element of F holds A is Subset of S,N ) implies ex B being Subset of S,N st B c= meet F ) assume A1: for A being Element of F holds A is Subset of S,N ; ::_thesis: ex B being Subset of S,N st B c= meet F A2: now__::_thesis:_for_x_being_set_st_x_in_F_holds_ ex_y_being_set_st_ (_y_in_the_carrier_of_N_&_S1[x,y]_) let x be set ; ::_thesis: ( x in F implies ex y being set st ( y in the carrier of N & S1[x,y] ) ) assume x in F ; ::_thesis: ex y being set st ( y in the carrier of N & S1[x,y] ) then reconsider A = x as Subset of S,N by A1; consider i being Element of N such that A3: A = rng the mapping of (N | i) by Def2; reconsider y = i as set ; take y = y; ::_thesis: ( y in the carrier of N & S1[x,y] ) thus y in the carrier of N ; ::_thesis: S1[x,y] thus S1[x,y] by A3; ::_thesis: verum end; consider f being Function such that A4: ( dom f = F & rng f c= the carrier of N ) and A5: for x being set st x in F holds S1[x,f . x] from FUNCT_1:sch_5(A2); reconsider B = rng f as finite Subset of N by A4, FINSET_1:8; [#] N is directed by WAYBEL_0:def_6; then consider j being Element of N such that j in [#] N and A6: j is_>=_than B by WAYBEL_0:1; reconsider C = rng the mapping of (N | j) as Subset of S,N by Def2; take C ; ::_thesis: C c= meet F let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C or x in meet F ) A7: the carrier of (N | j) = { k where k is Element of N : j <= k } by WAYBEL_9:12; assume x in C ; ::_thesis: x in meet F then consider y being set such that A8: y in dom the mapping of (N | j) and A9: x = the mapping of (N | j) . y by FUNCT_1:def_3; A10: y in the carrier of (N | j) by A8; reconsider y = y as Element of (N | j) by A8; consider k being Element of N such that A11: y = k and A12: j <= k by A10, A7; now__::_thesis:_for_X_being_set_st_X_in_F_holds_ x_in_X let X be set ; ::_thesis: ( X in F implies x in X ) assume A13: X in F ; ::_thesis: x in X then consider i being Element of N such that A14: f . X = i and A15: X = rng the mapping of (N | i) by A5; i in B by A4, A13, A14, FUNCT_1:def_3; then i <= j by A6, LATTICE3:def_9; then i <= k by A12, ORDERS_2:3; then y in { l where l is Element of N : i <= l } by A11; then reconsider z = y as Element of (N | i) by WAYBEL_9:12; x = (N | j) . y by A9 .= N . k by A11, WAYBEL_9:16 .= (N | i) . z by A11, WAYBEL_9:16 .= the mapping of (N | i) . z ; hence x in X by A15, FUNCT_2:4; ::_thesis: verum end; hence x in meet F by SETFAM_1:def_1; ::_thesis: verum end; definition let T be non empty 1-sorted ; let N be non empty NetStr over T; func a_filter N -> Subset of (BoolePoset ([#] T)) equals :: YELLOW19:def 3 { A where A is Subset of T : N is_eventually_in A } ; coherence { A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T)) proof set X = the carrier of T; set F = { A where A is Subset of T : N is_eventually_in A } ; A1: { A where A is Subset of T : N is_eventually_in A } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { A where A is Subset of T : N is_eventually_in A } or x in bool the carrier of T ) assume x in { A where A is Subset of T : N is_eventually_in A } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T st ( x = A & N is_eventually_in A ) ; hence x in bool the carrier of T ; ::_thesis: verum end; BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4 .= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ; hence { A where A is Subset of T : N is_eventually_in A } is Subset of (BoolePoset ([#] T)) by A1; ::_thesis: verum end; end; :: deftheorem defines a_filter YELLOW19:def_3_:_ for T being non empty 1-sorted for N being non empty NetStr over T holds a_filter N = { A where A is Subset of T : N is_eventually_in A } ; theorem Th10: :: YELLOW19:10 for T being non empty 1-sorted for N being non empty NetStr over T for A being set holds ( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) ) proof let T be non empty 1-sorted ; ::_thesis: for N being non empty NetStr over T for A being set holds ( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) ) let N be non empty NetStr over T; ::_thesis: for A being set holds ( A in a_filter N iff ( N is_eventually_in A & A is Subset of T ) ) let B be set ; ::_thesis: ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) ) ( B in a_filter N iff ex A being Subset of T st ( B = A & N is_eventually_in A ) ) ; hence ( B in a_filter N iff ( N is_eventually_in B & B is Subset of T ) ) ; ::_thesis: verum end; registration let T be non empty 1-sorted ; let N be non empty NetStr over T; cluster a_filter N -> non empty upper ; coherence ( not a_filter N is empty & a_filter N is upper ) proof set X = the carrier of T; set L = BoolePoset ([#] T); set F = a_filter N; N is_eventually_in [#] T proof set i = the Element of N; take the Element of N ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of N holds ( not the Element of N <= b1 or N . b1 in [#] T ) thus for b1 being Element of the carrier of N holds ( not the Element of N <= b1 or N . b1 in [#] T ) ; ::_thesis: verum end; hence not a_filter N is empty by Th10; ::_thesis: a_filter N is upper let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_20 ::_thesis: ( not a in a_filter N or not a <= b or b in a_filter N ) assume a in a_filter N ; ::_thesis: ( not a <= b or b in a_filter N ) then A1: N is_eventually_in a by Th10; assume a <= b ; ::_thesis: b in a_filter N then a c= b by YELLOW_1:2; then A2: N is_eventually_in b by A1, WAYBEL_0:8; BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4 .= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ; hence b in a_filter N by A2; ::_thesis: verum end; end; registration let T be non empty 1-sorted ; let N be net of T; cluster a_filter N -> proper filtered ; coherence ( a_filter N is proper & a_filter N is filtered ) proof set X = the carrier of T; set L = BoolePoset ([#] T); set F = a_filter N; A1: BoolePoset the carrier of T = InclPoset (bool the carrier of T) by YELLOW_1:4 .= RelStr(# (bool the carrier of T),(RelIncl (bool the carrier of T)) #) by YELLOW_1:def_1 ; now__::_thesis:_(_{}_c=_the_carrier_of_T_&_not_{}_in_a_filter_N_) thus {} c= the carrier of T by XBOOLE_1:2; ::_thesis: not {} in a_filter N assume {} in a_filter N ; ::_thesis: contradiction then N is_eventually_in {} by Th10; then consider i being Element of N such that A2: for j being Element of N st i <= j holds N . j in {} by WAYBEL_0:def_11; ex j being Element of N st ( i <= j & i <= j ) by YELLOW_6:def_3; hence contradiction by A2; ::_thesis: verum end; then a_filter N <> bool the carrier of T ; hence a_filter N is proper by A1, SUBSET_1:def_6; ::_thesis: a_filter N is filtered let a, b be Element of (BoolePoset ([#] T)); :: according to WAYBEL_0:def_2 ::_thesis: ( not a in a_filter N or not b in a_filter N or ex b1 being Element of the carrier of (BoolePoset ([#] T)) st ( b1 in a_filter N & b1 <= a & b1 <= b ) ) assume that A3: a in a_filter N and A4: b in a_filter N ; ::_thesis: ex b1 being Element of the carrier of (BoolePoset ([#] T)) st ( b1 in a_filter N & b1 <= a & b1 <= b ) N is_eventually_in a by A3, Th10; then consider i1 being Element of N such that A5: for j being Element of N st i1 <= j holds N . j in a by WAYBEL_0:def_11; N is_eventually_in b by A4, Th10; then consider i2 being Element of N such that A6: for j being Element of N st i2 <= j holds N . j in b by WAYBEL_0:def_11; take z = a "/\" b; ::_thesis: ( z in a_filter N & z <= a & z <= b ) A7: z = a /\ b by YELLOW_1:17; then A8: z c= b by XBOOLE_1:17; consider i being Element of N such that A9: i1 <= i and A10: i2 <= i by YELLOW_6:def_3; now__::_thesis:_for_j_being_Element_of_N_st_i_<=_j_holds_ N_._j_in_a_/\_b let j be Element of N; ::_thesis: ( i <= j implies N . j in a /\ b ) assume A11: i <= j ; ::_thesis: N . j in a /\ b then A12: N . j in b by A6, A10, ORDERS_2:3; N . j in a by A5, A9, A11, ORDERS_2:3; hence N . j in a /\ b by A12, XBOOLE_0:def_4; ::_thesis: verum end; then N is_eventually_in z by A7, WAYBEL_0:def_11; hence z in a_filter N by A1; ::_thesis: ( z <= a & z <= b ) z c= a by A7, XBOOLE_1:17; hence ( z <= a & z <= b ) by A8, YELLOW_1:2; ::_thesis: verum end; end; theorem Th11: :: YELLOW19:11 for T being non empty TopSpace for N being net of T for x being Point of T holds ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T ) proof let T be non empty TopSpace; ::_thesis: for N being net of T for x being Point of T holds ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T ) let N be net of T; ::_thesis: for x being Point of T holds ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T ) set F = a_filter N; let x be Point of T; ::_thesis: ( x is_a_cluster_point_of N iff x is_a_cluster_point_of a_filter N,T ) thus ( x is_a_cluster_point_of N implies x is_a_cluster_point_of a_filter N,T ) ::_thesis: ( x is_a_cluster_point_of a_filter N,T implies x is_a_cluster_point_of N ) proof assume A1: for O being a_neighborhood of x holds N is_often_in O ; :: according to WAYBEL_9:def_9 ::_thesis: x is_a_cluster_point_of a_filter N,T let A be Subset of T; :: according to WAYBEL_7:def_4 ::_thesis: ( not A is open or not x in A or for b1 being set holds ( not b1 in a_filter N or not A misses b1 ) ) assume that A2: A is open and A3: x in A ; ::_thesis: for b1 being set holds ( not b1 in a_filter N or not A misses b1 ) let B be set ; ::_thesis: ( not B in a_filter N or not A misses B ) assume B in a_filter N ; ::_thesis: not A misses B then N is_eventually_in B by Th10; then consider i being Element of N such that A4: for j being Element of N st i <= j holds N . j in B by WAYBEL_0:def_11; A is a_neighborhood of x by A2, A3, CONNSP_2:3; then N is_often_in A by A1; then ex j being Element of N st ( i <= j & N . j in A ) by WAYBEL_0:def_12; then ex a being Point of T st ( a in B & a in A ) by A4; hence not A misses B by XBOOLE_0:3; ::_thesis: verum end; assume A5: for A being Subset of T st A is open & x in A holds for B being set st B in a_filter N holds A meets B ; :: according to WAYBEL_7:def_4 ::_thesis: x is_a_cluster_point_of N let O be a_neighborhood of x; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in O let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st ( i <= b1 & N . b1 in O ) reconsider B = rng the mapping of (N | i) as Subset of T,N by Def2; N is_eventually_in B by Th8; then A6: B in a_filter N ; x in Int O by CONNSP_2:def_1; then Int O meets B by A5, A6; then consider x being set such that A7: x in Int O and A8: x in B by XBOOLE_0:3; consider j being Element of N such that A9: i <= j and A10: x = N . j by A8, Th7; take j ; ::_thesis: ( i <= j & N . j in O ) Int O c= O by TOPS_1:16; hence ( i <= j & N . j in O ) by A7, A9, A10; ::_thesis: verum end; theorem Th12: :: YELLOW19:12 for T being non empty TopSpace for N being net of T for x being Point of T holds ( x in Lim N iff x is_a_convergence_point_of a_filter N,T ) proof let T be non empty TopSpace; ::_thesis: for N being net of T for x being Point of T holds ( x in Lim N iff x is_a_convergence_point_of a_filter N,T ) let N be net of T; ::_thesis: for x being Point of T holds ( x in Lim N iff x is_a_convergence_point_of a_filter N,T ) set F = a_filter N; let x be Point of T; ::_thesis: ( x in Lim N iff x is_a_convergence_point_of a_filter N,T ) thus ( x in Lim N implies x is_a_convergence_point_of a_filter N,T ) ::_thesis: ( x is_a_convergence_point_of a_filter N,T implies x in Lim N ) proof assume A1: x in Lim N ; ::_thesis: x is_a_convergence_point_of a_filter N,T let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in a_filter N ) assume that A2: A is open and A3: x in A ; ::_thesis: A in a_filter N A is a_neighborhood of x by A2, A3, CONNSP_2:3; then N is_eventually_in A by A1, YELLOW_6:def_15; hence A in a_filter N ; ::_thesis: verum end; assume A4: for A being Subset of T st A is open & x in A holds A in a_filter N ; :: according to WAYBEL_7:def_5 ::_thesis: x in Lim N now__::_thesis:_for_O_being_a_neighborhood_of_x_holds_N_is_eventually_in_O let O be a_neighborhood of x; ::_thesis: N is_eventually_in O x in Int O by CONNSP_2:def_1; then Int O in a_filter N by A4; then A5: N is_eventually_in Int O by Th10; Int O c= O by TOPS_1:16; hence N is_eventually_in O by A5, WAYBEL_0:8; ::_thesis: verum end; hence x in Lim N by YELLOW_6:def_15; ::_thesis: verum end; definition let L be non empty 1-sorted ; let O be non empty Subset of L; let F be Filter of (BoolePoset O); func a_net F -> non empty strict NetStr over L means :Def4: :: YELLOW19:def 4 ( the carrier of it = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it holds it . i = i `1 ) ); existence ex b1 being non empty strict NetStr over L st ( the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) ) proof deffunc H1( set ) -> set = \$1 `1 ; set S = { [a,f] where a is Element of L, f is Element of F : a in f } ; Top (BoolePoset O) = O by YELLOW_1:19; then reconsider f = O as Element of F by WAYBEL12:8; reconsider f = f as Subset of L ; consider a being Element of L such that A1: a in f by SUBSET_1:4; reconsider a = a as Element of L ; [a,f] in { [a,f] where a is Element of L, f is Element of F : a in f } by A1; then reconsider S = { [a,f] where a is Element of L, f is Element of F : a in f } as non empty set ; defpred S1[ set , set ] means \$2 `2 c= \$1 `2 ; consider R being Relation of S,S such that A2: for x, y being Element of S holds ( [x,y] in R iff S1[x,y] ) from RELSET_1:sch_2(); A3: for x being set st x in S holds H1(x) in the carrier of L proof let x be set ; ::_thesis: ( x in S implies H1(x) in the carrier of L ) assume x in S ; ::_thesis: H1(x) in the carrier of L then consider a being Element of L, f being Element of F such that A4: x = [a,f] and a in f ; [a,f] `1 = a ; hence H1(x) in the carrier of L by A4; ::_thesis: verum end; consider h being Function of S, the carrier of L such that A5: for x being set st x in S holds h . x = H1(x) from FUNCT_2:sch_2(A3); take N = NetStr(# S,R,h #); ::_thesis: ( the carrier of N = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of N holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) for i, j being Element of N holds ( i <= j iff j `2 c= i `2 ) proof let i, j be Element of N; ::_thesis: ( i <= j iff j `2 c= i `2 ) reconsider x = i, y = j as Element of S ; ( [x,y] in the InternalRel of N iff y `2 c= x `2 ) by A2; hence ( i <= j iff j `2 c= i `2 ) by ORDERS_2:def_5; ::_thesis: verum end; hence ( the carrier of N = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of N holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of N holds N . i = i `1 ) ) by A5; ::_thesis: verum end; uniqueness for b1, b2 being non empty strict NetStr over L st the carrier of b1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b1 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b1 holds b1 . i = i `1 ) & the carrier of b2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b2 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b2 holds b2 . i = i `1 ) holds b1 = b2 proof set S = { [a,f] where a is Element of L, f is Element of F : a in f } ; let it1, it2 be non empty strict NetStr over L; ::_thesis: ( the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it1 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it1 holds it1 . i = i `1 ) & the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of it2 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of it2 holds it2 . i = i `1 ) implies it1 = it2 ) assume that A6: the carrier of it1 = { [a,f] where a is Element of L, f is Element of F : a in f } and A7: for i, j being Element of it1 holds ( i <= j iff j `2 c= i `2 ) and A8: for i being Element of it1 holds it1 . i = i `1 and A9: the carrier of it2 = { [a,f] where a is Element of L, f is Element of F : a in f } and A10: for i, j being Element of it2 holds ( i <= j iff j `2 c= i `2 ) and A11: for i being Element of it2 holds it2 . i = i `1 ; ::_thesis: it1 = it2 A12: for x, y being set holds ( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 ) proof let x, y be set ; ::_thesis: ( [x,y] in the InternalRel of it1 iff [x,y] in the InternalRel of it2 ) hereby ::_thesis: ( [x,y] in the InternalRel of it2 implies [x,y] in the InternalRel of it1 ) assume A13: [x,y] in the InternalRel of it1 ; ::_thesis: [x,y] in the InternalRel of it2 then reconsider i = x, j = y as Element of it1 by ZFMISC_1:87; reconsider i9 = x, j9 = y as Element of it2 by A6, A9, A13, ZFMISC_1:87; i <= j by A13, ORDERS_2:def_5; then j9 `2 c= i9 `2 by A7; then i9 <= j9 by A10; hence [x,y] in the InternalRel of it2 by ORDERS_2:def_5; ::_thesis: verum end; assume A14: [x,y] in the InternalRel of it2 ; ::_thesis: [x,y] in the InternalRel of it1 then reconsider i = x, j = y as Element of it2 by ZFMISC_1:87; reconsider i9 = x, j9 = y as Element of it1 by A6, A9, A14, ZFMISC_1:87; i <= j by A14, ORDERS_2:def_5; then j9 `2 c= i9 `2 by A10; then i9 <= j9 by A7; hence [x,y] in the InternalRel of it1 by ORDERS_2:def_5; ::_thesis: verum end; the mapping of it1 = the mapping of it2 proof reconsider f2 = the mapping of it2 as Function of { [a,f] where a is Element of L, f is Element of F : a in f } , the carrier of L by A9; reconsider f1 = the mapping of it1 as Function of { [a,f] where a is Element of L, f is Element of F : a in f } , the carrier of L by A6; for x being set st x in { [a,f] where a is Element of L, f is Element of F : a in f } holds f1 . x = f2 . x proof let x be set ; ::_thesis: ( x in { [a,f] where a is Element of L, f is Element of F : a in f } implies f1 . x = f2 . x ) assume A15: x in { [a,f] where a is Element of L, f is Element of F : a in f } ; ::_thesis: f1 . x = f2 . x then reconsider x1 = x as Element of it1 by A6; reconsider x2 = x as Element of it2 by A9, A15; reconsider x = x as Element of { [a,f] where a is Element of L, f is Element of F : a in f } by A15; f1 . x = it1 . x1 .= x1 `1 by A8 .= it2 . x2 by A11 ; hence f1 . x = f2 . x ; ::_thesis: verum end; hence the mapping of it1 = the mapping of it2 by FUNCT_2:12; ::_thesis: verum end; hence it1 = it2 by A6, A9, A12, RELAT_1:def_2; ::_thesis: verum end; end; :: deftheorem Def4 defines a_net YELLOW19:def_4_:_ for L being non empty 1-sorted for O being non empty Subset of L for F being Filter of (BoolePoset O) for b4 being non empty strict NetStr over L holds ( b4 = a_net F iff ( the carrier of b4 = { [a,f] where a is Element of L, f is Element of F : a in f } & ( for i, j being Element of b4 holds ( i <= j iff j `2 c= i `2 ) ) & ( for i being Element of b4 holds b4 . i = i `1 ) ) ); registration let L be non empty 1-sorted ; let O be non empty Subset of L; let F be Filter of (BoolePoset O); cluster a_net F -> non empty reflexive transitive strict ; coherence ( a_net F is reflexive & a_net F is transitive ) proof for x, y, z being set st x in the carrier of (a_net F) & y in the carrier of (a_net F) & z in the carrier of (a_net F) & [x,y] in the InternalRel of (a_net F) & [y,z] in the InternalRel of (a_net F) holds [x,z] in the InternalRel of (a_net F) proof let x, y, z be set ; ::_thesis: ( x in the carrier of (a_net F) & y in the carrier of (a_net F) & z in the carrier of (a_net F) & [x,y] in the InternalRel of (a_net F) & [y,z] in the InternalRel of (a_net F) implies [x,z] in the InternalRel of (a_net F) ) assume that A1: x in the carrier of (a_net F) and A2: y in the carrier of (a_net F) and A3: z in the carrier of (a_net F) and A4: [x,y] in the InternalRel of (a_net F) and A5: [y,z] in the InternalRel of (a_net F) ; ::_thesis: [x,z] in the InternalRel of (a_net F) reconsider k = z as Element of (a_net F) by A3; reconsider j = y as Element of (a_net F) by A2; j <= k by A5, ORDERS_2:def_5; then A6: k `2 c= j `2 by Def4; reconsider i = x as Element of (a_net F) by A1; i <= j by A4, ORDERS_2:def_5; then j `2 c= i `2 by Def4; then k `2 c= i `2 by A6, XBOOLE_1:1; then i <= k by Def4; hence [x,z] in the InternalRel of (a_net F) by ORDERS_2:def_5; ::_thesis: verum end; then A7: the InternalRel of (a_net F) is_transitive_in the carrier of (a_net F) by RELAT_2:def_8; for x being set st x in the carrier of (a_net F) holds [x,x] in the InternalRel of (a_net F) proof let x be set ; ::_thesis: ( x in the carrier of (a_net F) implies [x,x] in the InternalRel of (a_net F) ) assume x in the carrier of (a_net F) ; ::_thesis: [x,x] in the InternalRel of (a_net F) then reconsider i = x as Element of (a_net F) ; i `2 c= i `2 ; then i <= i by Def4; hence [x,x] in the InternalRel of (a_net F) by ORDERS_2:def_5; ::_thesis: verum end; then the InternalRel of (a_net F) is_reflexive_in the carrier of (a_net F) by RELAT_2:def_1; hence ( a_net F is reflexive & a_net F is transitive ) by A7, ORDERS_2:def_2, ORDERS_2:def_3; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let O be non empty Subset of L; let F be proper Filter of (BoolePoset O); cluster a_net F -> non empty strict directed ; coherence a_net F is directed proof set S = { [a,f] where a is Element of L, f is Element of F : a in f } ; for x, y being Element of (a_net F) st x in [#] (a_net F) & y in [#] (a_net F) holds ex z being Element of (a_net F) st ( z in [#] (a_net F) & x <= z & y <= z ) proof let x, y be Element of (a_net F); ::_thesis: ( x in [#] (a_net F) & y in [#] (a_net F) implies ex z being Element of (a_net F) st ( z in [#] (a_net F) & x <= z & y <= z ) ) assume that x in [#] (a_net F) and y in [#] (a_net F) ; ::_thesis: ex z being Element of (a_net F) st ( z in [#] (a_net F) & x <= z & y <= z ) x in the carrier of (a_net F) ; then x in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4; then consider a being Element of L, f being Element of F such that A1: x = [a,f] and a in f ; reconsider f = f as Element of (BoolePoset O) ; y in the carrier of (a_net F) ; then y in { [a,f] where a is Element of L, f is Element of F : a in f } by Def4; then consider b being Element of L, g being Element of F such that A2: y = [b,g] and b in g ; reconsider g = g as Element of (BoolePoset O) ; reconsider h = f "/\" g as Element of F by WAYBEL_0:41; set s = the Element of h; A3: h c= O by WAYBEL_8:26; not Bottom (BoolePoset O) in F by WAYBEL_7:4; then not {} in F by YELLOW_1:18; then A4: h <> {} ; then the Element of h in h ; then the Element of h in O by A3; then reconsider s = the Element of h as Element of L ; [s,h] in { [a,f] where a is Element of L, f is Element of F : a in f } by A4; then reconsider z = [s,h] as Element of (a_net F) by Def4; reconsider i = x, j = y, k = z as Element of (a_net F) ; A5: [b,g] `2 = g ; take z ; ::_thesis: ( z in [#] (a_net F) & x <= z & y <= z ) A6: [s,h] `2 = h ; f /\ g c= g by XBOOLE_1:17; then A7: h c= g by YELLOW_1:17; f /\ g c= f by XBOOLE_1:17; then A8: h c= f by YELLOW_1:17; [a,f] `2 = f ; hence ( z in [#] (a_net F) & x <= z & y <= z ) by A5, A6, A8, A7, Def4, A1, A2; ::_thesis: verum end; then [#] (a_net F) is directed by WAYBEL_0:def_1; hence a_net F is directed by WAYBEL_0:def_6; ::_thesis: verum end; end; theorem Th13: :: YELLOW19:13 for T being non empty 1-sorted for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F) proof let T be non empty 1-sorted ; ::_thesis: for F being Filter of (BoolePoset ([#] T)) holds F \ {{}} = a_filter (a_net F) let F be Filter of (BoolePoset ([#] T)); ::_thesis: F \ {{}} = a_filter (a_net F) set X = a_filter (a_net F); A1: the carrier of (a_net F) = { [a,f] where a is Element of T, f is Element of F : a in f } by Def4; A2: BoolePoset ([#] T) = InclPoset (bool ([#] T)) by YELLOW_1:4; thus F \ {{}} c= a_filter (a_net F) :: according to XBOOLE_0:def_10 ::_thesis: a_filter (a_net F) c= F \ {{}} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F \ {{}} or x in a_filter (a_net F) ) assume A3: x in F \ {{}} ; ::_thesis: x in a_filter (a_net F) then reconsider A = x as Subset of T by A2, YELLOW_1:1; set a = the Element of A; not x in {{}} by A3, XBOOLE_0:def_5; then A4: A <> {} by TARSKI:def_1; then the Element of A in A ; then reconsider a = the Element of A as Element of T ; x in F by A3, XBOOLE_0:def_5; then [a,A] in the carrier of (a_net F) by A1, A4; then reconsider i = [a,A] as Element of (a_net F) ; a_net F is_eventually_in A proof take i ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of (a_net F) holds ( not i <= b1 or (a_net F) . b1 in A ) let j be Element of (a_net F); ::_thesis: ( not i <= j or (a_net F) . j in A ) A5: i `2 = A by MCART_1:7; A6: (a_net F) . j = j `1 by Def4; assume i <= j ; ::_thesis: (a_net F) . j in A then A7: j `2 c= i `2 by Def4; j in the carrier of (a_net F) ; then consider a being Element of T, f being Element of F such that A8: j = [a,f] and A9: a in f by A1; A10: j `1 = a by A8, MCART_1:7; j `2 = f by A8, MCART_1:7; hence (a_net F) . j in A by A9, A7, A6, A5, A10; ::_thesis: verum end; hence x in a_filter (a_net F) ; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a_filter (a_net F) or x in F \ {{}} ) assume A11: x in a_filter (a_net F) ; ::_thesis: x in F \ {{}} then a_net F is_eventually_in x by Th10; then consider i being Element of (a_net F) such that A12: for j being Element of (a_net F) st i <= j holds (a_net F) . j in x by WAYBEL_0:def_11; i in the carrier of (a_net F) ; then consider a being Element of T, f being Element of F such that A13: i = [a,f] and A14: a in f by A1; A15: the carrier of (BoolePoset ([#] T)) = bool ([#] T) by A2, YELLOW_1:1; A16: f c= x proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f or x in x ) assume A17: x in f ; ::_thesis: x in x then reconsider b = x as Element of T by A15; [b,f] in the carrier of (a_net F) by A1, A17; then reconsider j = [b,f] as Element of (a_net F) ; A18: j `2 = f by MCART_1:7; j `1 = b by MCART_1:7; then A19: (a_net F) . j = b by Def4; i `2 = f by A13, MCART_1:7; then i <= j by A18, Def4; hence x in x by A12, A19; ::_thesis: verum end; x is Subset of T by A11, Th10; then A20: x in F by A16, WAYBEL_7:7; not x in {{}} by A14, A16, TARSKI:def_1; hence x in F \ {{}} by A20, XBOOLE_0:def_5; ::_thesis: verum end; theorem Th14: :: YELLOW19:14 for T being non empty 1-sorted for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F) proof let T be non empty 1-sorted ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) holds F = a_filter (a_net F) let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: F = a_filter (a_net F) not {} in F by Th1; then F \ {{}} = F by ZFMISC_1:57; hence F = a_filter (a_net F) by Th13; ::_thesis: verum end; theorem Th15: :: YELLOW19:15 for T being non empty 1-sorted for F being Filter of (BoolePoset ([#] T)) for A being non empty Subset of T holds ( A in F iff a_net F is_eventually_in A ) proof let T be non empty 1-sorted ; ::_thesis: for F being Filter of (BoolePoset ([#] T)) for A being non empty Subset of T holds ( A in F iff a_net F is_eventually_in A ) let F be Filter of (BoolePoset ([#] T)); ::_thesis: for A being non empty Subset of T holds ( A in F iff a_net F is_eventually_in A ) let B be non empty Subset of T; ::_thesis: ( B in F iff a_net F is_eventually_in B ) A1: ( B in F iff B in F \ {{}} ) by ZFMISC_1:56; F \ {{}} = a_filter (a_net F) by Th13; hence ( B in F iff a_net F is_eventually_in B ) by A1, Th10; ::_thesis: verum end; theorem Th16: :: YELLOW19:16 for T being non empty TopSpace for F being proper Filter of (BoolePoset ([#] T)) for x being Point of T holds ( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) for x being Point of T holds ( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: for x being Point of T holds ( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) F = a_filter (a_net F) by Th14; hence for x being Point of T holds ( x is_a_cluster_point_of a_net F iff x is_a_cluster_point_of F,T ) by Th11; ::_thesis: verum end; theorem Th17: :: YELLOW19:17 for T being non empty TopSpace for F being proper Filter of (BoolePoset ([#] T)) for x being Point of T holds ( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) for x being Point of T holds ( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: for x being Point of T holds ( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) F = a_filter (a_net F) by Th14; hence for x being Point of T holds ( x in Lim (a_net F) iff x is_a_convergence_point_of F,T ) by Th12; ::_thesis: verum end; theorem Th18: :: YELLOW19:18 for T being non empty TopSpace for x being Point of T for A being Subset of T st x in Cl A holds for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds a_net F is_often_in A proof let T be non empty TopSpace; ::_thesis: for x being Point of T for A being Subset of T st x in Cl A holds for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds a_net F is_often_in A let x be Point of T; ::_thesis: for A being Subset of T st x in Cl A holds for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds a_net F is_often_in A let A be Subset of T; ::_thesis: ( x in Cl A implies for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds a_net F is_often_in A ) assume A1: x in Cl A ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) st F = NeighborhoodSystem x holds a_net F is_often_in A let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: ( F = NeighborhoodSystem x implies a_net F is_often_in A ) assume A2: F = NeighborhoodSystem x ; ::_thesis: a_net F is_often_in A set N = a_net F; let i be Element of (a_net F); :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of (a_net F) st ( i <= b1 & (a_net F) . b1 in A ) A3: the carrier of (a_net F) = { [a,f] where a is Element of T, f is Element of F : a in f } by Def4; i in the carrier of (a_net F) ; then consider a being Element of T, f being Element of F such that A4: i = [a,f] and a in f by A3; reconsider f = f as a_neighborhood of x by A2, Th2; A5: i `2 = f by A4, MCART_1:7; f meets A by A1, CONNSP_2:27; then consider b being set such that A6: b in f and A7: b in A by XBOOLE_0:3; reconsider b = b as Element of T by A6; [b,f] in the carrier of (a_net F) by A3, A6; then reconsider j = [b,f] as Element of (a_net F) ; take j ; ::_thesis: ( i <= j & (a_net F) . j in A ) A8: j `1 = b by MCART_1:7; j `2 = f by MCART_1:7; hence ( i <= j & (a_net F) . j in A ) by A7, A5, A8, Def4; ::_thesis: verum end; theorem Th19: :: YELLOW19:19 for T being non empty 1-sorted for A being set for N being net of T st N is_eventually_in A holds for S being subnet of N holds S is_eventually_in A proof let T be non empty 1-sorted ; ::_thesis: for A being set for N being net of T st N is_eventually_in A holds for S being subnet of N holds S is_eventually_in A let A be set ; ::_thesis: for N being net of T st N is_eventually_in A holds for S being subnet of N holds S is_eventually_in A let N be net of T; ::_thesis: ( N is_eventually_in A implies for S being subnet of N holds S is_eventually_in A ) given i being Element of N such that A1: for j being Element of N st i <= j holds N . j in A ; :: according to WAYBEL_0:def_11 ::_thesis: for S being subnet of N holds S is_eventually_in A let S be subnet of N; ::_thesis: S is_eventually_in A consider f being Function of S,N such that A2: the mapping of S = the mapping of N * f and A3: for m being Element of N ex n being Element of S st for p being Element of S st n <= p holds m <= f . p by YELLOW_6:def_9; consider n being Element of S such that A4: for p being Element of S st n <= p holds i <= f . p by A3; take n ; :: according to WAYBEL_0:def_11 ::_thesis: for b1 being Element of the carrier of S holds ( not n <= b1 or S . b1 in A ) let p be Element of S; ::_thesis: ( not n <= p or S . p in A ) assume n <= p ; ::_thesis: S . p in A then N . (f . p) in A by A1, A4; hence S . p in A by A2, FUNCT_2:15; ::_thesis: verum end; theorem Th20: :: YELLOW19:20 for T being non empty TopSpace for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds x is_a_convergence_point_of G,T proof let T be non empty TopSpace; ::_thesis: for F, G, x being set st F c= G & x is_a_convergence_point_of F,T holds x is_a_convergence_point_of G,T let F, G, x be set ; ::_thesis: ( F c= G & x is_a_convergence_point_of F,T implies x is_a_convergence_point_of G,T ) assume that A1: F c= G and A2: for A being Subset of T st A is open & x in A holds A in F ; :: according to WAYBEL_7:def_5 ::_thesis: x is_a_convergence_point_of G,T let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in G ) assume that A3: A is open and A4: x in A ; ::_thesis: A in G A in F by A2, A3, A4; hence A in G by A1; ::_thesis: verum end; theorem Th21: :: YELLOW19:21 for T being non empty TopSpace for A being Subset of T for x being Point of T holds ( x in Cl A iff ex N being net of T st ( N is_eventually_in A & x is_a_cluster_point_of N ) ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Point of T holds ( x in Cl A iff ex N being net of T st ( N is_eventually_in A & x is_a_cluster_point_of N ) ) let A be Subset of T; ::_thesis: for x being Point of T holds ( x in Cl A iff ex N being net of T st ( N is_eventually_in A & x is_a_cluster_point_of N ) ) let x be Point of T; ::_thesis: ( x in Cl A iff ex N being net of T st ( N is_eventually_in A & x is_a_cluster_point_of N ) ) reconsider F = NeighborhoodSystem x as proper Filter of (BoolePoset ([#] T)) ; hereby ::_thesis: ( ex N being net of T st ( N is_eventually_in A & x is_a_cluster_point_of N ) implies x in Cl A ) assume x in Cl A ; ::_thesis: ex N9 being net of T st ( N9 is_eventually_in A & x is_a_cluster_point_of N9 ) then reconsider N = (a_net F) " A as subnet of a_net F by Th18, YELLOW_6:22; reconsider N9 = N as net of T ; take N9 = N9; ::_thesis: ( N9 is_eventually_in A & x is_a_cluster_point_of N9 ) thus N9 is_eventually_in A by YELLOW_6:23; ::_thesis: x is_a_cluster_point_of N9 x is_a_convergence_point_of F,T by Th3; then A1: x in Lim (a_net F) by Th17; Lim (a_net F) c= Lim N by YELLOW_6:32; hence x is_a_cluster_point_of N9 by A1, WAYBEL_9:29; ::_thesis: verum end; given N being net of T such that A2: N is_eventually_in A and A3: x is_a_cluster_point_of N ; ::_thesis: x in Cl A consider i being Element of N such that A4: for j being Element of N st i <= j holds N . j in A by A2, WAYBEL_0:def_11; now__::_thesis:_for_G_being_Subset_of_T_st_G_is_open_&_x_in_G_holds_ A_meets_G let G be Subset of T; ::_thesis: ( G is open & x in G implies A meets G ) assume that A5: G is open and A6: x in G ; ::_thesis: A meets G Int G = G by A5, TOPS_1:23; then G is a_neighborhood of x by A6, CONNSP_2:def_1; then N is_often_in G by A3, WAYBEL_9:def_9; then consider j being Element of N such that A7: i <= j and A8: N . j in G by WAYBEL_0:def_12; N . j in A by A4, A7; hence A meets G by A8, XBOOLE_0:3; ::_thesis: verum end; hence x in Cl A by PRE_TOPC:def_7; ::_thesis: verum end; theorem Th22: :: YELLOW19:22 for T being non empty TopSpace for A being Subset of T for x being Point of T holds ( x in Cl A iff ex N being convergent net of T st ( N is_eventually_in A & x in Lim N ) ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Point of T holds ( x in Cl A iff ex N being convergent net of T st ( N is_eventually_in A & x in Lim N ) ) let A be Subset of T; ::_thesis: for x being Point of T holds ( x in Cl A iff ex N being convergent net of T st ( N is_eventually_in A & x in Lim N ) ) let x be Point of T; ::_thesis: ( x in Cl A iff ex N being convergent net of T st ( N is_eventually_in A & x in Lim N ) ) hereby ::_thesis: ( ex N being convergent net of T st ( N is_eventually_in A & x in Lim N ) implies x in Cl A ) assume x in Cl A ; ::_thesis: ex S being convergent net of T st ( S is_eventually_in A & x in Lim S ) then consider N being net of T such that A1: N is_eventually_in A and A2: x is_a_cluster_point_of N by Th21; consider S being subnet of N such that A3: x in Lim S by A2, WAYBEL_9:32; reconsider S = S as convergent net of T by A3, YELLOW_6:def_16; take S = S; ::_thesis: ( S is_eventually_in A & x in Lim S ) thus S is_eventually_in A by A1, Th19; ::_thesis: x in Lim S thus x in Lim S by A3; ::_thesis: verum end; given N being convergent net of T such that A4: N is_eventually_in A and A5: x in Lim N ; ::_thesis: x in Cl A x is_a_cluster_point_of N by A5, WAYBEL_9:29; hence x in Cl A by A4, Th21; ::_thesis: verum end; theorem :: YELLOW19:23 for T being non empty TopSpace for A being Subset of T holds ( A is closed iff for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is closed iff for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ) let A be Subset of T; ::_thesis: ( A is closed iff for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ) ( A is closed iff Cl A = A ) by PRE_TOPC:22; hence ( A is closed implies for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ) by Th21; ::_thesis: ( ( for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ) implies A is closed ) assume A1: for N being net of T st N is_eventually_in A holds for x being Point of T st x is_a_cluster_point_of N holds x in A ; ::_thesis: A is closed A = Cl A proof thus A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A ) assume A2: x in Cl A ; ::_thesis: x in A then reconsider y = x as Element of T ; ex N being net of T st ( N is_eventually_in A & y is_a_cluster_point_of N ) by A2, Th21; hence x in A by A1; ::_thesis: verum end; hence A is closed ; ::_thesis: verum end; theorem :: YELLOW19:24 for T being non empty TopSpace for A being Subset of T holds ( A is closed iff for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is closed iff for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ) let A be Subset of T; ::_thesis: ( A is closed iff for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ) ( A is closed iff Cl A = A ) by PRE_TOPC:22; hence ( A is closed implies for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ) by Th22; ::_thesis: ( ( for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ) implies A is closed ) assume A1: for N being convergent net of T st N is_eventually_in A holds for x being Point of T st x in Lim N holds x in A ; ::_thesis: A is closed A = Cl A proof thus A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A ) assume A2: x in Cl A ; ::_thesis: x in A then reconsider y = x as Element of T ; ex N being convergent net of T st ( N is_eventually_in A & y in Lim N ) by A2, Th22; hence x in A by A1; ::_thesis: verum end; hence A is closed ; ::_thesis: verum end; theorem Th25: :: YELLOW19:25 for T being non empty TopSpace for A being Subset of T for x being Point of T holds ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Point of T holds ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) ) let A be Subset of T; ::_thesis: for x being Point of T holds ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) ) let x be Point of T; ::_thesis: ( x in Cl A iff ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) ) hereby ::_thesis: ( ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) implies x in Cl A ) assume x in Cl A ; ::_thesis: ex F being Subset of (BoolePoset ([#] T)) st ( A in F & x is_a_cluster_point_of F,T ) then consider N being net of T such that A1: N is_eventually_in A and A2: x is_a_cluster_point_of N by Th21; set F = a_filter N; take F = a_filter N; ::_thesis: ( A in F & x is_a_cluster_point_of F,T ) thus A in F by A1; ::_thesis: x is_a_cluster_point_of F,T thus x is_a_cluster_point_of F,T by A2, Th11; ::_thesis: verum end; given F being proper Filter of (BoolePoset ([#] T)) such that A3: A in F and A4: x is_a_cluster_point_of F,T ; ::_thesis: x in Cl A reconsider F9 = F as proper Filter of (BoolePoset ([#] T)) ; A5: a_filter (a_net F9) = F by Th14; then A6: x is_a_cluster_point_of a_net F9 by A4, Th11; a_net F9 is_eventually_in A by A3, A5, Th10; hence x in Cl A by A6, Th21; ::_thesis: verum end; theorem Th26: :: YELLOW19:26 for T being non empty TopSpace for A being Subset of T for x being Point of T holds ( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_convergence_point_of F,T ) ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T for x being Point of T holds ( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_convergence_point_of F,T ) ) let A be Subset of T; ::_thesis: for x being Point of T holds ( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_convergence_point_of F,T ) ) let x be Point of T; ::_thesis: ( x in Cl A iff ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_convergence_point_of F,T ) ) hereby ::_thesis: ( ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & x is_a_convergence_point_of F,T ) implies x in Cl A ) assume x in Cl A ; ::_thesis: ex G being ultra Filter of (BoolePoset ([#] T)) st ( A in G & x is_a_convergence_point_of G,T ) then consider N being net of T such that A1: N is_eventually_in A and A2: x is_a_cluster_point_of N by Th21; consider S being subnet of N such that A3: x in Lim S by A2, WAYBEL_9:32; set F = a_filter S; consider G being Filter of (BoolePoset ([#] T)) such that A4: a_filter S c= G and A5: G is ultra by WAYBEL_7:26; reconsider G = G as ultra Filter of (BoolePoset ([#] T)) by A5; take G = G; ::_thesis: ( A in G & x is_a_convergence_point_of G,T ) S is_eventually_in A by A1, Th19; then A in a_filter S ; hence A in G by A4; ::_thesis: x is_a_convergence_point_of G,T x is_a_convergence_point_of a_filter S,T by A3, Th12; hence x is_a_convergence_point_of G,T by A4, Th20; ::_thesis: verum end; given F being ultra Filter of (BoolePoset ([#] T)) such that A6: A in F and A7: x is_a_convergence_point_of F,T ; ::_thesis: x in Cl A x is_a_cluster_point_of F,T by A7, WAYBEL_7:27; hence x in Cl A by A6, Th25; ::_thesis: verum end; theorem :: YELLOW19:27 for T being non empty TopSpace for A being Subset of T holds ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ) let A be Subset of T; ::_thesis: ( A is closed iff for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ) ( A is closed iff Cl A = A ) by PRE_TOPC:22; hence ( A is closed implies for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ) by Th25; ::_thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ) implies A is closed ) assume A1: for F being proper Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_cluster_point_of F,T holds x in A ; ::_thesis: A is closed A = Cl A proof thus A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A ) assume A2: x in Cl A ; ::_thesis: x in A then reconsider y = x as Element of T ; ex F being proper Filter of (BoolePoset ([#] T)) st ( A in F & y is_a_cluster_point_of F,T ) by A2, Th25; hence x in A by A1; ::_thesis: verum end; hence A is closed ; ::_thesis: verum end; theorem :: YELLOW19:28 for T being non empty TopSpace for A being Subset of T holds ( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ) proof let T be non empty TopSpace; ::_thesis: for A being Subset of T holds ( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ) let A be Subset of T; ::_thesis: ( A is closed iff for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ) ( A is closed iff Cl A = A ) by PRE_TOPC:22; hence ( A is closed implies for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ) by Th26; ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ) implies A is closed ) assume A1: for F being ultra Filter of (BoolePoset ([#] T)) st A in F holds for x being Point of T st x is_a_convergence_point_of F,T holds x in A ; ::_thesis: A is closed A = Cl A proof thus A c= Cl A by PRE_TOPC:18; :: according to XBOOLE_0:def_10 ::_thesis: Cl A c= A let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in A ) assume A2: x in Cl A ; ::_thesis: x in A then reconsider y = x as Element of T ; ex F being ultra Filter of (BoolePoset ([#] T)) st ( A in F & y is_a_convergence_point_of F,T ) by A2, Th26; hence x in A by A1; ::_thesis: verum end; hence A is closed ; ::_thesis: verum end; theorem Th29: :: YELLOW19:29 for T being non empty TopSpace for N being net of T for s being Point of T holds ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A ) proof let T be non empty TopSpace; ::_thesis: for N being net of T for s being Point of T holds ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A ) let N be net of T; ::_thesis: for s being Point of T holds ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A ) let s be Point of T; ::_thesis: ( s is_a_cluster_point_of N iff for A being Subset of T,N holds s in Cl A ) hereby ::_thesis: ( ( for A being Subset of T,N holds s in Cl A ) implies s is_a_cluster_point_of N ) assume A1: s is_a_cluster_point_of N ; ::_thesis: for A being Subset of T,N holds s in Cl A let A be Subset of T,N; ::_thesis: s in Cl A N is_eventually_in A by Th8; hence s in Cl A by A1, Th21; ::_thesis: verum end; assume A2: for A being Subset of T,N holds s in Cl A ; ::_thesis: s is_a_cluster_point_of N let V be a_neighborhood of s; :: according to WAYBEL_9:def_9 ::_thesis: N is_often_in V let i be Element of N; :: according to WAYBEL_0:def_12 ::_thesis: ex b1 being Element of the carrier of N st ( i <= b1 & N . b1 in V ) reconsider A = rng the mapping of (N | i) as Subset of T,N by Def2; set x = the Element of A /\ (Int V); A3: s in Int V by CONNSP_2:def_1; s in Cl A by A2; then A meets Int V by A3, PRE_TOPC:def_7; then A4: A /\ (Int V) <> {} T by XBOOLE_0:def_7; then A5: the Element of A /\ (Int V) in Int V by XBOOLE_0:def_4; A6: Int V c= V by TOPS_1:16; the Element of A /\ (Int V) in A by A4, XBOOLE_0:def_4; then consider j being set such that A7: j in dom the mapping of (N | i) and A8: the Element of A /\ (Int V) = the mapping of (N | i) . j by FUNCT_1:def_3; A9: the carrier of (N | i) = { l where l is Element of N : i <= l } by WAYBEL_9:12; reconsider j = j as Element of (N | i) by A7; dom the mapping of (N | i) = the carrier of (N | i) by FUNCT_2:def_1; then consider l being Element of N such that A10: j = l and A11: i <= l by A7, A9; take l ; ::_thesis: ( i <= l & N . l in V ) thus i <= l by A11; ::_thesis: N . l in V the Element of A /\ (Int V) = (N | i) . j by A8 .= N . l by A10, WAYBEL_9:16 ; hence N . l in V by A5, A6; ::_thesis: verum end; theorem :: YELLOW19:30 for T being non empty TopSpace for F being Subset-Family of T st F is closed holds FinMeetCl F is closed proof let T be non empty TopSpace; ::_thesis: for F being Subset-Family of T st F is closed holds FinMeetCl F is closed let F be Subset-Family of T; ::_thesis: ( F is closed implies FinMeetCl F is closed ) assume A1: F is closed ; ::_thesis: FinMeetCl F is closed now__::_thesis:_for_P_being_Subset_of_T_st_P_in_FinMeetCl_F_holds_ P_is_closed let P be Subset of T; ::_thesis: ( P in FinMeetCl F implies P is closed ) assume P in FinMeetCl F ; ::_thesis: P is closed then consider Y being Subset-Family of T such that A2: Y c= F and Y is finite and A3: P = Intersect Y by CANTOR_1:def_3; A4: ( ( P = the carrier of T & the carrier of T = [#] T ) or P = meet Y ) by A3, SETFAM_1:def_9; for A being Subset of T st A in Y holds A is closed by A1, A2, TOPS_2:def_2; hence P is closed by A4, PRE_TOPC:14; ::_thesis: verum end; hence FinMeetCl F is closed by TOPS_2:def_2; ::_thesis: verum end; Lm1: for T being non empty TopSpace st T is compact holds for N being net of T ex x being Point of T st x is_a_cluster_point_of N proof let T be non empty TopSpace; ::_thesis: ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) assume A1: T is compact ; ::_thesis: for N being net of T ex x being Point of T st x is_a_cluster_point_of N let N be net of T; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N set F = { (Cl A) where A is Subset of T,N : verum } ; { (Cl A) where A is Subset of T,N : verum } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Cl A) where A is Subset of T,N : verum } or x in bool the carrier of T ) assume x in { (Cl A) where A is Subset of T,N : verum } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T,N st x = Cl A ; hence x in bool the carrier of T ; ::_thesis: verum end; then reconsider F = { (Cl A) where A is Subset of T,N : verum } as Subset-Family of T ; set x = the Element of meet F; A2: F is centered proof defpred S1[ set , set ] means ex A being Subset of T,N ex i being Element of N st ( \$1 = Cl A & \$2 = i & A = rng the mapping of (N | i) ); set A0 = the Subset of T,N; Cl the Subset of T,N in F ; hence F <> {} ; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds ( b1 = {} or not b1 c= F or not b1 is finite or not meet b1 = {} ) let G be set ; ::_thesis: ( G = {} or not G c= F or not G is finite or not meet G = {} ) assume that A3: G <> {} and A4: G c= F and A5: G is finite ; ::_thesis: not meet G = {} A6: now__::_thesis:_for_x_being_set_st_x_in_G_holds_ ex_y_being_set_st_ (_y_in_the_carrier_of_N_&_S1[x,y]_) let x be set ; ::_thesis: ( x in G implies ex y being set st ( y in the carrier of N & S1[x,y] ) ) assume x in G ; ::_thesis: ex y being set st ( y in the carrier of N & S1[x,y] ) then x in F by A4; then consider A being Subset of T,N such that A7: x = Cl A ; consider i being Element of N such that A8: A = rng the mapping of (N | i) by Def2; reconsider y = i as set ; take y = y; ::_thesis: ( y in the carrier of N & S1[x,y] ) thus y in the carrier of N ; ::_thesis: S1[x,y] thus S1[x,y] by A7, A8; ::_thesis: verum end; consider f being Function such that A9: ( dom f = G & rng f c= the carrier of N ) and A10: for x being set st x in G holds S1[x,f . x] from FUNCT_1:sch_5(A6); reconsider B = rng f as finite Subset of N by A5, A9, FINSET_1:8; [#] N is directed by WAYBEL_0:def_6; then consider j being Element of N such that j in [#] N and A11: j is_>=_than B by WAYBEL_0:1; now__::_thesis:_for_X_being_set_st_X_in_G_holds_ N_._j_in_X let X be set ; ::_thesis: ( X in G implies N . j in X ) assume A12: X in G ; ::_thesis: N . j in X then consider A being Subset of T,N, i being Element of N such that A13: X = Cl A and A14: f . X = i and A15: A = rng the mapping of (N | i) by A10; A16: A c= X by A13, PRE_TOPC:18; A17: the mapping of (N | i) = the mapping of N | the carrier of (N | i) by WAYBEL_9:def_7; i in B by A9, A12, A14, FUNCT_1:def_3; then i <= j by A11, LATTICE3:def_9; then j in the carrier of (N | i) by WAYBEL_9:def_7; then A18: j in dom the mapping of (N | i) by FUNCT_2:def_1; then the mapping of (N | i) . j in A by A15, FUNCT_1:def_3; then N . j in A by A18, A17, FUNCT_1:47; hence N . j in X by A16; ::_thesis: verum end; hence not meet G = {} by A3, SETFAM_1:def_1; ::_thesis: verum end; F is closed proof let S be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not S in F or S is closed ) assume S in F ; ::_thesis: S is closed then ex A being Subset of T,N st S = Cl A ; hence S is closed ; ::_thesis: verum end; then A19: meet F <> {} by A1, A2, COMPTS_1:4; then the Element of meet F in meet F ; then reconsider x = the Element of meet F as Point of T ; take x ; ::_thesis: x is_a_cluster_point_of N now__::_thesis:_for_A_being_Subset_of_T,N_holds_x_in_Cl_A let A be Subset of T,N; ::_thesis: x in Cl A Cl A in F ; hence x in Cl A by A19, SETFAM_1:def_1; ::_thesis: verum end; hence x is_a_cluster_point_of N by Th29; ::_thesis: verum end; Lm2: for T being non empty TopSpace st ( for N being net of T st N in NetUniv T holds ex x being Point of T st x is_a_cluster_point_of N ) holds T is compact proof let T be non empty TopSpace; ::_thesis: ( ( for N being net of T st N in NetUniv T holds ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact ) assume A1: for N being net of T st N in NetUniv T holds ex x being Point of T st x is_a_cluster_point_of N ; ::_thesis: T is compact now__::_thesis:_for_F_being_Subset-Family_of_T_st_F_is_centered_&_F_is_closed_holds_ meet_F_<>_{} set X = the carrier of T; defpred S1[ set , set ] means \$2 in \$1; let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} ) assume that A2: F is centered and A3: F is closed ; ::_thesis: meet F <> {} set G = FinMeetCl F; A4: now__::_thesis:_for_x_being_set_st_x_in_FinMeetCl_F_holds_ ex_y_being_set_st_ (_y_in_the_carrier_of_T_&_S1[x,y]_) let x be set ; ::_thesis: ( x in FinMeetCl F implies ex y being set st ( y in the carrier of T & S1[x,y] ) ) set y = the Element of x; assume x in FinMeetCl F ; ::_thesis: ex y being set st ( y in the carrier of T & S1[x,y] ) then consider Y being Subset-Family of T such that A5: Y c= F and A6: Y is finite and A7: x = Intersect Y by CANTOR_1:def_3; ( Y = {} or Y <> {} ) ; then ( x = the carrier of T or ( x = meet Y & meet Y <> {} ) ) by A2, A5, A6, A7, FINSET_1:def_3, SETFAM_1:def_9; then the Element of x in x ; hence ex y being set st ( y in the carrier of T & S1[x,y] ) by A7; ::_thesis: verum end; consider f being Function such that A8: ( dom f = FinMeetCl F & rng f c= the carrier of T ) and A9: for a being set st a in FinMeetCl F holds S1[a,f . a] from FUNCT_1:sch_5(A4); A10: F c= FinMeetCl F by CANTOR_1:4; A11: F <> {} by A2, FINSET_1:def_3; then reconsider G = FinMeetCl F as non empty Subset-Family of T by A10; set R = (InclPoset G) opp ; A12: InclPoset G = RelStr(# G,(RelIncl G) #) by YELLOW_1:def_1; then A13: the carrier of ((InclPoset G) opp) = G by YELLOW_6:3; (InclPoset G) opp is directed proof let x, y be Element of ((InclPoset G) opp); :: according to WAYBEL_0:def_1,WAYBEL_0:def_6 ::_thesis: ( not x in [#] ((InclPoset G) opp) or not y in [#] ((InclPoset G) opp) or ex b1 being Element of the carrier of ((InclPoset G) opp) st ( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 ) ) assume that x in [#] ((InclPoset G) opp) and y in [#] ((InclPoset G) opp) ; ::_thesis: ex b1 being Element of the carrier of ((InclPoset G) opp) st ( b1 in [#] ((InclPoset G) opp) & x <= b1 & y <= b1 ) A14: ~ x = x by LATTICE3:def_7; y in G by A13; then consider Y being Subset-Family of T such that A15: Y c= F and A16: Y is finite and A17: y = Intersect Y by CANTOR_1:def_3; x in G by A13; then consider X being Subset-Family of T such that A18: X c= F and A19: X is finite and A20: x = Intersect X by CANTOR_1:def_3; set z = Intersect (X \/ Y); X \/ Y c= F by A18, A15, XBOOLE_1:8; then reconsider z = Intersect (X \/ Y) as Element of ((InclPoset G) opp) by A13, A19, A16, CANTOR_1:def_3; A21: ~ z = z by LATTICE3:def_7; take z ; ::_thesis: ( z in [#] ((InclPoset G) opp) & x <= z & y <= z ) thus z in [#] ((InclPoset G) opp) ; ::_thesis: ( x <= z & y <= z ) A22: ~ y = y by LATTICE3:def_7; z c= y by A17, SETFAM_1:44, XBOOLE_1:7; then A23: ~ z <= ~ y by A22, A21, YELLOW_1:3; z c= x by A20, SETFAM_1:44, XBOOLE_1:7; then ~ z <= ~ x by A14, A21, YELLOW_1:3; hence ( x <= z & y <= z ) by A23, YELLOW_7:1; ::_thesis: verum end; then reconsider R = (InclPoset G) opp as non empty transitive directed RelStr ; reconsider f = f as Function of the carrier of R, the carrier of T by A8, A13, FUNCT_2:2; set N = R *' f; A24: RelStr(# the carrier of (R *' f), the InternalRel of (R *' f) #) = RelStr(# the carrier of R, the InternalRel of R #) by WAYBEL32:def_3; A25: the_universe_of the carrier of T = Tarski-Class (the_transitive-closure_of the carrier of T) by YELLOW_6:def_1; the carrier of T c= the_transitive-closure_of the carrier of T by CLASSES1:52; then the carrier of T in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:2, CLASSES1:3; then bool the carrier of T in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:4; then G in Tarski-Class (the_transitive-closure_of the carrier of T) by CLASSES1:3; then R *' f in NetUniv T by A13, A24, A25, YELLOW_6:def_11; then consider x being Point of T such that A26: x is_a_cluster_point_of R *' f by A1; A27: the mapping of (R *' f) = f by WAYBEL32:def_3; now__::_thesis:_for_X_being_set_st_X_in_F_holds_ x_in_X let X be set ; ::_thesis: ( X in F implies x in X ) assume A28: X in F ; ::_thesis: x in X then reconsider A = X as Subset of T ; reconsider a = X as Element of (R *' f) by A10, A12, A24, A28, YELLOW_6:3; A29: now__::_thesis:_for_V_being_Subset_of_T_st_V_is_open_&_x_in_V_holds_ A_meets_V let V be Subset of T; ::_thesis: ( V is open & x in V implies A meets V ) assume that A30: V is open and A31: x in V ; ::_thesis: A meets V Int V = V by A30, TOPS_1:23; then V is a_neighborhood of x by A31, CONNSP_2:def_1; then R *' f is_often_in V by A26, WAYBEL_9:def_9; then consider b being Element of (R *' f) such that A32: a <= b and A33: (R *' f) . b in V by WAYBEL_0:def_12; reconsider a9 = a, b9 = b as Element of ((InclPoset G) opp) by A24; a9 <= b9 by A24, A32, YELLOW_0:1; then A34: ~ a9 >= ~ b9 by YELLOW_7:1; A35: ~ b9 = b by LATTICE3:def_7; ~ a9 = A by LATTICE3:def_7; then A36: b c= A by A34, A35, YELLOW_1:3; (R *' f) . b in b by A9, A12, A27, A35; hence A meets V by A33, A36, XBOOLE_0:3; ::_thesis: verum end; A is closed by A3, A28, TOPS_2:def_2; then Cl A = A by PRE_TOPC:22; hence x in X by A29, PRE_TOPC:def_7; ::_thesis: verum end; hence meet F <> {} by A11, SETFAM_1:def_1; ::_thesis: verum end; hence T is compact by COMPTS_1:4; ::_thesis: verum end; theorem Th31: :: YELLOW19:31 for T being non empty TopSpace holds ( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) set X = the carrier of T; hereby ::_thesis: ( ( for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ) implies T is compact ) assume A1: T is compact ; ::_thesis: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T let F be ultra Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_convergence_point_of F,T set G = { (Cl A) where A is Subset of T : A in F } ; { (Cl A) where A is Subset of T : A in F } c= bool the carrier of T proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Cl A) where A is Subset of T : A in F } or x in bool the carrier of T ) assume x in { (Cl A) where A is Subset of T : A in F } ; ::_thesis: x in bool the carrier of T then ex A being Subset of T st ( x = Cl A & A in F ) ; hence x in bool the carrier of T ; ::_thesis: verum end; then reconsider G = { (Cl A) where A is Subset of T : A in F } as Subset-Family of T ; A2: G is centered proof set A0 = the Element of F; reconsider A0 = the Element of F as Subset of T by WAYBEL_7:2; Cl A0 in G ; hence G <> {} ; :: according to FINSET_1:def_3 ::_thesis: for b1 being set holds ( b1 = {} or not b1 c= G or not b1 is finite or not meet b1 = {} ) let H be set ; ::_thesis: ( H = {} or not H c= G or not H is finite or not meet H = {} ) assume that A3: H <> {} and A4: H c= G and A5: H is finite ; ::_thesis: not meet H = {} reconsider H1 = H as finite Subset-Family of the carrier of T by A4, A5, XBOOLE_1:1; H1 c= F proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H1 or x in F ) assume x in H1 ; ::_thesis: x in F then x in G by A4; then consider A being Subset of T such that A6: x = Cl A and A7: A in F ; A c= Cl A by PRE_TOPC:18; hence x in F by A6, A7, WAYBEL_7:7; ::_thesis: verum end; then Intersect H1 in F by WAYBEL_7:11; then Intersect H1 <> {} by Th1; hence not meet H = {} by A3, SETFAM_1:def_9; ::_thesis: verum end; set x = the Element of meet G; G is closed proof let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in G or A is closed ) assume A in G ; ::_thesis: A is closed then ex B being Subset of T st ( A = Cl B & B in F ) ; hence A is closed ; ::_thesis: verum end; then A8: meet G <> {} by A1, A2, COMPTS_1:4; then the Element of meet G in meet G ; then reconsider x = the Element of meet G as Point of T ; take x = x; ::_thesis: x is_a_convergence_point_of F,T thus x is_a_convergence_point_of F,T ::_thesis: verum proof let A be Subset of T; :: according to WAYBEL_7:def_5 ::_thesis: ( not A is open or not x in A or A in F ) assume that A9: A is open and A10: x in A ; ::_thesis: A in F set B = A ` ; A11: now__::_thesis:_not_A_`_in_F assume A ` in F ; ::_thesis: contradiction then Cl (A `) in G ; then A12: A ` in G by A9, PRE_TOPC:22; not x in A ` by A10, XBOOLE_0:def_5; hence contradiction by A8, A12, SETFAM_1:def_1; ::_thesis: verum end; F is prime by WAYBEL_7:22; hence A in F by A11, WAYBEL_7:21; ::_thesis: verum end; end; assume A13: for F being ultra Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_convergence_point_of F,T ; ::_thesis: T is compact now__::_thesis:_for_F_being_Subset-Family_of_T_st_F_is_centered_&_F_is_closed_holds_ meet_F_<>_{} set L = BoolePoset the carrier of T; let F be Subset-Family of T; ::_thesis: ( F is centered & F is closed implies meet F <> {} ) assume A14: ( F is centered & F is closed ) ; ::_thesis: meet F <> {} reconsider Y = F as Subset of (BoolePoset the carrier of T) by WAYBEL_7:2; set G = uparrow (fininfs Y); now__::_thesis:_not_Bottom_(BoolePoset_the_carrier_of_T)_in_uparrow_(fininfs_Y) assume Bottom (BoolePoset the carrier of T) in uparrow (fininfs Y) ; ::_thesis: contradiction then consider x being Element of (BoolePoset the carrier of T) such that A15: x <= Bottom (BoolePoset the carrier of T) and A16: x in fininfs Y by WAYBEL_0:def_16; A17: Bottom (BoolePoset the carrier of T) = {} by YELLOW_1:18; consider Z being finite Subset of Y such that A18: x = "/\" (Z,(BoolePoset the carrier of T)) and ex_inf_of Z, BoolePoset the carrier of T by A16; reconsider Z = Z as Subset of (BoolePoset the carrier of T) by XBOOLE_1:1; A19: x = Bottom (BoolePoset the carrier of T) by A15, YELLOW_5:19; then x <> Top (BoolePoset the carrier of T) by WAYBEL_7:3; then A20: Z <> {} by A18, YELLOW_0:def_12; then meet Z <> {} by A14, FINSET_1:def_3; hence contradiction by A17, A18, A19, A20, YELLOW_1:20; ::_thesis: verum end; then uparrow (fininfs Y) is proper by WAYBEL_7:4; then consider UF being Filter of (BoolePoset the carrier of T) such that A21: uparrow (fininfs Y) c= UF and A22: UF is ultra by WAYBEL_7:26; consider x being Point of T such that A23: x is_a_convergence_point_of UF,T by A13, A22; F c= uparrow (fininfs Y) by WAYBEL_0:62; then A24: F c= UF by A21, XBOOLE_1:1; A25: now__::_thesis:_for_A_being_set_st_A_in_F_holds_ x_in_A let A be set ; ::_thesis: ( A in F implies x in A ) assume A26: A in F ; ::_thesis: x in A then reconsider B = A as Subset of T ; A27: now__::_thesis:_for_C_being_Subset_of_T_st_C_is_open_&_x_in_C_holds_ A_meets_C let C be Subset of T; ::_thesis: ( C is open & x in C implies A meets C ) assume that A28: C is open and A29: x in C ; ::_thesis: A meets C A30: C in UF by A23, A28, A29, WAYBEL_7:def_5; A in UF by A24, A26; then reconsider c = C, a = A as Element of (BoolePoset the carrier of T) by A30; a "/\" c in UF by A24, A26, A30, WAYBEL_0:41; then a "/\" c <> {} by A22, Th1; then A /\ C <> {} by YELLOW_1:17; hence A meets C by XBOOLE_0:def_7; ::_thesis: verum end; B is closed by A14, A26, TOPS_2:def_2; then Cl B = B by PRE_TOPC:22; hence x in A by A27, PRE_TOPC:24; ::_thesis: verum end; F <> {} by A14, FINSET_1:def_3; hence meet F <> {} by A25, SETFAM_1:def_1; ::_thesis: verum end; hence T is compact by COMPTS_1:4; ::_thesis: verum end; theorem :: YELLOW19:32 for T being non empty TopSpace holds ( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ) hereby ::_thesis: ( ( for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ) implies T is compact ) assume A1: T is compact ; ::_thesis: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T let F be proper Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_cluster_point_of F,T reconsider G = F as proper Filter of (BoolePoset ([#] T)) ; consider x being Point of T such that A2: x is_a_cluster_point_of a_net G by A1, Lm1; take x = x; ::_thesis: x is_a_cluster_point_of F,T thus x is_a_cluster_point_of F,T by A2, Th16; ::_thesis: verum end; assume A3: for F being proper Filter of (BoolePoset ([#] T)) ex x being Point of T st x is_a_cluster_point_of F,T ; ::_thesis: T is compact now__::_thesis:_for_N_being_net_of_T_st_N_in_NetUniv_T_holds_ ex_x_being_Point_of_T_st_x_is_a_cluster_point_of_N let N be net of T; ::_thesis: ( N in NetUniv T implies ex x being Point of T st x is_a_cluster_point_of N ) assume N in NetUniv T ; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N reconsider F = a_filter N as proper Filter of (BoolePoset the carrier of T) ; consider x being Point of T such that A4: x is_a_cluster_point_of F,T by A3; take x = x; ::_thesis: x is_a_cluster_point_of N thus x is_a_cluster_point_of N by A4, Th11; ::_thesis: verum end; hence T is compact by Lm2; ::_thesis: verum end; theorem Th33: :: YELLOW19:33 for T being non empty TopSpace holds ( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) thus ( T is compact implies for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) by Lm1; ::_thesis: ( ( for N being net of T ex x being Point of T st x is_a_cluster_point_of N ) implies T is compact ) assume for N being net of T ex x being Point of T st x is_a_cluster_point_of N ; ::_thesis: T is compact then for N being net of T st N in NetUniv T holds ex x being Point of T st x is_a_cluster_point_of N ; hence T is compact by Lm2; ::_thesis: verum end; theorem :: YELLOW19:34 for T being non empty TopSpace holds ( T is compact iff for N being net of T st N in NetUniv T holds ex x being Point of T st x is_a_cluster_point_of N ) by Lm1, Lm2; registration let L be non empty 1-sorted ; let N be transitive NetStr over L; cluster full -> transitive full for SubNetStr of N; coherence for b1 being full SubNetStr of N holds b1 is transitive proof let S be full SubNetStr of N; ::_thesis: S is transitive S is full SubRelStr of N by YELLOW_6:def_7; hence S is transitive ; ::_thesis: verum end; end; registration let L be non empty 1-sorted ; let N be non empty directed NetStr over L; cluster non empty strict directed full for SubNetStr of N; existence ex b1 being SubNetStr of N st ( b1 is strict & not b1 is empty & b1 is directed & b1 is full ) proof set S = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #); A1: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of N, the InternalRel of N #) ; N is full SubRelStr of N by YELLOW_6:6; then A2: NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) is full SubRelStr of N by A1, WAYBEL21:12; N is SubNetStr of N by YELLOW_6:8; then the mapping of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) = the mapping of N | the carrier of NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) by YELLOW_6:def_6; then reconsider S = NetStr(# the carrier of N, the InternalRel of N, the mapping of N #) as non empty strict full SubNetStr of N by A2, YELLOW_6:def_6, YELLOW_6:def_7; [#] N is directed by WAYBEL_0:def_6; then [#] S is directed by A1, WAYBEL_0:3; then S is directed by WAYBEL_0:def_6; hence ex b1 being SubNetStr of N st ( b1 is strict & not b1 is empty & b1 is directed & b1 is full ) ; ::_thesis: verum end; end; theorem :: YELLOW19:35 for T being non empty TopSpace holds ( T is compact iff for N being net of T ex S being subnet of N st S is convergent ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for N being net of T ex S being subnet of N st S is convergent ) hereby ::_thesis: ( ( for N being net of T ex S being subnet of N st S is convergent ) implies T is compact ) assume A1: T is compact ; ::_thesis: for N being net of T ex S being subnet of N st S is convergent let N be net of T; ::_thesis: ex S being subnet of N st S is convergent consider x being Point of T such that A2: x is_a_cluster_point_of N by A1, Th33; consider S being subnet of N such that A3: x in Lim S by A2, WAYBEL_9:32; take S = S; ::_thesis: S is convergent thus S is convergent by A3, YELLOW_6:def_16; ::_thesis: verum end; assume A4: for N being net of T ex S being subnet of N st S is convergent ; ::_thesis: T is compact now__::_thesis:_for_N_being_net_of_T_ex_x_being_Point_of_T_st_x_is_a_cluster_point_of_N let N be net of T; ::_thesis: ex x being Point of T st x is_a_cluster_point_of N consider S being subnet of N such that A5: S is convergent by A4; set x = the Element of Lim S; A6: Lim S <> {} by A5, YELLOW_6:def_16; then the Element of Lim S in Lim S ; then reconsider x = the Element of Lim S as Point of T ; take x = x; ::_thesis: x is_a_cluster_point_of N thus x is_a_cluster_point_of N by A6, WAYBEL_9:29, WAYBEL_9:31; ::_thesis: verum end; hence T is compact by Th33; ::_thesis: verum end; definition let S be non empty 1-sorted ; let N be non empty NetStr over S; attrN is Cauchy means :: YELLOW19:def 5 for A being Subset of S holds ( N is_eventually_in A or N is_eventually_in A ` ); end; :: deftheorem defines Cauchy YELLOW19:def_5_:_ for S being non empty 1-sorted for N being non empty NetStr over S holds ( N is Cauchy iff for A being Subset of S holds ( N is_eventually_in A or N is_eventually_in A ` ) ); registration let S be non empty 1-sorted ; let F be ultra Filter of (BoolePoset ([#] S)); cluster a_net F -> non empty strict Cauchy ; coherence a_net F is Cauchy proof let A be Subset of S; :: according to YELLOW19:def_5 ::_thesis: ( a_net F is_eventually_in A or a_net F is_eventually_in A ` ) F is prime by WAYBEL_7:22; then A1: ( ( ( A is empty or not A is empty ) & ( A ` is empty or not A ` is empty ) & A in F ) or A ` in F ) by WAYBEL_7:21; ({} S) ` = [#] S ; then ( A ` = {} S implies A = [#] S ) ; hence ( a_net F is_eventually_in A or a_net F is_eventually_in A ` ) by A1, Th15, YELLOW_6:20; ::_thesis: verum end; end; theorem :: YELLOW19:36 for T being non empty TopSpace holds ( T is compact iff for N being net of T st N is Cauchy holds N is convergent ) proof let T be non empty TopSpace; ::_thesis: ( T is compact iff for N being net of T st N is Cauchy holds N is convergent ) thus ( T is compact implies for N being net of T st N is Cauchy holds N is convergent ) ::_thesis: ( ( for N being net of T st N is Cauchy holds N is convergent ) implies T is compact ) proof assume A1: T is compact ; ::_thesis: for N being net of T st N is Cauchy holds N is convergent let N be net of T; ::_thesis: ( N is Cauchy implies N is convergent ) assume A2: for A being Subset of T holds ( N is_eventually_in A or N is_eventually_in A ` ) ; :: according to YELLOW19:def_5 ::_thesis: N is convergent consider x being Point of T such that A3: x is_a_cluster_point_of N by A1, Lm1; now__::_thesis:_for_V_being_a_neighborhood_of_x_holds_N_is_eventually_in_V let V be a_neighborhood of x; ::_thesis: N is_eventually_in V assume not N is_eventually_in V ; ::_thesis: contradiction then N is_eventually_in V ` by A2; then consider i being Element of N such that A4: for j being Element of N st i <= j holds N . j in V ` by WAYBEL_0:def_11; N is_often_in V by A3, WAYBEL_9:def_9; then consider j being Element of N such that A5: i <= j and A6: N . j in V by WAYBEL_0:def_12; N . j in V ` by A4, A5; hence contradiction by A6, XBOOLE_0:def_5; ::_thesis: verum end; then x in Lim N by YELLOW_6:def_15; hence N is convergent by YELLOW_6:def_16; ::_thesis: verum end; assume A7: for N being net of T st N is Cauchy holds N is convergent ; ::_thesis: T is compact now__::_thesis:_for_F_being_ultra_Filter_of_(BoolePoset_([#]_T))_ex_x_being_Point_of_T_st_x_is_a_convergence_point_of_F,T let F be ultra Filter of (BoolePoset ([#] T)); ::_thesis: ex x being Point of T st x is_a_convergence_point_of F,T set x = the Element of Lim (a_net F); a_net F is convergent by A7; then A8: Lim (a_net F) <> {} by YELLOW_6:def_16; then the Element of Lim (a_net F) in Lim (a_net F) ; then reconsider x = the Element of Lim (a_net F) as Point of T ; take x = x; ::_thesis: x is_a_convergence_point_of F,T thus x is_a_convergence_point_of F,T by A8, Th17; ::_thesis: verum end; hence T is compact by Th31; ::_thesis: verum end;