:: SETLIM_1 semantic presentation begin Lm1: for i, j being Element of NAT holds ( not i <= j or i = j or i + 1 <= j ) proof let i, j be Element of NAT ; ::_thesis: ( not i <= j or i = j or i + 1 <= j ) assume i <= j ; ::_thesis: ( i = j or i + 1 <= j ) then i + 1 <= j + 1 by XREAL_1:6; hence ( i = j or i + 1 <= j ) by NAT_1:8, XCMPLX_1:2; ::_thesis: verum end; theorem Th1: :: SETLIM_1:1 for n, m being Element of NAT for Y being set for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k } proof let n, m be Element of NAT ; ::_thesis: for Y being set for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k } let Y be set ; ::_thesis: for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k } n <= n + m by NAT_1:11; hence for f being Function of NAT,Y holds f . (n + m) in { (f . k) where k is Element of NAT : n <= k } ; ::_thesis: verum end; theorem Th2: :: SETLIM_1:2 for n being Element of NAT for Y being set for f being Function of NAT,Y holds { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} proof let n be Element of NAT ; ::_thesis: for Y being set for f being Function of NAT,Y holds { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} let Y be set ; ::_thesis: for f being Function of NAT,Y holds { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} let f be Function of NAT,Y; ::_thesis: { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} set Z1 = { (f . k1) where k1 is Element of NAT : n <= k1 } ; set Z2 = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } ; A1: { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} c= { (f . k1) where k1 is Element of NAT : n <= k1 } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} or x in { (f . k1) where k1 is Element of NAT : n <= k1 } ) assume A2: x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} ; ::_thesis: x in { (f . k1) where k1 is Element of NAT : n <= k1 } now__::_thesis:_(_(_x_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_+_1_<=_k2__}__&_x_in__{__(f_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}__)_or_(_x_in_{(f_._n)}_&_x_in__{__(f_._k1)_where_k1_is_Element_of_NAT_:_n_<=_k1__}__)_) percases ( x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } or x in {(f . n)} ) by A2, XBOOLE_0:def_3; case x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } ; ::_thesis: x in { (f . k1) where k1 is Element of NAT : n <= k1 } then consider z being set such that A3: x = z and A4: z in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } ; consider k11 being Element of NAT such that A5: z = f . k11 and A6: n + 1 <= k11 by A4; n <= k11 by A6, NAT_1:13; hence x in { (f . k1) where k1 is Element of NAT : n <= k1 } by A3, A5; ::_thesis: verum end; case x in {(f . n)} ; ::_thesis: x in { (f . k1) where k1 is Element of NAT : n <= k1 } then x = f . n by TARSKI:def_1; hence x in { (f . k1) where k1 is Element of NAT : n <= k1 } ; ::_thesis: verum end; end; end; hence x in { (f . k1) where k1 is Element of NAT : n <= k1 } ; ::_thesis: verum end; { (f . k1) where k1 is Element of NAT : n <= k1 } c= { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . k1) where k1 is Element of NAT : n <= k1 } or x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} ) assume x in { (f . k1) where k1 is Element of NAT : n <= k1 } ; ::_thesis: x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} then consider z being set such that A7: x = z and A8: z in { (f . k1) where k1 is Element of NAT : n <= k1 } ; consider k being Element of NAT such that A9: ( z = f . k & n <= k ) by A8; ( ( z = f . k & n + 1 <= k ) or ( z = f . k & n = k ) ) by A9, Lm1; then ( z in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } or z in {(f . n)} ) by TARSKI:def_1; hence x in { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} by A7, XBOOLE_0:def_3; ::_thesis: verum end; hence { (f . k1) where k1 is Element of NAT : n <= k1 } = { (f . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(f . n)} by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th3: :: SETLIM_1:3 for n being Element of NAT for Y, x being set for f being Function of NAT,Y holds ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z ) proof let n be Element of NAT ; ::_thesis: for Y, x being set for f being Function of NAT,Y holds ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z ) let Y, x be set ; ::_thesis: for f being Function of NAT,Y holds ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z ) let f be Function of NAT,Y; ::_thesis: ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z ) set Z = { (f . k2) where k2 is Element of NAT : n <= k2 } ; now__::_thesis:_(_(_for_k1_being_Element_of_NAT_holds_x_in_f_._(n_+_k1)_)_implies_for_Z1_being_set_st_Z1_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_<=_k2__}__holds_ x_in_Z1_) assume A1: for k1 being Element of NAT holds x in f . (n + k1) ; ::_thesis: for Z1 being set st Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z1 now__::_thesis:_for_Z1_being_set_st_Z1_in__{__(f_._k2)_where_k2_is_Element_of_NAT_:_n_<=_k2__}__holds_ x_in_Z1 let Z1 be set ; ::_thesis: ( Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } implies x in Z1 ) assume Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } ; ::_thesis: x in Z1 then consider k1 being Element of NAT such that A2: Z1 = f . k1 and A3: n <= k1 ; ex m being Nat st k1 = n + m by A3, NAT_1:10; then consider k2 being Nat such that A4: Z1 = f . (n + k2) by A2; k2 in NAT by ORDINAL1:def_12; hence x in Z1 by A1, A4; ::_thesis: verum end; hence for Z1 being set st Z1 in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z1 ; ::_thesis: verum end; hence ( ( for k1 being Element of NAT holds x in f . (n + k1) ) iff for Z being set st Z in { (f . k2) where k2 is Element of NAT : n <= k2 } holds x in Z ) by Th1; ::_thesis: verum end; theorem Th4: :: SETLIM_1:4 for x being set for Y being non empty set for f being Function of NAT,Y holds ( x in rng f iff ex n being Element of NAT st x = f . n ) proof let x be set ; ::_thesis: for Y being non empty set for f being Function of NAT,Y holds ( x in rng f iff ex n being Element of NAT st x = f . n ) let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds ( x in rng f iff ex n being Element of NAT st x = f . n ) let f be Function of NAT,Y; ::_thesis: ( x in rng f iff ex n being Element of NAT st x = f . n ) thus ( x in rng f implies ex n being Element of NAT st x = f . n ) ::_thesis: ( ex n being Element of NAT st x = f . n implies x in rng f ) proof assume x in rng f ; ::_thesis: ex n being Element of NAT st x = f . n then consider y being set such that A1: y in dom f and A2: x = f . y by FUNCT_1:def_3; reconsider m = y as Element of NAT by A1; take m ; ::_thesis: x = f . m thus x = f . m by A2; ::_thesis: verum end; given n being Element of NAT such that A3: x = f . n ; ::_thesis: x in rng f dom f = NAT by FUNCT_2:def_1; hence x in rng f by A3, FUNCT_1:def_3; ::_thesis: verum end; theorem Th5: :: SETLIM_1:5 for Y being non empty set for f being Function of NAT,Y holds rng f = { (f . k) where k is Element of NAT : 0 <= k } proof let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds rng f = { (f . k) where k is Element of NAT : 0 <= k } let f be Function of NAT,Y; ::_thesis: rng f = { (f . k) where k is Element of NAT : 0 <= k } set Z = { (f . k) where k is Element of NAT : 0 <= k } ; A1: dom f = NAT by FUNCT_2:def_1; A2: rng f c= { (f . k) where k is Element of NAT : 0 <= k } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in { (f . k) where k is Element of NAT : 0 <= k } ) assume y in rng f ; ::_thesis: y in { (f . k) where k is Element of NAT : 0 <= k } then consider n being set such that A3: n in NAT and A4: y = f . n by A1, FUNCT_1:def_3; reconsider n = n as Element of NAT by A3; 0 <= n by NAT_1:2; hence y in { (f . k) where k is Element of NAT : 0 <= k } by A4; ::_thesis: verum end; { (f . k) where k is Element of NAT : 0 <= k } c= rng f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . k) where k is Element of NAT : 0 <= k } or x in rng f ) assume x in { (f . k) where k is Element of NAT : 0 <= k } ; ::_thesis: x in rng f then ex n1 being Element of NAT st ( x = f . n1 & 0 <= n1 ) ; hence x in rng f by FUNCT_2:4; ::_thesis: verum end; hence rng f = { (f . k) where k is Element of NAT : 0 <= k } by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th6: :: SETLIM_1:6 for k being Element of NAT for Y being non empty set for f being Function of NAT,Y holds rng (f ^\ k) = { (f . n) where n is Element of NAT : k <= n } proof let k be Element of NAT ; ::_thesis: for Y being non empty set for f being Function of NAT,Y holds rng (f ^\ k) = { (f . n) where n is Element of NAT : k <= n } let Y be non empty set ; ::_thesis: for f being Function of NAT,Y holds rng (f ^\ k) = { (f . n) where n is Element of NAT : k <= n } let f be Function of NAT,Y; ::_thesis: rng (f ^\ k) = { (f . n) where n is Element of NAT : k <= n } reconsider f1 = f ^\ k as Function of NAT,Y ; rng f1 = { (f . m) where m is Element of NAT : k <= m } proof set Z = { (f . m) where m is Element of NAT : k <= m } ; A1: dom f1 = NAT by FUNCT_2:def_1; A2: rng f1 c= { (f . m) where m is Element of NAT : k <= m } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f1 or y in { (f . m) where m is Element of NAT : k <= m } ) assume y in rng f1 ; ::_thesis: y in { (f . m) where m is Element of NAT : k <= m } then consider m1 being set such that A3: m1 in NAT and A4: y = f1 . m1 by A1, FUNCT_1:def_3; reconsider m1 = m1 as Element of NAT by A3; y = f . (k + m1) by A4, NAT_1:def_3; hence y in { (f . m) where m is Element of NAT : k <= m } by Th1; ::_thesis: verum end; { (f . m) where m is Element of NAT : k <= m } c= rng f1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . m) where m is Element of NAT : k <= m } or x in rng f1 ) assume x in { (f . m) where m is Element of NAT : k <= m } ; ::_thesis: x in rng f1 then consider k1 being Element of NAT such that A5: x = f . k1 and A6: k <= k1 ; consider k2 being Nat such that A7: k1 = k + k2 by A6, NAT_1:10; ( k2 in NAT & x = f1 . k2 ) by A5, A7, NAT_1:def_3, ORDINAL1:def_12; hence x in rng f1 by FUNCT_2:4; ::_thesis: verum end; hence rng f1 = { (f . m) where m is Element of NAT : k <= m } by A2, XBOOLE_0:def_10; ::_thesis: verum end; hence rng (f ^\ k) = { (f . n) where n is Element of NAT : k <= n } ; ::_thesis: verum end; theorem Th7: :: SETLIM_1:7 for X, x being set for B being SetSequence of X holds ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) proof let X, x be set ; ::_thesis: for B being SetSequence of X holds ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) let B be SetSequence of X; ::_thesis: ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) A1: dom B = NAT by FUNCT_2:def_1; A2: now__::_thesis:_for_x_being_set_st_(_for_n_being_Element_of_NAT_holds_x_in_B_._n_)_holds_ x_in_meet_(rng_B) let x be set ; ::_thesis: ( ( for n being Element of NAT holds x in B . n ) implies x in meet (rng B) ) assume A3: for n being Element of NAT holds x in B . n ; ::_thesis: x in meet (rng B) now__::_thesis:_for_Y_being_set_st_Y_in_rng_B_holds_ x_in_Y let Y be set ; ::_thesis: ( Y in rng B implies x in Y ) assume Y in rng B ; ::_thesis: x in Y then consider n being set such that A4: n in NAT and A5: Y = B . n by A1, FUNCT_1:def_3; thus x in Y by A3, A4, A5; ::_thesis: verum end; hence x in meet (rng B) by SETFAM_1:def_1; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_B)_holds_ for_n_being_Element_of_NAT_holds_x_in_B_._n let x be set ; ::_thesis: ( x in meet (rng B) implies for n being Element of NAT holds x in B . n ) assume A6: x in meet (rng B) ; ::_thesis: for n being Element of NAT holds x in B . n now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_B_._k let k be Element of NAT ; ::_thesis: x in B . k B . k in rng B by FUNCT_2:4; hence x in B . k by A6, SETFAM_1:def_1; ::_thesis: verum end; hence for n being Element of NAT holds x in B . n ; ::_thesis: verum end; hence ( x in meet (rng B) iff for n being Element of NAT holds x in B . n ) by A2; ::_thesis: verum end; theorem Th8: :: SETLIM_1:8 for X being set for B being SetSequence of X holds Intersection B = meet (rng B) proof let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B = meet (rng B) let B be SetSequence of X; ::_thesis: Intersection B = meet (rng B) now__::_thesis:_for_x_being_set_st_x_in_meet_(rng_B)_holds_ x_in_Intersection_B let x be set ; ::_thesis: ( x in meet (rng B) implies x in Intersection B ) assume x in meet (rng B) ; ::_thesis: x in Intersection B then for n being Element of NAT holds x in B . n by Th7; hence x in Intersection B by PROB_1:13; ::_thesis: verum end; then A1: meet (rng B) c= Intersection B by TARSKI:def_3; Intersection B c= meet (rng B) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection B or x in meet (rng B) ) assume x in Intersection B ; ::_thesis: x in meet (rng B) then for n being Element of NAT holds x in B . n by PROB_1:13; hence x in meet (rng B) by Th7; ::_thesis: verum end; hence Intersection B = meet (rng B) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: SETLIM_1:9 for X being set for B being SetSequence of X holds Intersection B c= Union B proof let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= Union B let B be SetSequence of X; ::_thesis: Intersection B c= Union B meet (rng B) c= union (rng B) by SETFAM_1:2; then Intersection B c= union (rng B) by Th8; hence Intersection B c= Union B by CARD_3:def_4; ::_thesis: verum end; theorem Th10: :: SETLIM_1:10 for X being set for A being Subset of X for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Union B = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Union B = A let A be Subset of X; ::_thesis: for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Union B = A let B be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds B . n = A ) implies Union B = A ) assume A1: for n being Element of NAT holds B . n = A ; ::_thesis: Union B = A now__::_thesis:_for_x_being_set_st_x_in_rng_B_holds_ x_=_A let x be set ; ::_thesis: ( x in rng B implies x = A ) assume x in rng B ; ::_thesis: x = A then ex n being Element of NAT st x = B . n by Th4; hence x = A by A1; ::_thesis: verum end; then rng B = {A} by ZFMISC_1:35; then union (rng B) = A by ZFMISC_1:25; hence Union B = A by CARD_3:def_4; ::_thesis: verum end; theorem Th11: :: SETLIM_1:11 for X being set for A being Subset of X for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Intersection B = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Intersection B = A let A be Subset of X; ::_thesis: for B being SetSequence of X st ( for n being Element of NAT holds B . n = A ) holds Intersection B = A let B be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds B . n = A ) implies Intersection B = A ) assume A1: for n being Element of NAT holds B . n = A ; ::_thesis: Intersection B = A now__::_thesis:_for_x_being_set_st_x_in_rng_B_holds_ x_=_A let x be set ; ::_thesis: ( x in rng B implies x = A ) assume x in rng B ; ::_thesis: x = A then ex n being Element of NAT st x = B . n by Th4; hence x = A by A1; ::_thesis: verum end; then rng B = {A} by ZFMISC_1:35; then meet (rng B) = A by SETFAM_1:10; hence Intersection B = A by Th8; ::_thesis: verum end; theorem :: SETLIM_1:12 for X being set for B being SetSequence of X st B is constant holds Union B = Intersection B proof let X be set ; ::_thesis: for B being SetSequence of X st B is constant holds Union B = Intersection B let B be SetSequence of X; ::_thesis: ( B is constant implies Union B = Intersection B ) assume B is constant ; ::_thesis: Union B = Intersection B then consider A being Subset of X such that A1: for n being Nat holds B . n = A by VALUED_0:def_18; A2: for n being Element of NAT holds B . n = A by A1; then Union B = A by Th10; hence Union B = Intersection B by A2, Th11; ::_thesis: verum end; Lm2: for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) ) assume that A1: B is constant and A2: the_value_of B = A ; ::_thesis: for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) consider x being set such that A3: x in dom B and A4: A = B . x by A1, A2, FUNCT_1:def_12; dom B = NAT by FUNCT_2:def_1; then for n being Element of NAT holds B . n = A by A1, A3, A4, FUNCT_1:def_10; hence for n being Element of NAT holds ( B . n = A & Union B = A & Intersection B = A ) by Th10, Th11; ::_thesis: verum end; theorem Th13: :: SETLIM_1:13 for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds union { (B . k) where k is Element of NAT : n <= k } = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds union { (B . k) where k is Element of NAT : n <= k } = A let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds union { (B . k) where k is Element of NAT : n <= k } = A let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds union { (B . k) where k is Element of NAT : n <= k } = A ) assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds union { (B . k) where k is Element of NAT : n <= k } = A let n be Element of NAT ; ::_thesis: union { (B . k) where k is Element of NAT : n <= k } = A set Y = { (B . k) where k is Element of NAT : n <= k } ; A2: now__::_thesis:_for_x_being_set_st_x_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_=_A let x be set ; ::_thesis: ( x in { (B . k) where k is Element of NAT : n <= k } implies x = A ) assume x in { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: x = A then ex k being Element of NAT st ( x = B . k & n <= k ) ; hence x = A by A1, Lm2; ::_thesis: verum end; { (B . k) where k is Element of NAT : n <= k } <> {} by Th1; then { (B . k) where k is Element of NAT : n <= k } = {A} by A2, ZFMISC_1:35; hence union { (B . k) where k is Element of NAT : n <= k } = A by ZFMISC_1:25; ::_thesis: verum end; theorem Th14: :: SETLIM_1:14 for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A ) assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds meet { (B . k) where k is Element of NAT : n <= k } = A let n be Element of NAT ; ::_thesis: meet { (B . k) where k is Element of NAT : n <= k } = A set Y = { (B . k) where k is Element of NAT : n <= k } ; A2: now__::_thesis:_for_x_being_set_st_x_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_=_A let x be set ; ::_thesis: ( x in { (B . k) where k is Element of NAT : n <= k } implies x = A ) assume x in { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: x = A then ex k being Element of NAT st ( x = B . k & n <= k ) ; hence x = A by A1, Lm2; ::_thesis: verum end; { (B . k) where k is Element of NAT : n <= k } <> {} by Th1; then { (B . k) where k is Element of NAT : n <= k } = {A} by A2, ZFMISC_1:35; hence meet { (B . k) where k is Element of NAT : n <= k } = A by SETFAM_1:10; ::_thesis: verum end; theorem Th15: :: SETLIM_1:15 for X being set for B being SetSequence of X for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds f is SetSequence of X proof let X be set ; ::_thesis: for B being SetSequence of X for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds f is SetSequence of X let B be SetSequence of X; ::_thesis: for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds f is SetSequence of X let f be Function; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ) implies f is SetSequence of X ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n = meet { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: f is SetSequence of X rng f c= bool X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in bool X ) assume z in rng f ; ::_thesis: z in bool X then consider x being set such that A3: x in dom f and A4: z = f . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A1, A3; set Y = { (B . k) where k is Element of NAT : n <= k } ; set y = meet { (B . k) where k is Element of NAT : n <= k } ; A5: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X proof A6: now__::_thesis:_(__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__<>_{}_implies_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__is_Subset_of_X_) assume { (B . k) where k is Element of NAT : n <= k } <> {} ; ::_thesis: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X then consider Z1 being set such that A7: Z1 in { (B . k) where k is Element of NAT : n <= k } by XBOOLE_0:def_1; A8: ex k1 being Element of NAT st ( Z1 = B . k1 & n <= k1 ) by A7; now__::_thesis:_for_x_being_set_st_x_in_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ x_in_X let x be set ; ::_thesis: ( x in meet { (B . k) where k is Element of NAT : n <= k } implies x in X ) assume x in meet { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: x in X then x in Z1 by A7, SETFAM_1:def_1; hence x in X by A8; ::_thesis: verum end; hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by TARSKI:def_3; ::_thesis: verum end; now__::_thesis:_(__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__=_{}_implies_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__is_Subset_of_X_) assume { (B . k) where k is Element of NAT : n <= k } = {} ; ::_thesis: meet { (B . k) where k is Element of NAT : n <= k } is Subset of X then meet { (B . k) where k is Element of NAT : n <= k } = {} by SETFAM_1:def_1; hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by XBOOLE_1:2; ::_thesis: verum end; hence meet { (B . k) where k is Element of NAT : n <= k } is Subset of X by A6; ::_thesis: verum end; z = meet { (B . k) where k is Element of NAT : n <= k } by A2, A4; hence z in bool X by A5; ::_thesis: verum end; hence f is SetSequence of X by A1, FUNCT_2:2; ::_thesis: verum end; theorem Th16: :: SETLIM_1:16 for X being set for B being SetSequence of X for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union { (B . k) where k is Element of NAT : n <= k } ) holds f is Function of NAT,(bool X) proof let X be set ; ::_thesis: for B being SetSequence of X for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union { (B . k) where k is Element of NAT : n <= k } ) holds f is Function of NAT,(bool X) let B be SetSequence of X; ::_thesis: for f being Function st dom f = NAT & ( for n being Element of NAT holds f . n = union { (B . k) where k is Element of NAT : n <= k } ) holds f is Function of NAT,(bool X) let f be Function; ::_thesis: ( dom f = NAT & ( for n being Element of NAT holds f . n = union { (B . k) where k is Element of NAT : n <= k } ) implies f is Function of NAT,(bool X) ) assume that A1: dom f = NAT and A2: for n being Element of NAT holds f . n = union { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: f is Function of NAT,(bool X) rng f c= bool X proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng f or z in bool X ) assume z in rng f ; ::_thesis: z in bool X then consider x being set such that A3: x in dom f and A4: z = f . x by FUNCT_1:def_3; reconsider n = x as Element of NAT by A1, A3; set Y = { (B . k) where k is Element of NAT : n <= k } ; set y = union { (B . k) where k is Element of NAT : n <= k } ; now__::_thesis:_for_z_being_set_st_z_in_union__{__(B_._k)_where_k_is_Element_of_NAT_:_n_<=_k__}__holds_ z_in_X let z be set ; ::_thesis: ( z in union { (B . k) where k is Element of NAT : n <= k } implies z in X ) assume z in union { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: z in X then ex Z being set st ( z in Z & Z in { (B . k) where k is Element of NAT : n <= k } ) by TARSKI:def_4; then consider Z1 being set such that A5: Z1 in { (B . k) where k is Element of NAT : n <= k } and A6: z in Z1 ; ex k1 being Element of NAT st ( Z1 = B . k1 & n <= k1 ) by A5; hence z in X by A6; ::_thesis: verum end; then A7: union { (B . k) where k is Element of NAT : n <= k } is Subset of X by TARSKI:def_3; z = union { (B . k) where k is Element of NAT : n <= k } by A2, A4; hence z in bool X by A7; ::_thesis: verum end; hence f is Function of NAT,(bool X) by A1, FUNCT_2:2; ::_thesis: verum end; definition let X be set ; let B be SetSequence of X; attrB is monotone means :Def1: :: SETLIM_1:def 1 ( not B is V50() or not B is V49() ); end; :: deftheorem Def1 defines monotone SETLIM_1:def_1_:_ for X being set for B being SetSequence of X holds ( B is monotone iff ( not B is V50() or not B is V49() ) ); definition let B be Function; func inferior_setsequence B -> Function means :Def2: :: SETLIM_1:def 2 ( dom it = NAT & ( for n being Element of NAT holds it . n = meet { (B . k) where k is Element of NAT : n <= k } ) ); existence ex b1 being Function st ( dom b1 = NAT & ( for n being Element of NAT holds b1 . n = meet { (B . k) where k is Element of NAT : n <= k } ) ) proof deffunc H1( Nat) -> set = meet { (B . k) where k is Element of NAT : \$1 <= k } ; thus ex f being Function st ( dom f = NAT & ( for n being Element of NAT holds f . n = H1(n) ) ) from FUNCT_1:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = NAT & ( for n being Element of NAT holds b1 . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom b2 = NAT & ( for n being Element of NAT holds b2 . n = meet { (B . k) where k is Element of NAT : n <= k } ) holds b1 = b2 proof let BSeq, CSeq be Function; ::_thesis: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) & dom CSeq = NAT & ( for n being Element of NAT holds CSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) implies BSeq = CSeq ) assume that A1: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = meet { (B . k) where k is Element of NAT : n <= k } ) ) and A2: ( dom CSeq = NAT & ( for m being Element of NAT holds CSeq . m = meet { (B . k) where k is Element of NAT : m <= k } ) ) ; ::_thesis: BSeq = CSeq for y being set st y in NAT holds BSeq . y = CSeq . y proof let y be set ; ::_thesis: ( y in NAT implies BSeq . y = CSeq . y ) assume y in NAT ; ::_thesis: BSeq . y = CSeq . y then reconsider y = y as Element of NAT ; set Y = { (B . k) where k is Element of NAT : y <= k } ; BSeq . y = meet { (B . k) where k is Element of NAT : y <= k } by A1; hence BSeq . y = CSeq . y by A2; ::_thesis: verum end; hence BSeq = CSeq by A1, A2, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines inferior_setsequence SETLIM_1:def_2_:_ for B, b2 being Function holds ( b2 = inferior_setsequence B iff ( dom b2 = NAT & ( for n being Element of NAT holds b2 . n = meet { (B . k) where k is Element of NAT : n <= k } ) ) ); definition let X be set ; let B be SetSequence of X; :: original: inferior_setsequence redefine func inferior_setsequence B -> SetSequence of X; coherence inferior_setsequence B is SetSequence of X proof A1: for n being Element of NAT holds (inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by Def2; dom (inferior_setsequence B) = NAT by Def2; hence inferior_setsequence B is SetSequence of X by A1, Th15; ::_thesis: verum end; end; definition let B be Function; func superior_setsequence B -> Function means :Def3: :: SETLIM_1:def 3 ( dom it = NAT & ( for n being Element of NAT holds it . n = union { (B . k) where k is Element of NAT : n <= k } ) ); existence ex b1 being Function st ( dom b1 = NAT & ( for n being Element of NAT holds b1 . n = union { (B . k) where k is Element of NAT : n <= k } ) ) proof deffunc H1( Nat) -> set = union { (B . k) where k is Element of NAT : \$1 <= k } ; thus ex f being Function st ( dom f = NAT & ( for n being Element of NAT holds f . n = H1(n) ) ) from FUNCT_1:sch_4(); ::_thesis: verum end; uniqueness for b1, b2 being Function st dom b1 = NAT & ( for n being Element of NAT holds b1 . n = union { (B . k) where k is Element of NAT : n <= k } ) & dom b2 = NAT & ( for n being Element of NAT holds b2 . n = union { (B . k) where k is Element of NAT : n <= k } ) holds b1 = b2 proof let BSeq, CSeq be Function; ::_thesis: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = union { (B . k) where k is Element of NAT : n <= k } ) & dom CSeq = NAT & ( for n being Element of NAT holds CSeq . n = union { (B . k) where k is Element of NAT : n <= k } ) implies BSeq = CSeq ) assume that A1: ( dom BSeq = NAT & ( for n being Element of NAT holds BSeq . n = union { (B . k) where k is Element of NAT : n <= k } ) ) and A2: ( dom CSeq = NAT & ( for m being Element of NAT holds CSeq . m = union { (B . k) where k is Element of NAT : m <= k } ) ) ; ::_thesis: BSeq = CSeq for y being set st y in NAT holds BSeq . y = CSeq . y proof let y be set ; ::_thesis: ( y in NAT implies BSeq . y = CSeq . y ) assume y in NAT ; ::_thesis: BSeq . y = CSeq . y then reconsider y = y as Element of NAT ; set Y = { (B . k) where k is Element of NAT : y <= k } ; BSeq . y = union { (B . k) where k is Element of NAT : y <= k } by A1; hence BSeq . y = CSeq . y by A2; ::_thesis: verum end; hence BSeq = CSeq by A1, A2, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def3 defines superior_setsequence SETLIM_1:def_3_:_ for B, b2 being Function holds ( b2 = superior_setsequence B iff ( dom b2 = NAT & ( for n being Element of NAT holds b2 . n = union { (B . k) where k is Element of NAT : n <= k } ) ) ); definition let X be set ; let B be SetSequence of X; :: original: superior_setsequence redefine func superior_setsequence B -> SetSequence of X; coherence superior_setsequence B is SetSequence of X proof A1: for n being Element of NAT holds (superior_setsequence B) . n = union { (B . k) where k is Element of NAT : n <= k } by Def3; dom (superior_setsequence B) = NAT by Def3; hence superior_setsequence B is SetSequence of X by A1, Th16; ::_thesis: verum end; end; theorem Th17: :: SETLIM_1:17 for X being set for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B proof let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . 0 = Intersection B let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . 0 = Intersection B (inferior_setsequence B) . 0 = meet { (B . k) where k is Element of NAT : k >= 0 } by Def2 .= meet (rng B) by Th5 .= Intersection B by Th8 ; hence (inferior_setsequence B) . 0 = Intersection B ; ::_thesis: verum end; theorem Th18: :: SETLIM_1:18 for X being set for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B proof let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . 0 = Union B let B be SetSequence of X; ::_thesis: (superior_setsequence B) . 0 = Union B (superior_setsequence B) . 0 = union { (B . k) where k is Element of NAT : 0 <= k } by Def3 .= union (rng B) by Th5 .= Union B by CARD_3:def_4 ; hence (superior_setsequence B) . 0 = Union B ; ::_thesis: verum end; theorem Th19: :: SETLIM_1:19 for n being Element of NAT for X, x being set for B being SetSequence of X holds ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) proof let n be Element of NAT ; ::_thesis: for X, x being set for B being SetSequence of X holds ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) let X, x be set ; ::_thesis: for B being SetSequence of X holds ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) let B be SetSequence of X; ::_thesis: ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) set Y = { (B . k) where k is Element of NAT : n <= k } ; A1: (inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by Def2; A2: now__::_thesis:_(_x_in_(inferior_setsequence_B)_._n_implies_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k)_) assume A3: x in (inferior_setsequence B) . n ; ::_thesis: for k being Element of NAT holds x in B . (n + k) now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k) let k be Element of NAT ; ::_thesis: x in B . (n + k) B . (n + k) in { (B . k) where k is Element of NAT : n <= k } by Th1; hence x in B . (n + k) by A1, A3, SETFAM_1:def_1; ::_thesis: verum end; hence for k being Element of NAT holds x in B . (n + k) ; ::_thesis: verum end; A4: { (B . k) where k is Element of NAT : n <= k } <> {} by Th1; now__::_thesis:_(_(_for_k_being_Element_of_NAT_holds_x_in_B_._(n_+_k)_)_implies_x_in_(inferior_setsequence_B)_._n_) assume for k being Element of NAT holds x in B . (n + k) ; ::_thesis: x in (inferior_setsequence B) . n then for Z being set st Z in { (B . k) where k is Element of NAT : n <= k } holds x in Z by Th3; hence x in (inferior_setsequence B) . n by A1, A4, SETFAM_1:def_1; ::_thesis: verum end; hence ( x in (inferior_setsequence B) . n iff for k being Element of NAT holds x in B . (n + k) ) by A2; ::_thesis: verum end; theorem Th20: :: SETLIM_1:20 for n being Element of NAT for X, x being set for B being SetSequence of X holds ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) ) proof let n be Element of NAT ; ::_thesis: for X, x being set for B being SetSequence of X holds ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) ) let X, x be set ; ::_thesis: for B being SetSequence of X holds ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) ) let B be SetSequence of X; ::_thesis: ( x in (superior_setsequence B) . n iff ex k being Element of NAT st x in B . (n + k) ) set Y = { (B . k) where k is Element of NAT : n <= k } ; A1: (superior_setsequence B) . n = union { (B . k) where k is Element of NAT : n <= k } by Def3; thus ( x in (superior_setsequence B) . n implies ex k being Element of NAT st x in B . (n + k) ) ::_thesis: ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n ) proof assume x in (superior_setsequence B) . n ; ::_thesis: ex k being Element of NAT st x in B . (n + k) then consider Y1 being set such that A2: x in Y1 and A3: Y1 in { (B . k) where k is Element of NAT : n <= k } by A1, TARSKI:def_4; consider k11 being Element of NAT such that A4: Y1 = B . k11 and A5: n <= k11 by A3; ex k being Nat st k11 = n + k by A5, NAT_1:10; then consider k22 being Nat such that A6: Y1 = B . (n + k22) by A4; k22 in NAT by ORDINAL1:def_12; hence ex k being Element of NAT st x in B . (n + k) by A2, A6; ::_thesis: verum end; now__::_thesis:_(_ex_k_being_Element_of_NAT_st_x_in_B_._(n_+_k)_implies_x_in_(superior_setsequence_B)_._n_) assume ex k being Element of NAT st x in B . (n + k) ; ::_thesis: x in (superior_setsequence B) . n then consider k1 being Element of NAT such that A7: x in B . (n + k1) ; B . (n + k1) in { (B . k) where k is Element of NAT : n <= k } by Th1; hence x in (superior_setsequence B) . n by A1, A7, TARSKI:def_4; ::_thesis: verum end; hence ( ex k being Element of NAT st x in B . (n + k) implies x in (superior_setsequence B) . n ) ; ::_thesis: verum end; theorem Th21: :: SETLIM_1:21 for n being Element of NAT for X being set for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_setsequence_B)_._n_=_((inferior_setsequence_B)_._(n_+_1))_/\_(B_._n) let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) A1: (inferior_setsequence B) . n = meet { (B . k1) where k1 is Element of NAT : n <= k1 } by Def2; A2: { (B . k1) where k1 is Element of NAT : n <= k1 } = { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(B . n)} by Th2; A3: (inferior_setsequence B) . (n + 1) = meet { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } by Def2; A4: { (B . k1) where k1 is Element of NAT : n <= k1 } <> {} by Th1; A5: now__::_thesis:_for_x_being_set_st_x_in_(inferior_setsequence_B)_._(n_+_1)_&_x_in_B_._n_holds_ x_in_(inferior_setsequence_B)_._n let x be set ; ::_thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n implies x in (inferior_setsequence B) . n ) assume that A6: x in (inferior_setsequence B) . (n + 1) and A7: x in B . n ; ::_thesis: x in (inferior_setsequence B) . n for Z being set st Z in { (B . k2) where k2 is Element of NAT : n <= k2 } holds x in Z proof let Z be set ; ::_thesis: ( Z in { (B . k2) where k2 is Element of NAT : n <= k2 } implies x in Z ) assume Z in { (B . k1) where k1 is Element of NAT : n <= k1 } ; ::_thesis: x in Z then consider Z1 being set such that A8: ( Z = Z1 & Z1 in { (B . k1) where k1 is Element of NAT : n <= k1 } ) ; consider k11 being Element of NAT such that A9: ( Z1 = B . k11 & n <= k11 ) by A8; now__::_thesis:_(_(_Z1_=_B_._k11_&_n_=_k11_&_x_in_Z1_)_or_(_Z1_=_B_._k11_&_n_+_1_<=_k11_&_x_in_Z1_)_) percases ( ( Z1 = B . k11 & n = k11 ) or ( Z1 = B . k11 & n + 1 <= k11 ) ) by A9, Lm1; case ( Z1 = B . k11 & n = k11 ) ; ::_thesis: x in Z1 hence x in Z1 by A7; ::_thesis: verum end; case ( Z1 = B . k11 & n + 1 <= k11 ) ; ::_thesis: x in Z1 then Z1 in { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } ; hence x in Z1 by A3, A6, SETFAM_1:def_1; ::_thesis: verum end; end; end; hence x in Z by A8; ::_thesis: verum end; then x in meet { (B . k2) where k2 is Element of NAT : n <= k2 } by A4, SETFAM_1:def_1; hence x in (inferior_setsequence B) . n by Def2; ::_thesis: verum end; { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } <> {} by Th1; then A10: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by A1, A3, A2, SETFAM_1:6, XBOOLE_1:7; now__::_thesis:_for_x_being_set_st_x_in_(inferior_setsequence_B)_._n_holds_ (_x_in_(inferior_setsequence_B)_._(n_+_1)_&_x_in_B_._n_) let x be set ; ::_thesis: ( x in (inferior_setsequence B) . n implies ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) ) A11: B . n in { (B . k1) where k1 is Element of NAT : n <= k1 } ; assume x in (inferior_setsequence B) . n ; ::_thesis: ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) hence ( x in (inferior_setsequence B) . (n + 1) & x in B . n ) by A1, A10, A11, SETFAM_1:def_1; ::_thesis: verum end; hence (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by A5, XBOOLE_0:def_4; ::_thesis: verum end; hence (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) ; ::_thesis: verum end; theorem Th22: :: SETLIM_1:22 for n being Element of NAT for X being set for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_setsequence_B)_._n_=_((superior_setsequence_B)_._(n_+_1))_\/_(B_._n) let n be Element of NAT ; ::_thesis: (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) { (B . k1) where k1 is Element of NAT : n <= k1 } = { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } \/ {(B . n)} by Th2; then union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } c= union { (B . k1) where k1 is Element of NAT : n <= k1 } by XBOOLE_1:7, ZFMISC_1:77; then (superior_setsequence B) . (n + 1) c= union { (B . k1) where k1 is Element of NAT : n <= k1 } by Def3; then A1: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by Def3; A2: now__::_thesis:_for_x_being_set_st_(_x_in_(superior_setsequence_B)_._(n_+_1)_or_x_in_B_._n_)_holds_ x_in_(superior_setsequence_B)_._n let x be set ; ::_thesis: ( ( x in (superior_setsequence B) . (n + 1) or x in B . n ) implies x in (superior_setsequence B) . n ) assume A3: ( x in (superior_setsequence B) . (n + 1) or x in B . n ) ; ::_thesis: x in (superior_setsequence B) . n thus x in (superior_setsequence B) . n ::_thesis: verum proof now__::_thesis:_(_(_x_in_(superior_setsequence_B)_._(n_+_1)_&_x_in_(superior_setsequence_B)_._n_)_or_(_x_in_B_._n_&_x_in_(superior_setsequence_B)_._n_)_) percases ( x in (superior_setsequence B) . (n + 1) or x in B . n ) by A3; case x in (superior_setsequence B) . (n + 1) ; ::_thesis: x in (superior_setsequence B) . n hence x in (superior_setsequence B) . n by A1; ::_thesis: verum end; caseA4: x in B . n ; ::_thesis: x in (superior_setsequence B) . n B . n in { (B . k1) where k1 is Element of NAT : n <= k1 } ; then x in union { (B . k1) where k1 is Element of NAT : n <= k1 } by A4, TARSKI:def_4; hence x in (superior_setsequence B) . n by Def3; ::_thesis: verum end; end; end; hence x in (superior_setsequence B) . n ; ::_thesis: verum end; end; now__::_thesis:_for_x_being_set_holds_ (_not_x_in_(superior_setsequence_B)_._n_or_x_in_B_._n_or_x_in_(superior_setsequence_B)_._(n_+_1)_) let x be set ; ::_thesis: ( not x in (superior_setsequence B) . n or x in B . n or x in (superior_setsequence B) . (n + 1) ) assume x in (superior_setsequence B) . n ; ::_thesis: ( x in B . n or x in (superior_setsequence B) . (n + 1) ) then x in union { (B . k1) where k1 is Element of NAT : n <= k1 } by Def3; then consider Y1 being set such that A5: ( x in Y1 & Y1 in { (B . k1) where k1 is Element of NAT : n <= k1 } ) by TARSKI:def_4; consider k11 being Element of NAT such that A6: ( Y1 = B . k11 & n <= k11 ) by A5; now__::_thesis:_(_(_Y1_=_B_._k11_&_n_=_k11_&_x_in_B_._n_)_or_(_Y1_=_B_._k11_&_n_+_1_<=_k11_&_x_in_union__{__(B_._k2)_where_k2_is_Element_of_NAT_:_n_+_1_<=_k2__}__)_) percases ( ( Y1 = B . k11 & n = k11 ) or ( Y1 = B . k11 & n + 1 <= k11 ) ) by A6, Lm1; case ( Y1 = B . k11 & n = k11 ) ; ::_thesis: x in B . n hence x in B . n by A5; ::_thesis: verum end; case ( Y1 = B . k11 & n + 1 <= k11 ) ; ::_thesis: x in union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } then Y1 in { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } ; hence x in union { (B . k2) where k2 is Element of NAT : n + 1 <= k2 } by A5, TARSKI:def_4; ::_thesis: verum end; end; end; hence ( x in B . n or x in (superior_setsequence B) . (n + 1) ) by Def3; ::_thesis: verum end; then for x being set holds ( x in (superior_setsequence B) . n iff ( x in B . n or x in (superior_setsequence B) . (n + 1) ) ) by A2; hence (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by XBOOLE_0:def_3; ::_thesis: verum end; hence (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) ; ::_thesis: verum end; theorem Th23: :: SETLIM_1:23 for X being set for B being SetSequence of X holds inferior_setsequence B is V50() proof let X be set ; ::_thesis: for B being SetSequence of X holds inferior_setsequence B is V50() let B be SetSequence of X; ::_thesis: inferior_setsequence B is V50() now__::_thesis:_for_n_being_Element_of_NAT_holds_(inferior_setsequence_B)_._n_c=_(inferior_setsequence_B)_._(n_+_1) let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) (inferior_setsequence B) . n = ((inferior_setsequence B) . (n + 1)) /\ (B . n) by Th21; hence (inferior_setsequence B) . n c= (inferior_setsequence B) . (n + 1) by XBOOLE_1:17; ::_thesis: verum end; hence inferior_setsequence B is V50() by PROB_2:7; ::_thesis: verum end; theorem Th24: :: SETLIM_1:24 for X being set for B being SetSequence of X holds superior_setsequence B is V49() proof let X be set ; ::_thesis: for B being SetSequence of X holds superior_setsequence B is V49() let B be SetSequence of X; ::_thesis: superior_setsequence B is V49() now__::_thesis:_for_n_being_Element_of_NAT_holds_(superior_setsequence_B)_._(n_+_1)_c=_(superior_setsequence_B)_._n let n be Element of NAT ; ::_thesis: (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n (superior_setsequence B) . n = ((superior_setsequence B) . (n + 1)) \/ (B . n) by Th22; hence (superior_setsequence B) . (n + 1) c= (superior_setsequence B) . n by XBOOLE_1:7; ::_thesis: verum end; hence superior_setsequence B is V49() by PROB_2:6; ::_thesis: verum end; theorem :: SETLIM_1:25 for X being set for B being SetSequence of X holds ( inferior_setsequence B is monotone & superior_setsequence B is monotone ) proof let X be set ; ::_thesis: for B being SetSequence of X holds ( inferior_setsequence B is monotone & superior_setsequence B is monotone ) let B be SetSequence of X; ::_thesis: ( inferior_setsequence B is monotone & superior_setsequence B is monotone ) inferior_setsequence B is V50() by Th23; hence inferior_setsequence B is monotone by Def1; ::_thesis: superior_setsequence B is monotone superior_setsequence B is V49() by Th24; hence superior_setsequence B is monotone by Def1; ::_thesis: verum end; registration let X be set ; let A be SetSequence of X; cluster inferior_setsequence A -> V50() for SetSequence of X; coherence for b1 being SetSequence of X st b1 = inferior_setsequence A holds b1 is non-descending by Th23; end; registration let X be set ; let A be SetSequence of X; cluster superior_setsequence A -> V49() for SetSequence of X; coherence for b1 being SetSequence of X st b1 = superior_setsequence A holds b1 is non-ascending by Th24; end; theorem :: SETLIM_1:26 for n being Element of NAT for X being set for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= (inferior_setsequence B) . n let B be SetSequence of X; ::_thesis: Intersection B c= (inferior_setsequence B) . n 0 <= n by NAT_1:2; then (inferior_setsequence B) . 0 c= (inferior_setsequence B) . n by PROB_1:def_5; hence Intersection B c= (inferior_setsequence B) . n by Th17; ::_thesis: verum end; theorem :: SETLIM_1:27 for n being Element of NAT for X being set for B being SetSequence of X holds (superior_setsequence B) . n c= Union B proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds (superior_setsequence B) . n c= Union B let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n c= Union B let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n c= Union B 0 <= n by NAT_1:2; then (superior_setsequence B) . n c= (superior_setsequence B) . 0 by PROB_1:def_4; hence (superior_setsequence B) . n c= Union B by Th18; ::_thesis: verum end; theorem Th28: :: SETLIM_1:28 for X being set for B being SetSequence of X for n being Element of NAT holds { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X proof let X be set ; ::_thesis: for B being SetSequence of X for n being Element of NAT holds { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X let B be SetSequence of X; ::_thesis: for n being Element of NAT holds { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X let n be Element of NAT ; ::_thesis: { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X set Y1 = { (B . k) where k is Element of NAT : n <= k } ; { (B . k) where k is Element of NAT : n <= k } c= bool X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (B . k) where k is Element of NAT : n <= k } or x in bool X ) assume x in { (B . k) where k is Element of NAT : n <= k } ; ::_thesis: x in bool X then ex k being Element of NAT st ( x = B . k & n <= k ) ; hence x in bool X ; ::_thesis: verum end; hence { (B . k) where k is Element of NAT : n <= k } is Subset-Family of X ; ::_thesis: verum end; theorem :: SETLIM_1:29 for X being set for B being SetSequence of X holds Union B = (Intersection (Complement B)) ` proof let X be set ; ::_thesis: for B being SetSequence of X holds Union B = (Intersection (Complement B)) ` let B be SetSequence of X; ::_thesis: Union B = (Intersection (Complement B)) ` (Intersection (Complement B)) ` = ((Union (Complement (Complement B))) `) ` by PROB_1:def_3 .= Union B ; hence Union B = (Intersection (Complement B)) ` ; ::_thesis: verum end; theorem Th30: :: SETLIM_1:30 for n being Element of NAT for X being set for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` let X be set ; ::_thesis: for B being SetSequence of X holds (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` let B be SetSequence of X; ::_thesis: (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` set Y1 = { (B . k1) where k1 is Element of NAT : n <= k1 } ; set Y2 = { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } ; set Y3 = { ((B . k) `) where k is Element of NAT : n <= k } ; A1: { ((B . k) `) where k is Element of NAT : n <= k } c= { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { ((B . k) `) where k is Element of NAT : n <= k } or y in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } ) assume y in { ((B . k) `) where k is Element of NAT : n <= k } ; ::_thesis: y in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } then consider k being Element of NAT such that A2: y = (B . k) ` and A3: n <= k ; y = (Complement B) . k by A2, PROB_1:def_2; hence y in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } by A3; ::_thesis: verum end; { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } c= { ((B . k) `) where k is Element of NAT : n <= k } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } or x in { ((B . k) `) where k is Element of NAT : n <= k } ) assume x in { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } ; ::_thesis: x in { ((B . k) `) where k is Element of NAT : n <= k } then consider k being Element of NAT such that A4: x = (Complement B) . k and A5: n <= k ; x = (B . k) ` by A4, PROB_1:def_2; hence x in { ((B . k) `) where k is Element of NAT : n <= k } by A5; ::_thesis: verum end; then A6: { ((Complement B) . k2) where k2 is Element of NAT : n <= k2 } = { ((B . k) `) where k is Element of NAT : n <= k } by A1, XBOOLE_0:def_10; A7: { (B . k1) where k1 is Element of NAT : n <= k1 } <> {} by Th1; reconsider Y1 = { (B . k1) where k1 is Element of NAT : n <= k1 } as Subset-Family of X by Th28; A8: COMPLEMENT Y1 c= { ((B . k) `) where k is Element of NAT : n <= k } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in COMPLEMENT Y1 or y in { ((B . k) `) where k is Element of NAT : n <= k } ) assume A9: y in COMPLEMENT Y1 ; ::_thesis: y in { ((B . k) `) where k is Element of NAT : n <= k } then reconsider y = y as Subset of X ; y ` in Y1 by A9, SETFAM_1:def_7; then consider k being Element of NAT such that A10: y ` = B . k and A11: n <= k ; y = (B . k) ` by A10; hence y in { ((B . k) `) where k is Element of NAT : n <= k } by A11; ::_thesis: verum end; { ((B . k) `) where k is Element of NAT : n <= k } c= COMPLEMENT Y1 proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((B . k) `) where k is Element of NAT : n <= k } or x in COMPLEMENT Y1 ) assume x in { ((B . k) `) where k is Element of NAT : n <= k } ; ::_thesis: x in COMPLEMENT Y1 then consider k being Element of NAT such that A12: x = (B . k) ` and A13: n <= k ; reconsider z = B . k as Subset of X ; (z `) ` in Y1 by A13; hence x in COMPLEMENT Y1 by A12, SETFAM_1:def_7; ::_thesis: verum end; then { ((B . k) `) where k is Element of NAT : n <= k } = COMPLEMENT Y1 by A8, XBOOLE_0:def_10; then (superior_setsequence (Complement B)) . n = union (COMPLEMENT Y1) by A6, Def3 .= ([#] X) \ (meet Y1) by A7, SETFAM_1:34 .= (meet Y1) ` ; hence (inferior_setsequence B) . n = ((superior_setsequence (Complement B)) . n) ` by Def2; ::_thesis: verum end; theorem :: SETLIM_1:31 for n being Element of NAT for X being set for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` let X be set ; ::_thesis: for B being SetSequence of X holds (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` let B be SetSequence of X; ::_thesis: (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` reconsider Y = (inferior_setsequence (Complement B)) . n as Subset of X ; Y = ((superior_setsequence (Complement (Complement B))) . n) ` by Th30 .= ((superior_setsequence B) . n) ` ; hence (superior_setsequence B) . n = ((inferior_setsequence (Complement B)) . n) ` ; ::_thesis: verum end; theorem Th32: :: SETLIM_1:32 for X being set for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B) proof let X be set ; ::_thesis: for B being SetSequence of X holds Complement (inferior_setsequence B) = superior_setsequence (Complement B) let B be SetSequence of X; ::_thesis: Complement (inferior_setsequence B) = superior_setsequence (Complement B) reconsider A2 = inferior_setsequence B as SetSequence of X ; reconsider A3 = superior_setsequence (Complement B) as SetSequence of X ; now__::_thesis:_for_n_being_Element_of_NAT_holds_(Complement_A2)_._n_=_A3_._n let n be Element of NAT ; ::_thesis: (Complement A2) . n = A3 . n (A2 . n) ` = ((A3 . n) `) ` by Th30; hence (Complement A2) . n = A3 . n by PROB_1:def_2; ::_thesis: verum end; hence Complement (inferior_setsequence B) = superior_setsequence (Complement B) by FUNCT_2:63; ::_thesis: verum end; theorem :: SETLIM_1:33 for X being set for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B) proof let X be set ; ::_thesis: for B being SetSequence of X holds Complement (superior_setsequence B) = inferior_setsequence (Complement B) let B be SetSequence of X; ::_thesis: Complement (superior_setsequence B) = inferior_setsequence (Complement B) reconsider A2 = inferior_setsequence (Complement B) as SetSequence of X ; Complement A2 = superior_setsequence (Complement (Complement B)) by Th32 .= superior_setsequence B ; hence Complement (superior_setsequence B) = inferior_setsequence (Complement B) ; ::_thesis: verum end; theorem :: SETLIM_1:34 for X being set for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n proof let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n ) assume A1: for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: for n being Element of NAT holds ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n let n be Element of NAT ; ::_thesis: ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n set X1 = inferior_setsequence A1; set X2 = inferior_setsequence A2; set X3 = inferior_setsequence A3; now__::_thesis:_for_x_being_set_st_x_in_((inferior_setsequence_A1)_._n)_\/_((inferior_setsequence_A2)_._n)_holds_ x_in_(inferior_setsequence_A3)_._n let x be set ; ::_thesis: ( x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) implies b1 in (inferior_setsequence A3) . n ) assume A2: x in ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) ; ::_thesis: b1 in (inferior_setsequence A3) . n percases ( x in (inferior_setsequence A1) . n or x in (inferior_setsequence A2) . n ) by A2, XBOOLE_0:def_3; supposeA3: x in (inferior_setsequence A1) . n ; ::_thesis: b1 in (inferior_setsequence A3) . n now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k) let k be Element of NAT ; ::_thesis: x in A3 . (n + k) ( x in A1 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A3, Th19; hence x in A3 . (n + k) by XBOOLE_0:def_3; ::_thesis: verum end; hence x in (inferior_setsequence A3) . n by Th19; ::_thesis: verum end; supposeA4: x in (inferior_setsequence A2) . n ; ::_thesis: b1 in (inferior_setsequence A3) . n now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k) let k be Element of NAT ; ::_thesis: x in A3 . (n + k) ( x in A2 . (n + k) & A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) ) by A1, A4, Th19; hence x in A3 . (n + k) by XBOOLE_0:def_3; ::_thesis: verum end; hence x in (inferior_setsequence A3) . n by Th19; ::_thesis: verum end; end; end; hence ((inferior_setsequence A1) . n) \/ ((inferior_setsequence A2) . n) c= (inferior_setsequence A3) . n by TARSKI:def_3; ::_thesis: verum end; theorem :: SETLIM_1:35 for X being set for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) proof let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) implies for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) ) assume A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: for n being Element of NAT holds (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) let n be Element of NAT ; ::_thesis: (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) reconsider X3 = inferior_setsequence A3 as SetSequence of X ; reconsider X2 = inferior_setsequence A2 as SetSequence of X ; set B = A1; reconsider X1 = inferior_setsequence A1 as SetSequence of X ; A2: (X1 . n) /\ (X2 . n) c= X3 . n proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X1 . n) /\ (X2 . n) or x in X3 . n ) assume x in (X1 . n) /\ (X2 . n) ; ::_thesis: x in X3 . n then A3: ( x in X1 . n & x in X2 . n ) by XBOOLE_0:def_4; now__::_thesis:_for_k_being_Element_of_NAT_holds_x_in_A3_._(n_+_k) let k be Element of NAT ; ::_thesis: x in A3 . (n + k) ( x in A1 . (n + k) & x in A2 . (n + k) ) by A3, Th19; then x in (A1 . (n + k)) /\ (A2 . (n + k)) by XBOOLE_0:def_4; hence x in A3 . (n + k) by A1; ::_thesis: verum end; hence x in X3 . n by Th19; ::_thesis: verum end; X3 . n c= (X1 . n) /\ (X2 . n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) /\ (X2 . n) ) assume A4: x in X3 . n ; ::_thesis: x in (X1 . n) /\ (X2 . n) now__::_thesis:_for_k_being_Element_of_NAT_holds_ (_x_in_A1_._(n_+_k)_&_x_in_A2_._(n_+_k)_) let k be Element of NAT ; ::_thesis: ( x in A1 . (n + k) & x in A2 . (n + k) ) x in A3 . (n + k) by A4, Th19; then x in (A1 . (n + k)) /\ (A2 . (n + k)) by A1; hence ( x in A1 . (n + k) & x in A2 . (n + k) ) by XBOOLE_0:def_4; ::_thesis: verum end; then ( x in X1 . n & x in X2 . n ) by Th19; hence x in (X1 . n) /\ (X2 . n) by XBOOLE_0:def_4; ::_thesis: verum end; hence (inferior_setsequence A3) . n = ((inferior_setsequence A1) . n) /\ ((inferior_setsequence A2) . n) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: SETLIM_1:36 for X being set for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) proof let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) holds for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ) implies for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) ) assume A1: for n being Element of NAT holds A3 . n = (A1 . n) \/ (A2 . n) ; ::_thesis: for n being Element of NAT holds (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) let n be Element of NAT ; ::_thesis: (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) reconsider X3 = superior_setsequence A3 as SetSequence of X ; reconsider X2 = superior_setsequence A2 as SetSequence of X ; set B = A1; reconsider X1 = superior_setsequence A1 as SetSequence of X ; A2: (X1 . n) \/ (X2 . n) c= X3 . n proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (X1 . n) \/ (X2 . n) or x in X3 . n ) assume A3: x in (X1 . n) \/ (X2 . n) ; ::_thesis: x in X3 . n now__::_thesis:_(_(_x_in_X1_._n_&_x_in_X3_._n_)_or_(_x_in_X2_._n_&_x_in_X3_._n_)_) percases ( x in X1 . n or x in X2 . n ) by A3, XBOOLE_0:def_3; case x in X1 . n ; ::_thesis: x in X3 . n then consider k being Element of NAT such that A4: x in A1 . (n + k) by Th20; A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1; then x in A3 . (n + k) by A4, XBOOLE_0:def_3; hence x in X3 . n by Th20; ::_thesis: verum end; case x in X2 . n ; ::_thesis: x in X3 . n then consider k being Element of NAT such that A5: x in A2 . (n + k) by Th20; A3 . (n + k) = (A1 . (n + k)) \/ (A2 . (n + k)) by A1; then x in A3 . (n + k) by A5, XBOOLE_0:def_3; hence x in X3 . n by Th20; ::_thesis: verum end; end; end; hence x in X3 . n ; ::_thesis: verum end; X3 . n c= (X1 . n) \/ (X2 . n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) \/ (X2 . n) ) assume x in X3 . n ; ::_thesis: x in (X1 . n) \/ (X2 . n) then consider k being Element of NAT such that A6: x in A3 . (n + k) by Th20; A7: x in (A1 . (n + k)) \/ (A2 . (n + k)) by A1, A6; now__::_thesis:_(_(_x_in_A1_._(n_+_k)_&_x_in_X1_._n_)_or_(_x_in_A2_._(n_+_k)_&_x_in_X2_._n_)_) percases ( x in A1 . (n + k) or x in A2 . (n + k) ) by A7, XBOOLE_0:def_3; case x in A1 . (n + k) ; ::_thesis: x in X1 . n hence x in X1 . n by Th20; ::_thesis: verum end; case x in A2 . (n + k) ; ::_thesis: x in X2 . n hence x in X2 . n by Th20; ::_thesis: verum end; end; end; hence x in (X1 . n) \/ (X2 . n) by XBOOLE_0:def_3; ::_thesis: verum end; hence (superior_setsequence A3) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) by A2, XBOOLE_0:def_10; ::_thesis: verum end; theorem :: SETLIM_1:37 for X being set for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) proof let X be set ; ::_thesis: for A3, A1, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) holds for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) let A3, A1, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ) implies for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) ) assume A1: for n being Element of NAT holds A3 . n = (A1 . n) /\ (A2 . n) ; ::_thesis: for n being Element of NAT holds (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) let n be Element of NAT ; ::_thesis: (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) reconsider X3 = superior_setsequence A3 as SetSequence of X ; reconsider X2 = superior_setsequence A2 as SetSequence of X ; set B = A1; reconsider X1 = superior_setsequence A1 as SetSequence of X ; X3 . n c= (X1 . n) /\ (X2 . n) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X3 . n or x in (X1 . n) /\ (X2 . n) ) assume x in X3 . n ; ::_thesis: x in (X1 . n) /\ (X2 . n) then consider k being Element of NAT such that A2: x in A3 . (n + k) by Th20; A3: A3 . (n + k) = (A1 . (n + k)) /\ (A2 . (n + k)) by A1; then x in A2 . (n + k) by A2, XBOOLE_0:def_4; then A4: x in X2 . n by Th20; x in A1 . (n + k) by A2, A3, XBOOLE_0:def_4; then x in X1 . n by Th20; hence x in (X1 . n) /\ (X2 . n) by A4, XBOOLE_0:def_4; ::_thesis: verum end; hence (superior_setsequence A3) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) ; ::_thesis: verum end; theorem Th38: :: SETLIM_1:38 for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (inferior_setsequence B) . n = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (inferior_setsequence B) . n = A let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (inferior_setsequence B) . n = A let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds (inferior_setsequence B) . n = A ) assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds (inferior_setsequence B) . n = A let n be Element of NAT ; ::_thesis: (inferior_setsequence B) . n = A (inferior_setsequence B) . n = meet { (B . k) where k is Element of NAT : n <= k } by Def2; hence (inferior_setsequence B) . n = A by A1, Th14; ::_thesis: verum end; theorem Th39: :: SETLIM_1:39 for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (superior_setsequence B) . n = A proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (superior_setsequence B) . n = A let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds for n being Element of NAT holds (superior_setsequence B) . n = A let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies for n being Element of NAT holds (superior_setsequence B) . n = A ) assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: for n being Element of NAT holds (superior_setsequence B) . n = A let n be Element of NAT ; ::_thesis: (superior_setsequence B) . n = A (superior_setsequence B) . n = union { (B . k) where k is Element of NAT : n <= k } by Def3; hence (superior_setsequence B) . n = A by A1, Th13; ::_thesis: verum end; theorem Th40: :: SETLIM_1:40 for n being Element of NAT for X being set for B being SetSequence of X st B is V50() holds B . n c= (superior_setsequence B) . (n + 1) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V50() holds B . n c= (superior_setsequence B) . (n + 1) let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds B . n c= (superior_setsequence B) . (n + 1) let B be SetSequence of X; ::_thesis: ( B is V50() implies B . n c= (superior_setsequence B) . (n + 1) ) assume B is V50() ; ::_thesis: B . n c= (superior_setsequence B) . (n + 1) then A1: B . n c= B . (n + 1) by PROB_2:7; B . n c= union { (B . k) where k is Element of NAT : n + 1 <= k } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B . n or x in union { (B . k) where k is Element of NAT : n + 1 <= k } ) A2: B . (n + 1) in { (B . k) where k is Element of NAT : n + 1 <= k } ; assume x in B . n ; ::_thesis: x in union { (B . k) where k is Element of NAT : n + 1 <= k } hence x in union { (B . k) where k is Element of NAT : n + 1 <= k } by A1, A2, TARSKI:def_4; ::_thesis: verum end; hence B . n c= (superior_setsequence B) . (n + 1) by Def3; ::_thesis: verum end; theorem Th41: :: SETLIM_1:41 for n being Element of NAT for X being set for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) let B be SetSequence of X; ::_thesis: ( B is V50() implies (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) ) assume B is V50() ; ::_thesis: (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) then ((superior_setsequence B) . (n + 1)) \/ (B . n) = (superior_setsequence B) . (n + 1) by Th40, XBOOLE_1:12; hence (superior_setsequence B) . n = (superior_setsequence B) . (n + 1) by Th22; ::_thesis: verum end; theorem Th42: :: SETLIM_1:42 for n being Element of NAT for X being set for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = Union B proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = Union B let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds (superior_setsequence B) . n = Union B let B be SetSequence of X; ::_thesis: ( B is V50() implies (superior_setsequence B) . n = Union B ) defpred S1[ Nat] means (superior_setsequence B) . \$1 = Union B; assume B is V50() ; ::_thesis: (superior_setsequence B) . n = Union B then A1: for k being Element of NAT st S1[k] holds S1[k + 1] by Th41; A2: S1[ 0 ] by Th18; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); hence (superior_setsequence B) . n = Union B ; ::_thesis: verum end; theorem Th43: :: SETLIM_1:43 for X being set for B being SetSequence of X st B is V50() holds Intersection (superior_setsequence B) = Union B proof let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds Intersection (superior_setsequence B) = Union B let B be SetSequence of X; ::_thesis: ( B is V50() implies Intersection (superior_setsequence B) = Union B ) assume A1: B is V50() ; ::_thesis: Intersection (superior_setsequence B) = Union B now__::_thesis:_for_x_being_set_st_x_in_Intersection_(superior_setsequence_B)_holds_ x_in_Union_B let x be set ; ::_thesis: ( x in Intersection (superior_setsequence B) implies x in Union B ) assume A2: x in Intersection (superior_setsequence B) ; ::_thesis: x in Union B now__::_thesis:_for_n_being_Element_of_NAT_holds_x_in_Union_B let n be Element of NAT ; ::_thesis: x in Union B (superior_setsequence B) . n = Union B by A1, Th42; hence x in Union B by A2, PROB_1:13; ::_thesis: verum end; hence x in Union B ; ::_thesis: verum end; then A3: Intersection (superior_setsequence B) c= Union B by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_Union_B_holds_ y_in_Intersection_(superior_setsequence_B) let y be set ; ::_thesis: ( y in Union B implies y in Intersection (superior_setsequence B) ) assume y in Union B ; ::_thesis: y in Intersection (superior_setsequence B) then for n being Element of NAT holds y in (superior_setsequence B) . n by A1, Th42; hence y in Intersection (superior_setsequence B) by PROB_1:13; ::_thesis: verum end; then Union B c= Intersection (superior_setsequence B) by TARSKI:def_3; hence Intersection (superior_setsequence B) = Union B by A3, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th44: :: SETLIM_1:44 for n being Element of NAT for X being set for B being SetSequence of X st B is V50() holds B . n c= (inferior_setsequence B) . (n + 1) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V50() holds B . n c= (inferior_setsequence B) . (n + 1) let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds B . n c= (inferior_setsequence B) . (n + 1) let B be SetSequence of X; ::_thesis: ( B is V50() implies B . n c= (inferior_setsequence B) . (n + 1) ) set Y = { (B . k) where k is Element of NAT : n + 1 <= k } ; assume A1: B is V50() ; ::_thesis: B . n c= (inferior_setsequence B) . (n + 1) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in B . n or x in (inferior_setsequence B) . (n + 1) ) assume A2: x in B . n ; ::_thesis: x in (inferior_setsequence B) . (n + 1) A3: now__::_thesis:_for_y_being_set_st_y_in__{__(B_._k)_where_k_is_Element_of_NAT_:_n_+_1_<=_k__}__holds_ x_in_y let y be set ; ::_thesis: ( y in { (B . k) where k is Element of NAT : n + 1 <= k } implies x in y ) assume y in { (B . k) where k is Element of NAT : n + 1 <= k } ; ::_thesis: x in y then consider k1 being Element of NAT such that A4: y = B . k1 and A5: n + 1 <= k1 ; n <= k1 by A5, NAT_1:13; then B . n c= B . k1 by A1, PROB_1:def_5; hence x in y by A2, A4; ::_thesis: verum end; A6: { (B . k) where k is Element of NAT : n + 1 <= k } <> {} by Th1; (inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Element of NAT : n + 1 <= k } by Def2; hence x in (inferior_setsequence B) . (n + 1) by A6, A3, SETFAM_1:def_1; ::_thesis: verum end; theorem Th45: :: SETLIM_1:45 for n being Element of NAT for X being set for B being SetSequence of X st B is V50() holds (inferior_setsequence B) . n = B . n proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V50() holds (inferior_setsequence B) . n = B . n let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds (inferior_setsequence B) . n = B . n let B be SetSequence of X; ::_thesis: ( B is V50() implies (inferior_setsequence B) . n = B . n ) assume B is V50() ; ::_thesis: (inferior_setsequence B) . n = B . n then ((inferior_setsequence B) . (n + 1)) /\ (B . n) = B . n by Th44, XBOOLE_1:28; hence (inferior_setsequence B) . n = B . n by Th21; ::_thesis: verum end; theorem Th46: :: SETLIM_1:46 for X being set for B being SetSequence of X st B is V50() holds inferior_setsequence B = B proof let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds inferior_setsequence B = B let B be SetSequence of X; ::_thesis: ( B is V50() implies inferior_setsequence B = B ) assume B is V50() ; ::_thesis: inferior_setsequence B = B then for n being Element of NAT holds (inferior_setsequence B) . n = B . n by Th45; hence inferior_setsequence B = B by FUNCT_2:63; ::_thesis: verum end; theorem Th47: :: SETLIM_1:47 for n being Element of NAT for X being set for B being SetSequence of X st B is V49() holds (superior_setsequence B) . (n + 1) c= B . n proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V49() holds (superior_setsequence B) . (n + 1) c= B . n let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds (superior_setsequence B) . (n + 1) c= B . n let B be SetSequence of X; ::_thesis: ( B is V49() implies (superior_setsequence B) . (n + 1) c= B . n ) assume A1: B is V49() ; ::_thesis: (superior_setsequence B) . (n + 1) c= B . n let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (superior_setsequence B) . (n + 1) or x in B . n ) assume x in (superior_setsequence B) . (n + 1) ; ::_thesis: x in B . n then consider k being Element of NAT such that A2: x in B . ((n + 1) + k) by Th20; n + 1 <= (n + 1) + k by NAT_1:11; then n <= (n + 1) + k by NAT_1:13; then B . ((n + 1) + k) c= B . n by A1, PROB_1:def_4; hence x in B . n by A2; ::_thesis: verum end; theorem Th48: :: SETLIM_1:48 for n being Element of NAT for X being set for B being SetSequence of X st B is V49() holds (superior_setsequence B) . n = B . n proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V49() holds (superior_setsequence B) . n = B . n let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds (superior_setsequence B) . n = B . n let B be SetSequence of X; ::_thesis: ( B is V49() implies (superior_setsequence B) . n = B . n ) assume B is V49() ; ::_thesis: (superior_setsequence B) . n = B . n then ((superior_setsequence B) . (n + 1)) \/ (B . n) = B . n by Th47, XBOOLE_1:12; hence (superior_setsequence B) . n = B . n by Th22; ::_thesis: verum end; theorem Th49: :: SETLIM_1:49 for X being set for B being SetSequence of X st B is V49() holds superior_setsequence B = B proof let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds superior_setsequence B = B let B be SetSequence of X; ::_thesis: ( B is V49() implies superior_setsequence B = B ) assume B is V49() ; ::_thesis: superior_setsequence B = B then for n being Element of NAT holds (superior_setsequence B) . n = B . n by Th48; hence superior_setsequence B = B by FUNCT_2:63; ::_thesis: verum end; theorem Th50: :: SETLIM_1:50 for n being Element of NAT for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . (n + 1) c= B . n proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . (n + 1) c= B . n let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . (n + 1) c= B . n let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . (n + 1) c= B . n ) set Y = { (B . k) where k is Element of NAT : n + 1 <= k } ; assume B is V49() ; ::_thesis: (inferior_setsequence B) . (n + 1) c= B . n then A1: B . (n + 1) c= B . n by PROB_2:6; A2: B . (n + 1) in { (B . k) where k is Element of NAT : n + 1 <= k } ; A3: now__::_thesis:_for_x_being_set_st_x_in_meet__{__(B_._k)_where_k_is_Element_of_NAT_:_n_+_1_<=_k__}__holds_ x_in_B_._n let x be set ; ::_thesis: ( x in meet { (B . k) where k is Element of NAT : n + 1 <= k } implies x in B . n ) assume x in meet { (B . k) where k is Element of NAT : n + 1 <= k } ; ::_thesis: x in B . n then x in B . (n + 1) by A2, SETFAM_1:def_1; hence x in B . n by A1; ::_thesis: verum end; (inferior_setsequence B) . (n + 1) = meet { (B . k) where k is Element of NAT : n + 1 <= k } by Def2; hence (inferior_setsequence B) . (n + 1) c= B . n by A3, TARSKI:def_3; ::_thesis: verum end; theorem Th51: :: SETLIM_1:51 for n being Element of NAT for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) ) assume B is V49() ; ::_thesis: (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) then ((inferior_setsequence B) . (n + 1)) /\ (B . n) = (inferior_setsequence B) . (n + 1) by Th50, XBOOLE_1:28; hence (inferior_setsequence B) . n = (inferior_setsequence B) . (n + 1) by Th21; ::_thesis: verum end; theorem Th52: :: SETLIM_1:52 for n being Element of NAT for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = Intersection B proof let n be Element of NAT ; ::_thesis: for X being set for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = Intersection B let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds (inferior_setsequence B) . n = Intersection B let B be SetSequence of X; ::_thesis: ( B is V49() implies (inferior_setsequence B) . n = Intersection B ) defpred S1[ Nat] means (inferior_setsequence B) . \$1 = Intersection B; assume B is V49() ; ::_thesis: (inferior_setsequence B) . n = Intersection B then A1: for k being Element of NAT st S1[k] holds S1[k + 1] by Th51; A2: S1[ 0 ] by Th17; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A2, A1); hence (inferior_setsequence B) . n = Intersection B ; ::_thesis: verum end; theorem Th53: :: SETLIM_1:53 for X being set for B being SetSequence of X st B is V49() holds Union (inferior_setsequence B) = Intersection B proof let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds Union (inferior_setsequence B) = Intersection B let B be SetSequence of X; ::_thesis: ( B is V49() implies Union (inferior_setsequence B) = Intersection B ) assume A1: B is V49() ; ::_thesis: Union (inferior_setsequence B) = Intersection B now__::_thesis:_for_x_being_set_st_x_in_Union_(inferior_setsequence_B)_holds_ x_in_Intersection_B let x be set ; ::_thesis: ( x in Union (inferior_setsequence B) implies x in Intersection B ) assume x in Union (inferior_setsequence B) ; ::_thesis: x in Intersection B then ex k being Element of NAT st x in (inferior_setsequence B) . k by PROB_1:12; hence x in Intersection B by A1, Th52; ::_thesis: verum end; then A2: Union (inferior_setsequence B) c= Intersection B by TARSKI:def_3; now__::_thesis:_for_y_being_set_st_y_in_Intersection_B_holds_ y_in_Union_(inferior_setsequence_B) let y be set ; ::_thesis: ( y in Intersection B implies y in Union (inferior_setsequence B) ) assume y in Intersection B ; ::_thesis: y in Union (inferior_setsequence B) then y in (inferior_setsequence B) . 0 by Th17; hence y in Union (inferior_setsequence B) by PROB_1:12; ::_thesis: verum end; then Intersection B c= Union (inferior_setsequence B) by TARSKI:def_3; hence Union (inferior_setsequence B) = Intersection B by A2, XBOOLE_0:def_10; ::_thesis: verum end; definition let X be set ; let B be SetSequence of X; redefine func lim_inf B equals :: SETLIM_1:def 4 Union (inferior_setsequence B); compatibility for b1 being Element of bool X holds ( b1 = lim_inf B iff b1 = Union (inferior_setsequence B) ) proof let F be Subset of X; ::_thesis: ( F = lim_inf B iff F = Union (inferior_setsequence B) ) hereby ::_thesis: ( F = Union (inferior_setsequence B) implies F = lim_inf B ) assume A1: F = lim_inf B ; ::_thesis: F = Union (inferior_setsequence B) for x being set holds ( x in F iff x in Union (inferior_setsequence B) ) proof let x be set ; ::_thesis: ( x in F iff x in Union (inferior_setsequence B) ) hereby ::_thesis: ( x in Union (inferior_setsequence B) implies x in F ) assume x in F ; ::_thesis: x in Union (inferior_setsequence B) then consider n being Element of NAT such that A2: for k being Element of NAT holds x in B . (n + k) by A1, KURATO_0:4; x in (inferior_setsequence B) . n by A2, Th19; hence x in Union (inferior_setsequence B) by PROB_1:12; ::_thesis: verum end; assume x in Union (inferior_setsequence B) ; ::_thesis: x in F then consider n being Element of NAT such that A3: x in (inferior_setsequence B) . n by PROB_1:12; for k being Element of NAT holds x in B . (n + k) by A3, Th19; hence x in F by A1, KURATO_0:4; ::_thesis: verum end; hence F = Union (inferior_setsequence B) by TARSKI:1; ::_thesis: verum end; assume A4: F = Union (inferior_setsequence B) ; ::_thesis: F = lim_inf B for x being set holds ( x in F iff x in lim_inf B ) proof let x be set ; ::_thesis: ( x in F iff x in lim_inf B ) hereby ::_thesis: ( x in lim_inf B implies x in F ) assume x in F ; ::_thesis: x in lim_inf B then consider n being Element of NAT such that A5: x in (inferior_setsequence B) . n by A4, PROB_1:12; for k being Element of NAT holds x in B . (n + k) by A5, Th19; hence x in lim_inf B by KURATO_0:4; ::_thesis: verum end; assume x in lim_inf B ; ::_thesis: x in F then consider n being Element of NAT such that A6: for k being Element of NAT holds x in B . (n + k) by KURATO_0:4; x in (inferior_setsequence B) . n by A6, Th19; hence x in F by A4, PROB_1:12; ::_thesis: verum end; hence F = lim_inf B by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines lim_inf SETLIM_1:def_4_:_ for X being set for B being SetSequence of X holds lim_inf B = Union (inferior_setsequence B); definition let X be set ; let B be SetSequence of X; redefine func lim_sup B equals :: SETLIM_1:def 5 Intersection (superior_setsequence B); compatibility for b1 being Element of bool X holds ( b1 = lim_sup B iff b1 = Intersection (superior_setsequence B) ) proof let F be Subset of X; ::_thesis: ( F = lim_sup B iff F = Intersection (superior_setsequence B) ) hereby ::_thesis: ( F = Intersection (superior_setsequence B) implies F = lim_sup B ) assume A1: F = lim_sup B ; ::_thesis: F = Intersection (superior_setsequence B) for x being set holds ( x in F iff x in Intersection (superior_setsequence B) ) proof let x be set ; ::_thesis: ( x in F iff x in Intersection (superior_setsequence B) ) hereby ::_thesis: ( x in Intersection (superior_setsequence B) implies x in F ) assume A2: x in F ; ::_thesis: x in Intersection (superior_setsequence B) for m being Element of NAT holds x in (superior_setsequence B) . m proof let m be Element of NAT ; ::_thesis: x in (superior_setsequence B) . m ex k being Element of NAT st x in B . (m + k) by A1, A2, KURATO_0:5; hence x in (superior_setsequence B) . m by Th20; ::_thesis: verum end; hence x in Intersection (superior_setsequence B) by PROB_1:13; ::_thesis: verum end; assume A3: x in Intersection (superior_setsequence B) ; ::_thesis: x in F now__::_thesis:_for_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_B_._(m_+_k) let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k) x in (superior_setsequence B) . m by A3, PROB_1:13; hence ex k being Element of NAT st x in B . (m + k) by Th20; ::_thesis: verum end; hence x in F by A1, KURATO_0:5; ::_thesis: verum end; hence F = Intersection (superior_setsequence B) by TARSKI:1; ::_thesis: verum end; assume A4: F = Intersection (superior_setsequence B) ; ::_thesis: F = lim_sup B for x being set holds ( x in F iff x in lim_sup B ) proof let x be set ; ::_thesis: ( x in F iff x in lim_sup B ) hereby ::_thesis: ( x in lim_sup B implies x in F ) assume A5: x in F ; ::_thesis: x in lim_sup B now__::_thesis:_for_m_being_Element_of_NAT_ex_k_being_Element_of_NAT_st_x_in_B_._(m_+_k) let m be Element of NAT ; ::_thesis: ex k being Element of NAT st x in B . (m + k) x in (superior_setsequence B) . m by A4, A5, PROB_1:13; hence ex k being Element of NAT st x in B . (m + k) by Th20; ::_thesis: verum end; hence x in lim_sup B by KURATO_0:5; ::_thesis: verum end; assume A6: x in lim_sup B ; ::_thesis: x in F for m being Element of NAT holds x in (superior_setsequence B) . m proof let m be Element of NAT ; ::_thesis: x in (superior_setsequence B) . m ex k being Element of NAT st x in B . (m + k) by A6, KURATO_0:5; hence x in (superior_setsequence B) . m by Th20; ::_thesis: verum end; hence x in F by A4, PROB_1:13; ::_thesis: verum end; hence F = lim_sup B by TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines lim_sup SETLIM_1:def_5_:_ for X being set for B being SetSequence of X holds lim_sup B = Intersection (superior_setsequence B); notation let X be set ; let B be SetSequence of X; synonym lim B for lim_sup B; end; theorem :: SETLIM_1:54 for X being set for B being SetSequence of X holds Intersection B c= lim_inf B proof let X be set ; ::_thesis: for B being SetSequence of X holds Intersection B c= lim_inf B let B be SetSequence of X; ::_thesis: Intersection B c= lim_inf B let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection B or x in lim_inf B ) assume x in Intersection B ; ::_thesis: x in lim_inf B then for k being Element of NAT holds x in B . (0 + k) by PROB_1:13; hence x in lim_inf B by KURATO_0:4; ::_thesis: verum end; theorem :: SETLIM_1:55 for X being set for B being SetSequence of X holds lim_inf B = lim (inferior_setsequence B) by Th43; theorem :: SETLIM_1:56 for X being set for B being SetSequence of X holds lim_sup B = lim (superior_setsequence B) by Th49; theorem :: SETLIM_1:57 for X being set for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) ` proof let X be set ; ::_thesis: for B being SetSequence of X holds lim_sup B = (lim_inf (Complement B)) ` let B be SetSequence of X; ::_thesis: lim_sup B = (lim_inf (Complement B)) ` lim_inf (Complement B) = (lim_sup (Complement (Complement B))) ` by KURATO_0:9 .= (lim_sup B) ` ; hence lim_sup B = (lim_inf (Complement B)) ` ; ::_thesis: verum end; theorem Th58: :: SETLIM_1:58 for X being set for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) proof let X be set ; ::_thesis: for A being Subset of X for B being SetSequence of X st B is constant & the_value_of B = A holds ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) let A be Subset of X; ::_thesis: for B being SetSequence of X st B is constant & the_value_of B = A holds ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) ) assume A1: ( B is constant & the_value_of B = A ) ; ::_thesis: ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) then for n being Element of NAT holds (superior_setsequence B) . n = A by Th39; then A2: lim_sup B = A by Th11; for n being Element of NAT holds (inferior_setsequence B) . n = A by A1, Th38; then lim_inf B = A by Th10; hence ( B is convergent & lim B = A & lim_inf B = A & lim_sup B = A ) by A2, KURATO_0:def_5; ::_thesis: verum end; theorem :: SETLIM_1:59 for X being set for B being SetSequence of X st B is V50() holds lim_sup B = Union B by Th43; theorem :: SETLIM_1:60 for X being set for B being SetSequence of X st B is V50() holds lim_inf B = Union B by Th46; theorem :: SETLIM_1:61 for X being set for B being SetSequence of X st B is V49() holds lim_sup B = Intersection B by Th49; theorem :: SETLIM_1:62 for X being set for B being SetSequence of X st B is V49() holds lim_inf B = Intersection B by Th53; theorem Th63: :: SETLIM_1:63 for X being set for B being SetSequence of X st B is V50() holds ( B is convergent & lim B = Union B ) proof let X be set ; ::_thesis: for B being SetSequence of X st B is V50() holds ( B is convergent & lim B = Union B ) let B be SetSequence of X; ::_thesis: ( B is V50() implies ( B is convergent & lim B = Union B ) ) assume A1: B is V50() ; ::_thesis: ( B is convergent & lim B = Union B ) then ( lim_sup B = Union B & lim_inf B = Union B ) by Th43, Th46; hence B is convergent by KURATO_0:def_5; ::_thesis: lim B = Union B thus lim B = Union B by A1, Th43; ::_thesis: verum end; theorem Th64: :: SETLIM_1:64 for X being set for B being SetSequence of X st B is V49() holds ( B is convergent & lim B = Intersection B ) proof let X be set ; ::_thesis: for B being SetSequence of X st B is V49() holds ( B is convergent & lim B = Intersection B ) let B be SetSequence of X; ::_thesis: ( B is V49() implies ( B is convergent & lim B = Intersection B ) ) assume A1: B is V49() ; ::_thesis: ( B is convergent & lim B = Intersection B ) then ( lim_sup B = Intersection B & lim_inf B = Intersection B ) by Th49, Th53; hence B is convergent by KURATO_0:def_5; ::_thesis: lim B = Intersection B thus lim B = Intersection B by A1, Th49; ::_thesis: verum end; theorem :: SETLIM_1:65 for X being set for B being SetSequence of X st B is monotone holds B is convergent proof let X be set ; ::_thesis: for B being SetSequence of X st B is monotone holds B is convergent let B be SetSequence of X; ::_thesis: ( B is monotone implies B is convergent ) assume A1: B is monotone ; ::_thesis: B is convergent percases ( not B is V49() or not B is V50() ) by A1, Def1; suppose B is V49() ; ::_thesis: B is convergent hence B is convergent by Th64; ::_thesis: verum end; suppose B is V50() ; ::_thesis: B is convergent hence B is convergent by Th63; ::_thesis: verum end; end; end; definition let X be set ; let Si be SigmaField of X; let S be SetSequence of Si; :: original: inferior_setsequence redefine func inferior_setsequence S -> SetSequence of Si; coherence inferior_setsequence S is SetSequence of Si proof now__::_thesis:_for_n_being_Nat_holds_(inferior_setsequence_S)_._n_in_Si let n be Nat; ::_thesis: (inferior_setsequence S) . n in Si reconsider DSeq = S ^\ n as SetSequence of X ; reconsider n1 = n as Element of NAT by ORDINAL1:def_12; for m being Nat holds DSeq . m in Si proof let m be Nat; ::_thesis: DSeq . m in Si ( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def_3; hence DSeq . m in Si ; ::_thesis: verum end; then rng DSeq c= Si by NAT_1:52; then A1: Intersection DSeq in Si by PROB_1:def_6; Intersection DSeq = meet (rng DSeq) by Th8; then Intersection DSeq = meet { (S . k) where k is Element of NAT : n1 <= k } by Th6; hence (inferior_setsequence S) . n in Si by A1, Def2; ::_thesis: verum end; then rng (inferior_setsequence S) c= Si by NAT_1:52; hence inferior_setsequence S is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum end; end; definition let X be set ; let Si be SigmaField of X; let S be SetSequence of Si; :: original: superior_setsequence redefine func superior_setsequence S -> SetSequence of Si; coherence superior_setsequence S is SetSequence of Si proof now__::_thesis:_for_n_being_Nat_holds_(superior_setsequence_S)_._n_in_Si let n be Nat; ::_thesis: (superior_setsequence S) . n in Si reconsider DSeq = S ^\ n as SetSequence of X ; reconsider n1 = n as Element of NAT by ORDINAL1:def_12; for m being Nat holds DSeq . m in Si proof let m be Nat; ::_thesis: DSeq . m in Si ( DSeq . m = S . (m + n1) & S . (m + n1) in rng S ) by NAT_1:51, NAT_1:def_3; hence DSeq . m in Si ; ::_thesis: verum end; then rng DSeq c= Si by NAT_1:52; then DSeq is SetSequence of Si by RELAT_1:def_19; then A1: Union DSeq in Si by PROB_1:17; Union DSeq = union (rng DSeq) by CARD_3:def_4; then Union DSeq = union { (S . k) where k is Element of NAT : n1 <= k } by Th6; hence (superior_setsequence S) . n in Si by A1, Def3; ::_thesis: verum end; then rng (superior_setsequence S) c= Si by NAT_1:52; hence superior_setsequence S is SetSequence of Si by RELAT_1:def_19; ::_thesis: verum end; end; theorem Th66: :: SETLIM_1:66 for X, x being set for Si being SigmaField of X for S being SetSequence of Si holds ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) proof let X, x be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) let S be SetSequence of Si; ::_thesis: ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) for B being SetSequence of X holds ( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) ) proof let B be SetSequence of X; ::_thesis: ( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) ) lim_sup B = Intersection (superior_setsequence B) ; hence ( x in Intersection (superior_setsequence B) iff for n being Element of NAT ex k being Element of NAT st x in B . (n + k) ) by KURATO_0:5; ::_thesis: verum end; hence ( x in lim_sup S iff for n being Element of NAT ex k being Element of NAT st x in S . (n + k) ) ; ::_thesis: verum end; theorem Th67: :: SETLIM_1:67 for X, x being set for Si being SigmaField of X for S being SetSequence of Si holds ( x in lim_inf S iff ex n being Element of NAT st for k being Element of NAT holds x in S . (n + k) ) proof let X, x be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds ( x in lim_inf S iff ex n being Element of NAT st for k being Element of NAT holds x in S . (n + k) ) let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds ( x in lim_inf S iff ex n being Element of NAT st for k being Element of NAT holds x in S . (n + k) ) let S be SetSequence of Si; ::_thesis: ( x in lim_inf S iff ex n being Element of NAT st for k being Element of NAT holds x in S . (n + k) ) for B being SetSequence of X holds ( x in Union (inferior_setsequence B) iff ex n being Element of NAT st for k being Element of NAT holds x in B . (n + k) ) proof let B be SetSequence of X; ::_thesis: ( x in Union (inferior_setsequence B) iff ex n being Element of NAT st for k being Element of NAT holds x in B . (n + k) ) lim_inf B = Union (inferior_setsequence B) ; hence ( x in Union (inferior_setsequence B) iff ex n being Element of NAT st for k being Element of NAT holds x in B . (n + k) ) by KURATO_0:4; ::_thesis: verum end; hence ( x in lim_inf S iff ex n being Element of NAT st for k being Element of NAT holds x in S . (n + k) ) ; ::_thesis: verum end; theorem :: SETLIM_1:68 for X being set for Si being SigmaField of X for S being SetSequence of Si holds Intersection S c= lim_inf S proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds Intersection S c= lim_inf S let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds Intersection S c= lim_inf S let S be SetSequence of Si; ::_thesis: Intersection S c= lim_inf S let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Intersection S or x in lim_inf S ) assume x in Intersection S ; ::_thesis: x in lim_inf S then for k being Element of NAT holds x in S . (0 + k) by PROB_1:13; hence x in lim_inf S by Th67; ::_thesis: verum end; theorem :: SETLIM_1:69 for X being set for Si being SigmaField of X for S being SetSequence of Si holds lim_sup S c= Union S proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds lim_sup S c= Union S let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_sup S c= Union S let S be SetSequence of Si; ::_thesis: lim_sup S c= Union S let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in lim_sup S or x in Union S ) assume x in lim_sup S ; ::_thesis: x in Union S then ex k being Element of NAT st x in S . (0 + k) by Th66; hence x in Union S by PROB_1:12; ::_thesis: verum end; theorem :: SETLIM_1:70 for X being set for Si being SigmaField of X for S being SetSequence of Si holds lim_inf S c= lim_sup S proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds lim_inf S c= lim_sup S let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_inf S c= lim_sup S let S be SetSequence of Si; ::_thesis: lim_inf S c= lim_sup S for B being SetSequence of X holds Union (inferior_setsequence B) c= Intersection (superior_setsequence B) proof let B be SetSequence of X; ::_thesis: Union (inferior_setsequence B) c= Intersection (superior_setsequence B) ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ; hence Union (inferior_setsequence B) c= Intersection (superior_setsequence B) by KURATO_0:6; ::_thesis: verum end; hence lim_inf S c= lim_sup S ; ::_thesis: verum end; theorem Th71: :: SETLIM_1:71 for X being set for Si being SigmaField of X for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) ` proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) ` let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_inf S = (lim_sup (Complement S)) ` let S be SetSequence of Si; ::_thesis: lim_inf S = (lim_sup (Complement S)) ` for B being SetSequence of X holds Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` proof let B be SetSequence of X; ::_thesis: Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` ( lim_inf B = Union (inferior_setsequence B) & (lim_sup (Complement B)) ` = (Intersection (superior_setsequence (Complement B))) ` ) ; hence Union (inferior_setsequence B) = (Intersection (superior_setsequence (Complement B))) ` by KURATO_0:9; ::_thesis: verum end; hence lim_inf S = (lim_sup (Complement S)) ` ; ::_thesis: verum end; theorem :: SETLIM_1:72 for X being set for Si being SigmaField of X for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) ` proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) ` let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si holds lim_sup S = (lim_inf (Complement S)) ` let S be SetSequence of Si; ::_thesis: lim_sup S = (lim_inf (Complement S)) ` lim_inf (Complement S) = (lim_sup (Complement (Complement S))) ` by Th71 .= (lim_sup S) ` ; hence lim_sup S = (lim_inf (Complement S)) ` ; ::_thesis: verum end; theorem :: SETLIM_1:73 for X being set for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 proof let X be set ; ::_thesis: for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) implies (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 ) A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) holds (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) proof let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) implies (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) ) A2: ( lim_inf B = Union (inferior_setsequence B) & lim_inf A2 = Union (inferior_setsequence A2) ) ; A3: lim_inf A3 = Union (inferior_setsequence A3) ; assume for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ; ::_thesis: (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) hence (Union (inferior_setsequence B)) \/ (Union (inferior_setsequence A2)) c= Union (inferior_setsequence A3) by A2, A3, KURATO_0:12; ::_thesis: verum end; assume for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ; ::_thesis: (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 hence (lim_inf S1) \/ (lim_inf S2) c= lim_inf S3 by A1; ::_thesis: verum end; theorem :: SETLIM_1:74 for X being set for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) proof let X be set ; ::_thesis: for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) implies lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) ) A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) holds (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) proof let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) implies (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) ) A2: ( lim_inf B = Union (inferior_setsequence B) & lim_inf A2 = Union (inferior_setsequence A2) ) ; A3: lim_inf A3 = Union (inferior_setsequence A3) ; assume for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ; ::_thesis: (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) hence (Union (inferior_setsequence B)) /\ (Union (inferior_setsequence A2)) = Union (inferior_setsequence A3) by A2, A3, KURATO_0:10; ::_thesis: verum end; assume for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ; ::_thesis: lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) hence lim_inf S3 = (lim_inf S1) /\ (lim_inf S2) by A1; ::_thesis: verum end; theorem :: SETLIM_1:75 for X being set for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) proof let X be set ; ::_thesis: for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) holds lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ) implies lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) ) A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) holds (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) proof let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ) implies (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) ) A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ; A3: lim_sup A3 = Intersection (superior_setsequence A3) ; assume for n being Element of NAT holds A3 . n = (B . n) \/ (A2 . n) ; ::_thesis: (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) hence (Intersection (superior_setsequence B)) \/ (Intersection (superior_setsequence A2)) = Intersection (superior_setsequence A3) by A2, A3, KURATO_0:11; ::_thesis: verum end; assume for n being Element of NAT holds S3 . n = (S1 . n) \/ (S2 . n) ; ::_thesis: lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) hence lim_sup S3 = (lim_sup S1) \/ (lim_sup S2) by A1; ::_thesis: verum end; theorem :: SETLIM_1:76 for X being set for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) proof let X be set ; ::_thesis: for Si being SigmaField of X for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) let Si be SigmaField of X; ::_thesis: for S3, S1, S2 being SetSequence of Si st ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) holds lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) let S3, S1, S2 be SetSequence of Si; ::_thesis: ( ( for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ) implies lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) ) A1: for A3, B, A2 being SetSequence of X st ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) holds Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) proof let A3, B, A2 be SetSequence of X; ::_thesis: ( ( for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ) implies Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) ) A2: ( lim_sup B = Intersection (superior_setsequence B) & lim_sup A2 = Intersection (superior_setsequence A2) ) ; A3: lim_sup A3 = Intersection (superior_setsequence A3) ; assume for n being Element of NAT holds A3 . n = (B . n) /\ (A2 . n) ; ::_thesis: Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) hence Intersection (superior_setsequence A3) c= (Intersection (superior_setsequence B)) /\ (Intersection (superior_setsequence A2)) by A2, A3, KURATO_0:13; ::_thesis: verum end; assume for n being Element of NAT holds S3 . n = (S1 . n) /\ (S2 . n) ; ::_thesis: lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) hence lim_sup S3 c= (lim_sup S1) /\ (lim_sup S2) by A1; ::_thesis: verum end; theorem :: SETLIM_1:77 for X being set for A being Subset of X for Si being SigmaField of X for S being SetSequence of Si st S is constant & the_value_of S = A holds ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) proof let X be set ; ::_thesis: for A being Subset of X for Si being SigmaField of X for S being SetSequence of Si st S is constant & the_value_of S = A holds ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) let A be Subset of X; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si st S is constant & the_value_of S = A holds ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is constant & the_value_of S = A holds ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) let S be SetSequence of Si; ::_thesis: ( S is constant & the_value_of S = A implies ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) ) A1: for B being SetSequence of X st B is constant & the_value_of B = A holds ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) proof let B be SetSequence of X; ::_thesis: ( B is constant & the_value_of B = A implies ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) ) A2: ( lim_inf B = Union (inferior_setsequence B) & lim_sup B = Intersection (superior_setsequence B) ) ; assume ( B is constant & the_value_of B = A ) ; ::_thesis: ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) hence ( Union (inferior_setsequence B) = A & Intersection (superior_setsequence B) = A ) by A2, Th58; ::_thesis: verum end; assume ( S is constant & the_value_of S = A ) ; ::_thesis: ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) then ( lim_inf S = A & lim_sup S = A ) by A1; hence ( S is convergent & lim S = A & lim_inf S = A & lim_sup S = A ) by KURATO_0:def_5; ::_thesis: verum end; theorem Th78: :: SETLIM_1:78 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V50() holds lim_sup S = Union S by Th43; theorem Th79: :: SETLIM_1:79 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V50() holds lim_inf S = Union S by Th46; theorem Th80: :: SETLIM_1:80 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V50() holds ( S is convergent & lim S = Union S ) proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si st S is V50() holds ( S is convergent & lim S = Union S ) let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is V50() holds ( S is convergent & lim S = Union S ) let S be SetSequence of Si; ::_thesis: ( S is V50() implies ( S is convergent & lim S = Union S ) ) assume A1: S is V50() ; ::_thesis: ( S is convergent & lim S = Union S ) then ( lim_sup S = Union S & lim_inf S = Union S ) by Th78, Th79; hence S is convergent by KURATO_0:def_5; ::_thesis: lim S = Union S thus lim S = Union S by A1, Th78; ::_thesis: verum end; theorem Th81: :: SETLIM_1:81 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V49() holds lim_sup S = Intersection S by Th49; theorem Th82: :: SETLIM_1:82 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V49() holds lim_inf S = Intersection S by Th53; theorem Th83: :: SETLIM_1:83 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is V49() holds ( S is convergent & lim S = Intersection S ) proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si st S is V49() holds ( S is convergent & lim S = Intersection S ) let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is V49() holds ( S is convergent & lim S = Intersection S ) let S be SetSequence of Si; ::_thesis: ( S is V49() implies ( S is convergent & lim S = Intersection S ) ) assume A1: S is V49() ; ::_thesis: ( S is convergent & lim S = Intersection S ) then ( lim_sup S = Intersection S & lim_inf S = Intersection S ) by Th81, Th82; hence S is convergent by KURATO_0:def_5; ::_thesis: lim S = Intersection S thus lim S = Intersection S by A1, Th81; ::_thesis: verum end; theorem :: SETLIM_1:84 for X being set for Si being SigmaField of X for S being SetSequence of Si st S is monotone holds S is convergent proof let X be set ; ::_thesis: for Si being SigmaField of X for S being SetSequence of Si st S is monotone holds S is convergent let Si be SigmaField of X; ::_thesis: for S being SetSequence of Si st S is monotone holds S is convergent let S be SetSequence of Si; ::_thesis: ( S is monotone implies S is convergent ) assume A1: S is monotone ; ::_thesis: S is convergent percases ( not S is V49() or not S is V50() ) by A1, Def1; suppose S is V49() ; ::_thesis: S is convergent hence S is convergent by Th83; ::_thesis: verum end; suppose S is V50() ; ::_thesis: S is convergent hence S is convergent by Th80; ::_thesis: verum end; end; end;