:: 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;