let L be Semilattice; :: thesis: for A being Subset of L
for f, g being Function of NAT ,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 Function of NAT ,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 Function of NAT ,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 set such that
A3: n in dom f and
A4: f . n = a by A1, FUNCT_1:def 5;
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;
A5: ( ex_inf_of {(f . n)},L & ex_inf_of T,L ) by YELLOW_0:55;
take b = "/\" T,L; :: thesis: ( b in rng g & b <= a )
A6: dom g = NAT by FUNCT_2:def 1;
g . n = b by A2;
hence b in rng g by A6, FUNCT_1:def 5; :: thesis: b <= a
f . n in T ;
then {(f . n)} c= T by ZFMISC_1:37;
then b <= "/\" {(f . n)},L by A5, YELLOW_0:35;
hence b <= a by A4, YELLOW_0:39; :: thesis: verum