let L be Semilattice; :: thesis: for A being Subset of L

for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

let A be Subset of L; :: thesis: for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

let f, g be sequence of the carrier of L; :: thesis: ( rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies A is_coarser_than rng g )

assume that

A1: rng f = A and

A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; :: thesis: A is_coarser_than rng g

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in A or ex b_{1} being Element of the carrier of L st

( b_{1} in rng g & b_{1} <= a ) )

assume a in A ; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} in rng g & b_{1} <= a )

then consider n being object such that

A3: n in dom f and

A4: f . n = a by A1, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A3;

reconsider T = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1;

take b = "/\" (T,L); :: thesis: ( b in rng g & b <= a )

( dom g = NAT & g . n = b ) by A2, FUNCT_2:def 1;

hence b in rng g by FUNCT_1:def 3; :: thesis: b <= a

f . n in T ;

then A5: {(f . n)} c= T by ZFMISC_1:31;

( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55;

then b <= "/\" ({(f . n)},L) by A5, YELLOW_0:35;

hence b <= a by A4, YELLOW_0:39; :: thesis: verum

for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

let A be Subset of L; :: thesis: for f, g being sequence of the carrier of L st rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) holds

A is_coarser_than rng g

let f, g be sequence of the carrier of L; :: thesis: ( rng f = A & ( for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ) implies A is_coarser_than rng g )

assume that

A1: rng f = A and

A2: for n being Element of NAT holds g . n = "/\" ( { (f . m) where m is Element of NAT : m <= n } ,L) ; :: thesis: A is_coarser_than rng g

let a be Element of L; :: according to YELLOW_4:def 2 :: thesis: ( not a in A or ex b

( b

assume a in A ; :: thesis: ex b

( b

then consider n being object such that

A3: n in dom f and

A4: f . n = a by A1, FUNCT_1:def 3;

reconsider n = n as Element of NAT by A3;

reconsider T = { (f . m) where m is Element of NAT : m <= n } as non empty finite Subset of L by Lm1;

take b = "/\" (T,L); :: thesis: ( b in rng g & b <= a )

( dom g = NAT & g . n = b ) by A2, FUNCT_2:def 1;

hence b in rng g by FUNCT_1:def 3; :: thesis: b <= a

f . n in T ;

then A5: {(f . n)} c= T by ZFMISC_1:31;

( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55;

then b <= "/\" ({(f . n)},L) by A5, YELLOW_0:35;

hence b <= a by A4, YELLOW_0:39; :: thesis: verum