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₁ being Element of the carrier of L st
( b₁ in rng g & b₁ <= a ) )
assume a in A ; :: thesis: ex b₁ being Element of the carrier of L st
( b₁ in rng g & b₁ <= 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