:: LATTICE2 semantic presentation begin theorem Th1: :: LATTICE2:1 for A being set for C being non empty set for B being Subset of A for g being Function of A,C holds dom (g | B) = B proof let A be set ; ::_thesis: for C being non empty set for B being Subset of A for g being Function of A,C holds dom (g | B) = B let C be non empty set ; ::_thesis: for B being Subset of A for g being Function of A,C holds dom (g | B) = B let B be Subset of A; ::_thesis: for g being Function of A,C holds dom (g | B) = B let g be Function of A,C; ::_thesis: dom (g | B) = B thus dom (g | B) = (dom g) /\ B by RELAT_1:61 .= A /\ B by FUNCT_2:def_1 .= B by XBOOLE_1:28 ; ::_thesis: verum end; theorem Th2: :: LATTICE2:2 for A being set for C being non empty set for B being Subset of A for f, g being Function of A,C holds ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x ) proof let A be set ; ::_thesis: for C being non empty set for B being Subset of A for f, g being Function of A,C holds ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x ) let C be non empty set ; ::_thesis: for B being Subset of A for f, g being Function of A,C holds ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x ) let B be Subset of A; ::_thesis: for f, g being Function of A,C holds ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x ) let f, g be Function of A,C; ::_thesis: ( f | B = g | B iff for x being Element of A st x in B holds g . x = f . x ) thus ( f | B = g | B implies for x being Element of A st x in B holds g . x = f . x ) ::_thesis: ( ( for x being Element of A st x in B holds g . x = f . x ) implies f | B = g | B ) proof assume A1: f | B = g | B ; ::_thesis: for x being Element of A st x in B holds g . x = f . x let x be Element of A; ::_thesis: ( x in B implies g . x = f . x ) assume A2: x in B ; ::_thesis: g . x = f . x hence g . x = (g | B) . x by FUNCT_1:49 .= f . x by A1, A2, FUNCT_1:49 ; ::_thesis: verum end; reconsider f9 = f | B, g9 = g | B as Function of B,C by FUNCT_2:32; assume A3: for x being Element of A st x in B holds g . x = f . x ; ::_thesis: f | B = g | B A4: now__::_thesis:_for_x_being_set_st_x_in_B_holds_ f9_._x_=_g9_._x let x be set ; ::_thesis: ( x in B implies f9 . x = g9 . x ) assume A5: x in B ; ::_thesis: f9 . x = g9 . x hence f9 . x = f . x by FUNCT_1:49 .= g . x by A3, A5 .= g9 . x by A5, FUNCT_1:49 ; ::_thesis: verum end; thus f | B = f9 | B .= g9 | B by A4, FUNCT_2:12 .= g | B ; ::_thesis: verum end; theorem Th3: :: LATTICE2:3 for A being set for C being non empty set for f, g being Function of A,C for B being set holds f +* (g | B) is Function of A,C proof let A be set ; ::_thesis: for C being non empty set for f, g being Function of A,C for B being set holds f +* (g | B) is Function of A,C let C be non empty set ; ::_thesis: for f, g being Function of A,C for B being set holds f +* (g | B) is Function of A,C let f, g be Function of A,C; ::_thesis: for B being set holds f +* (g | B) is Function of A,C let B be set ; ::_thesis: f +* (g | B) is Function of A,C A1: ( dom f = A & dom g = A ) by FUNCT_2:def_1; dom (f +* (g | B)) = (dom f) \/ (dom (g | B)) by FUNCT_4:def_1 .= (dom f) \/ ((dom g) /\ B) by RELAT_1:61 .= A by A1, XBOOLE_1:22 ; hence f +* (g | B) is Function of A,C by FUNCT_2:67; ::_thesis: verum end; theorem Th4: :: LATTICE2:4 for A being set for C being non empty set for B being Subset of A for g, f being Function of A,C holds (g | B) +* f = f proof let A be set ; ::_thesis: for C being non empty set for B being Subset of A for g, f being Function of A,C holds (g | B) +* f = f let C be non empty set ; ::_thesis: for B being Subset of A for g, f being Function of A,C holds (g | B) +* f = f let B be Subset of A; ::_thesis: for g, f being Function of A,C holds (g | B) +* f = f let g, f be Function of A,C; ::_thesis: (g | B) +* f = f ( dom (g | B) = B & dom f = A ) by Th1, FUNCT_2:def_1; hence (g | B) +* f = f by FUNCT_4:19; ::_thesis: verum end; theorem Th5: :: LATTICE2:5 for f, g being Function st g c= f holds f +* g = f proof let f, g be Function; ::_thesis: ( g c= f implies f +* g = f ) assume A1: g c= f ; ::_thesis: f +* g = f then dom g c= dom f by GRFUNC_1:2; then A2: dom f = (dom f) \/ (dom g) by XBOOLE_1:12; for x being set st x in dom f holds ( ( x in dom g implies f . x = g . x ) & ( not x in dom g implies f . x = f . x ) ) by A1, GRFUNC_1:2; hence f +* g = f by A2, FUNCT_4:def_1; ::_thesis: verum end; theorem :: LATTICE2:6 for A being set for C being non empty set for B being Subset of A for f being Function of A,C holds f +* (f | B) = f by Th5, RELAT_1:59; theorem Th7: :: LATTICE2:7 for A being set for C being non empty set for B being Subset of A for g, f being Function of A,C st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f proof let A be set ; ::_thesis: for C being non empty set for B being Subset of A for g, f being Function of A,C st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let C be non empty set ; ::_thesis: for B being Subset of A for g, f being Function of A,C st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let B be Subset of A; ::_thesis: for g, f being Function of A,C st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let g, f be Function of A,C; ::_thesis: ( ( for x being Element of A st x in B holds g . x = f . x ) implies f +* (g | B) = f ) assume for x being Element of A st x in B holds g . x = f . x ; ::_thesis: f +* (g | B) = f then g | B = f | B by Th2; hence f +* (g | B) = f by Th5, RELAT_1:59; ::_thesis: verum end; theorem :: LATTICE2:8 for A being set for C being non empty set for g, f being Function of A,C for B being Finite_Subset of A holds (g | B) +* f = f proof let A be set ; ::_thesis: for C being non empty set for g, f being Function of A,C for B being Finite_Subset of A holds (g | B) +* f = f let C be non empty set ; ::_thesis: for g, f being Function of A,C for B being Finite_Subset of A holds (g | B) +* f = f let g, f be Function of A,C; ::_thesis: for B being Finite_Subset of A holds (g | B) +* f = f let B be Finite_Subset of A; ::_thesis: (g | B) +* f = f reconsider C = B as Subset of A by FINSUB_1:17; (g | C) +* f = f by Th4; hence (g | B) +* f = f ; ::_thesis: verum end; theorem Th9: :: LATTICE2:9 for A being set for C being non empty set for g being Function of A,C for B being Finite_Subset of A holds dom (g | B) = B proof let A be set ; ::_thesis: for C being non empty set for g being Function of A,C for B being Finite_Subset of A holds dom (g | B) = B let C be non empty set ; ::_thesis: for g being Function of A,C for B being Finite_Subset of A holds dom (g | B) = B let g be Function of A,C; ::_thesis: for B being Finite_Subset of A holds dom (g | B) = B let B be Finite_Subset of A; ::_thesis: dom (g | B) = B reconsider C = B as Subset of A by FINSUB_1:17; dom (g | C) = C by Th1; hence dom (g | B) = B ; ::_thesis: verum end; theorem Th10: :: LATTICE2:10 for A being set for C being non empty set for g, f being Function of A,C for B being Finite_Subset of A st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f proof let A be set ; ::_thesis: for C being non empty set for g, f being Function of A,C for B being Finite_Subset of A st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let C be non empty set ; ::_thesis: for g, f being Function of A,C for B being Finite_Subset of A st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let g, f be Function of A,C; ::_thesis: for B being Finite_Subset of A st ( for x being Element of A st x in B holds g . x = f . x ) holds f +* (g | B) = f let B be Finite_Subset of A; ::_thesis: ( ( for x being Element of A st x in B holds g . x = f . x ) implies f +* (g | B) = f ) reconsider C = B as Subset of A by FINSUB_1:17; ( ( for x being Element of A st x in C holds g . x = f . x ) implies f +* (g | C) = f ) by Th7; hence ( ( for x being Element of A st x in B holds g . x = f . x ) implies f +* (g | B) = f ) ; ::_thesis: verum end; definition let D be non empty set ; let o, o9 be BinOp of D; predo absorbs o9 means :Def1: :: LATTICE2:def 1 for x, y being Element of D holds o . (x,(o9 . (x,y))) = x; end; :: deftheorem Def1 defines absorbs LATTICE2:def_1_:_ for D being non empty set for o, o9 being BinOp of D holds ( o absorbs o9 iff for x, y being Element of D holds o . (x,(o9 . (x,y))) = x ); notation let D be non empty set ; let o, o9 be BinOp of D; antonym o doesn't_absorb o9 for o absorbs o9; end; theorem Th11: :: LATTICE2:11 for L being non empty LattStr st the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L holds L is Lattice-like proof let L be non empty LattStr ; ::_thesis: ( the L_join of L is commutative & the L_join of L is associative & the L_meet of L is commutative & the L_meet of L is associative & the L_join of L absorbs the L_meet of L & the L_meet of L absorbs the L_join of L implies L is Lattice-like ) assume that A1: the L_join of L is commutative and A2: the L_join of L is associative and A3: the L_meet of L is commutative and A4: the L_meet of L is associative and A5: the L_join of L absorbs the L_meet of L and A6: the L_meet of L absorbs the L_join of L ; ::_thesis: L is Lattice-like thus for a, b being Element of L holds a "\/" b = b "\/" a by A1, BINOP_1:def_2; :: according to LATTICES:def_4,LATTICES:def_10 ::_thesis: ( L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) thus for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, BINOP_1:def_3; :: according to LATTICES:def_5 ::_thesis: ( L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) thus for a, b being Element of L holds (a "/\" b) "\/" b = b :: according to LATTICES:def_8 ::_thesis: ( L is meet-commutative & L is meet-associative & L is join-absorbing ) proof let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b thus (a "/\" b) "\/" b = b "\/" (a "/\" b) by A1, BINOP_1:def_2 .= b "\/" (b "/\" a) by A3, BINOP_1:def_2 .= b by A5, Def1 ; ::_thesis: verum end; thus for a, b being Element of L holds a "/\" b = b "/\" a by A3, BINOP_1:def_2; :: according to LATTICES:def_6 ::_thesis: ( L is meet-associative & L is join-absorbing ) thus for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c by A4, BINOP_1:def_3; :: according to LATTICES:def_7 ::_thesis: L is join-absorbing let a be Element of L; :: according to LATTICES:def_9 ::_thesis: for b1 being Element of the carrier of L holds a "/\" (a "\/" b1) = a let b be Element of L; ::_thesis: a "/\" (a "\/" b) = a thus a "/\" (a "\/" b) = a by A6, Def1; ::_thesis: verum end; definition let L be LattStr ; funcL .: -> strict LattStr equals :: LATTICE2:def 2 LattStr(# the carrier of L, the L_meet of L, the L_join of L #); correctness coherence LattStr(# the carrier of L, the L_meet of L, the L_join of L #) is strict LattStr ; ; end; :: deftheorem defines .: LATTICE2:def_2_:_ for L being LattStr holds L .: = LattStr(# the carrier of L, the L_meet of L, the L_join of L #); registration let L be non empty LattStr ; clusterL .: -> non empty strict ; coherence not L .: is empty ; end; theorem :: LATTICE2:12 for L being non empty LattStr holds ( the carrier of L = the carrier of (L .:) & the L_join of L = the L_meet of (L .:) & the L_meet of L = the L_join of (L .:) ) ; theorem :: LATTICE2:13 for L being non empty strict LattStr holds (L .:) .: = L ; theorem Th14: :: LATTICE2:14 for L being Lattice for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds u = Bottom L proof let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds u "\/" v = v ) holds u = Bottom L let u be Element of L; ::_thesis: ( ( for v being Element of L holds u "\/" v = v ) implies u = Bottom L ) assume A1: for v being Element of L holds u "\/" v = v ; ::_thesis: u = Bottom L now__::_thesis:_for_v_being_Element_of_L_holds_v_"/\"_u_=_u let v be Element of L; ::_thesis: v "/\" u = u v "\/" u = v by A1; then u [= v by LATTICES:def_3; hence v "/\" u = u by LATTICES:4; ::_thesis: verum end; hence u = Bottom L by RLSUB_2:64; ::_thesis: verum end; theorem Th15: :: LATTICE2:15 for L being Lattice for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds u = Bottom L proof let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds the L_join of L . (u,v) = v ) holds u = Bottom L let u be Element of L; ::_thesis: ( ( for v being Element of L holds the L_join of L . (u,v) = v ) implies u = Bottom L ) assume for v being Element of L holds the L_join of L . (u,v) = v ; ::_thesis: u = Bottom L then for v being Element of L holds u "\/" v = v ; hence u = Bottom L by Th14; ::_thesis: verum end; theorem Th16: :: LATTICE2:16 for L being Lattice for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds u = Top L proof let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds u "/\" v = v ) holds u = Top L let u be Element of L; ::_thesis: ( ( for v being Element of L holds u "/\" v = v ) implies u = Top L ) assume A1: for v being Element of L holds u "/\" v = v ; ::_thesis: u = Top L now__::_thesis:_for_v_being_Element_of_L_holds_u_=_v_"\/"_u let v be Element of L; ::_thesis: u = v "\/" u v "/\" u = v by A1; then v [= u by LATTICES:4; hence u = v "\/" u by LATTICES:def_3; ::_thesis: verum end; hence u = Top L by RLSUB_2:65; ::_thesis: verum end; theorem Th17: :: LATTICE2:17 for L being Lattice for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds u = Top L proof let L be Lattice; ::_thesis: for u being Element of L st ( for v being Element of L holds the L_meet of L . (u,v) = v ) holds u = Top L let u be Element of L; ::_thesis: ( ( for v being Element of L holds the L_meet of L . (u,v) = v ) implies u = Top L ) assume for v being Element of L holds the L_meet of L . (u,v) = v ; ::_thesis: u = Top L then for v being Element of L holds u "/\" v = v ; hence u = Top L by Th16; ::_thesis: verum end; registration let L be Lattice; cluster the L_join of L -> idempotent ; coherence the L_join of L is idempotent proof let a be Element of L; :: according to BINOP_1:def_4 ::_thesis: the L_join of L . (a,a) = a thus the L_join of L . (a,a) = a "\/" a .= a ; ::_thesis: verum end; end; registration let L be non empty join-commutative \/-SemiLattStr ; cluster the L_join of L -> commutative ; coherence the L_join of L is commutative proof let a, b be Element of L; :: according to BINOP_1:def_2 ::_thesis: the L_join of L . (a,b) = the L_join of L . (b,a) thus the L_join of L . (a,b) = b "\/" a by LATTICES:def_1 .= the L_join of L . (b,a) ; ::_thesis: verum end; end; theorem Th18: :: LATTICE2:18 for L being Lattice st the L_join of L is having_a_unity holds Bottom L = the_unity_wrt the L_join of L proof let L be Lattice; ::_thesis: ( the L_join of L is having_a_unity implies Bottom L = the_unity_wrt the L_join of L ) set J = the L_join of L; given u being Element of L such that A1: u is_a_unity_wrt the L_join of L ; :: according to SETWISEO:def_2 ::_thesis: Bottom L = the_unity_wrt the L_join of L for v being Element of L holds the L_join of L . (u,v) = v by A1, BINOP_1:4; then u = Bottom L by Th15; hence Bottom L = the_unity_wrt the L_join of L by A1, BINOP_1:def_8; ::_thesis: verum end; registration let L be non empty join-associative \/-SemiLattStr ; cluster the L_join of L -> associative ; coherence the L_join of L is associative proof let a, b, c be Element of L; :: according to BINOP_1:def_3 ::_thesis: the L_join of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_join of L . (a,b)),c) thus the L_join of L . (a,( the L_join of L . (b,c))) = a "\/" (b "\/" c) .= (a "\/" b) "\/" c by LATTICES:def_5 .= the L_join of L . (( the L_join of L . (a,b)),c) ; ::_thesis: verum end; end; registration let L be Lattice; cluster the L_meet of L -> idempotent ; coherence the L_meet of L is idempotent proof let a be Element of L; :: according to BINOP_1:def_4 ::_thesis: the L_meet of L . (a,a) = a thus the L_meet of L . (a,a) = a "/\" a .= a ; ::_thesis: verum end; end; registration let L be non empty meet-commutative /\-SemiLattStr ; cluster the L_meet of L -> commutative ; coherence the L_meet of L is commutative proof let a, b be Element of L; :: according to BINOP_1:def_2 ::_thesis: the L_meet of L . (a,b) = the L_meet of L . (b,a) thus the L_meet of L . (a,b) = b "/\" a by LATTICES:def_2 .= the L_meet of L . (b,a) ; ::_thesis: verum end; end; registration let L be non empty meet-associative /\-SemiLattStr ; cluster the L_meet of L -> associative ; coherence the L_meet of L is associative proof let a, b, c be Element of L; :: according to BINOP_1:def_3 ::_thesis: the L_meet of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_meet of L . (a,b)),c) thus the L_meet of L . (a,( the L_meet of L . (b,c))) = a "/\" (b "/\" c) .= (a "/\" b) "/\" c by LATTICES:def_7 .= the L_meet of L . (( the L_meet of L . (a,b)),c) ; ::_thesis: verum end; end; theorem Th19: :: LATTICE2:19 for L being Lattice st the L_meet of L is having_a_unity holds Top L = the_unity_wrt the L_meet of L proof let L be Lattice; ::_thesis: ( the L_meet of L is having_a_unity implies Top L = the_unity_wrt the L_meet of L ) set J = the L_meet of L; given u being Element of L such that A1: u is_a_unity_wrt the L_meet of L ; :: according to SETWISEO:def_2 ::_thesis: Top L = the_unity_wrt the L_meet of L for v being Element of L holds the L_meet of L . (u,v) = v by A1, BINOP_1:4; then u = Top L by Th17; hence Top L = the_unity_wrt the L_meet of L by A1, BINOP_1:def_8; ::_thesis: verum end; theorem Th20: :: LATTICE2:20 for L being Lattice holds the L_join of L is_distributive_wrt the L_join of L proof let L be Lattice; ::_thesis: the L_join of L is_distributive_wrt the L_join of L now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_join_of_L_._(a,(_the_L_join_of_L_._(b,c)))_=_the_L_join_of_L_._((_the_L_join_of_L_._(a,b)),(_the_L_join_of_L_._(a,c))) let a, b, c be Element of L; ::_thesis: the L_join of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) thus the L_join of L . (a,( the L_join of L . (b,c))) = a "\/" (b "\/" c) .= (a "\/" b) "\/" c by LATTICES:def_5 .= ((a "\/" a) "\/" b) "\/" c .= ((a "\/" b) "\/" a) "\/" c by LATTICES:def_5 .= (a "\/" b) "\/" (a "\/" c) by LATTICES:def_5 .= the L_join of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) ; ::_thesis: verum end; hence the L_join of L is_distributive_wrt the L_join of L by BINOP_1:12; ::_thesis: verum end; theorem :: LATTICE2:21 for L being Lattice st L is D_Lattice holds the L_join of L is_distributive_wrt the L_meet of L proof let L be Lattice; ::_thesis: ( L is D_Lattice implies the L_join of L is_distributive_wrt the L_meet of L ) assume A1: L is D_Lattice ; ::_thesis: the L_join of L is_distributive_wrt the L_meet of L now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_join_of_L_._(a,(_the_L_meet_of_L_._(b,c)))_=_the_L_meet_of_L_._((_the_L_join_of_L_._(a,b)),(_the_L_join_of_L_._(a,c))) let a, b, c be Element of L; ::_thesis: the L_join of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) thus the L_join of L . (a,( the L_meet of L . (b,c))) = a "\/" (b "/\" c) .= (a "\/" b) "/\" (a "\/" c) by A1, LATTICES:11 .= the L_meet of L . (( the L_join of L . (a,b)),( the L_join of L . (a,c))) ; ::_thesis: verum end; hence the L_join of L is_distributive_wrt the L_meet of L by BINOP_1:12; ::_thesis: verum end; theorem Th22: :: LATTICE2:22 for L being Lattice st the L_join of L is_distributive_wrt the L_meet of L holds L is distributive proof let L be Lattice; ::_thesis: ( the L_join of L is_distributive_wrt the L_meet of L implies L is distributive ) assume A1: the L_join of L is_distributive_wrt the L_meet of L ; ::_thesis: L is distributive then A2: for a, b, c being Element of L holds a "\/" (b "/\" c) = (a "\/" b) "/\" (a "\/" c) by BINOP_1:12; let a be Element of L; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of L holds a "/\" (b1 "\/" b2) = (a "/\" b1) "\/" (a "/\" b2) let b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) thus a "/\" (b "\/" c) = (a "/\" (c "\/" a)) "/\" (c "\/" b) by LATTICES:def_9 .= a "/\" ((c "\/" a) "/\" (c "\/" b)) by LATTICES:def_7 .= a "/\" ((a "/\" b) "\/" c) by A2 .= ((a "/\" b) "\/" a) "/\" ((a "/\" b) "\/" c) by LATTICES:def_8 .= (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:12 ; ::_thesis: verum end; theorem Th23: :: LATTICE2:23 for L being Lattice st L is D_Lattice holds the L_meet of L is_distributive_wrt the L_join of L proof let L be Lattice; ::_thesis: ( L is D_Lattice implies the L_meet of L is_distributive_wrt the L_join of L ) assume A1: L is D_Lattice ; ::_thesis: the L_meet of L is_distributive_wrt the L_join of L now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_meet_of_L_._(a,(_the_L_join_of_L_._(b,c)))_=_the_L_join_of_L_._((_the_L_meet_of_L_._(a,b)),(_the_L_meet_of_L_._(a,c))) let a, b, c be Element of L; ::_thesis: the L_meet of L . (a,( the L_join of L . (b,c))) = the L_join of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) thus the L_meet of L . (a,( the L_join of L . (b,c))) = a "/\" (b "\/" c) .= (a "/\" b) "\/" (a "/\" c) by A1, LATTICES:def_11 .= the L_join of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) ; ::_thesis: verum end; hence the L_meet of L is_distributive_wrt the L_join of L by BINOP_1:12; ::_thesis: verum end; theorem :: LATTICE2:24 for L being Lattice st the L_meet of L is_distributive_wrt the L_join of L holds L is distributive proof let L be Lattice; ::_thesis: ( the L_meet of L is_distributive_wrt the L_join of L implies L is distributive ) assume A1: the L_meet of L is_distributive_wrt the L_join of L ; ::_thesis: L is distributive let a be Element of L; :: according to LATTICES:def_11 ::_thesis: for b1, b2 being Element of the carrier of L holds a "/\" (b1 "\/" b2) = (a "/\" b1) "\/" (a "/\" b2) let b, c be Element of L; ::_thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) thus a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by A1, BINOP_1:12; ::_thesis: verum end; theorem Th25: :: LATTICE2:25 for L being Lattice holds the L_meet of L is_distributive_wrt the L_meet of L proof let L be Lattice; ::_thesis: the L_meet of L is_distributive_wrt the L_meet of L now__::_thesis:_for_a,_b,_c_being_Element_of_L_holds_the_L_meet_of_L_._(a,(_the_L_meet_of_L_._(b,c)))_=_the_L_meet_of_L_._((_the_L_meet_of_L_._(a,b)),(_the_L_meet_of_L_._(a,c))) let a, b, c be Element of L; ::_thesis: the L_meet of L . (a,( the L_meet of L . (b,c))) = the L_meet of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) thus the L_meet of L . (a,( the L_meet of L . (b,c))) = a "/\" (b "/\" c) .= (a "/\" b) "/\" c by LATTICES:def_7 .= ((a "/\" a) "/\" b) "/\" c .= ((a "/\" b) "/\" a) "/\" c by LATTICES:def_7 .= (a "/\" b) "/\" (a "/\" c) by LATTICES:def_7 .= the L_meet of L . (( the L_meet of L . (a,b)),( the L_meet of L . (a,c))) ; ::_thesis: verum end; hence the L_meet of L is_distributive_wrt the L_meet of L by BINOP_1:12; ::_thesis: verum end; theorem Th26: :: LATTICE2:26 for L being Lattice holds the L_join of L absorbs the L_meet of L proof let L be Lattice; ::_thesis: the L_join of L absorbs the L_meet of L let x, y be Element of L; :: according to LATTICE2:def_1 ::_thesis: the L_join of L . (x,( the L_meet of L . (x,y))) = x thus the L_join of L . (x,( the L_meet of L . (x,y))) = x "\/" (x "/\" y) .= x by LATTICES:def_8 ; ::_thesis: verum end; theorem Th27: :: LATTICE2:27 for L being Lattice holds the L_meet of L absorbs the L_join of L proof let L be Lattice; ::_thesis: the L_meet of L absorbs the L_join of L let x, y be Element of L; :: according to LATTICE2:def_1 ::_thesis: the L_meet of L . (x,( the L_join of L . (x,y))) = x thus the L_meet of L . (x,( the L_join of L . (x,y))) = x "/\" (x "\/" y) .= x by LATTICES:def_9 ; ::_thesis: verum end; definition let A be non empty set ; let L be Lattice; let B be Finite_Subset of A; let f be Function of A, the carrier of L; func FinJoin (B,f) -> Element of L equals :: LATTICE2:def 3 the L_join of L \$\$ (B,f); correctness coherence the L_join of L \$\$ (B,f) is Element of L; ; func FinMeet (B,f) -> Element of L equals :: LATTICE2:def 4 the L_meet of L \$\$ (B,f); correctness coherence the L_meet of L \$\$ (B,f) is Element of L; ; end; :: deftheorem defines FinJoin LATTICE2:def_3_:_ for A being non empty set for L being Lattice for B being Finite_Subset of A for f being Function of A, the carrier of L holds FinJoin (B,f) = the L_join of L \$\$ (B,f); :: deftheorem defines FinMeet LATTICE2:def_4_:_ for A being non empty set for L being Lattice for B being Finite_Subset of A for f being Function of A, the carrier of L holds FinMeet (B,f) = the L_meet of L \$\$ (B,f); theorem Th28: :: LATTICE2:28 for L being Lattice for A being non empty set for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds f . x [= FinJoin (B,f) proof let L be Lattice; ::_thesis: for A being non empty set for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds f . x [= FinJoin (B,f) let A be non empty set ; ::_thesis: for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds f . x [= FinJoin (B,f) let x be Element of A; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds f . x [= FinJoin (B,f) let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st x in B holds f . x [= FinJoin (B,f) let f be Function of A, the carrier of L; ::_thesis: ( x in B implies f . x [= FinJoin (B,f) ) assume x in B ; ::_thesis: f . x [= FinJoin (B,f) then (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by SETWISEO:22; hence f . x [= FinJoin (B,f) by LATTICES:def_3; ::_thesis: verum end; theorem Th29: :: LATTICE2:29 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & u [= f . x ) holds u [= FinJoin (B,f) proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & u [= f . x ) holds u [= FinJoin (B,f) let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & u [= f . x ) holds u [= FinJoin (B,f) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & u [= f . x ) holds u [= FinJoin (B,f) let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & u [= f . x ) holds u [= FinJoin (B,f) let f be Function of A, the carrier of L; ::_thesis: ( ex x being Element of A st ( x in B & u [= f . x ) implies u [= FinJoin (B,f) ) given x being Element of A such that A1: x in B and A2: u [= f . x ; ::_thesis: u [= FinJoin (B,f) f . x [= FinJoin (B,f) by A1, Th28; then A3: (f . x) "\/" (FinJoin (B,f)) = FinJoin (B,f) by LATTICES:def_3; then u "\/" (FinJoin (B,f)) = (u "\/" (f . x)) "\/" (FinJoin (B,f)) by LATTICES:def_5 .= FinJoin (B,f) by A2, A3, LATTICES:def_3 ; hence u [= FinJoin (B,f) by LATTICES:def_3; ::_thesis: verum end; theorem :: LATTICE2:30 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x = u ) & B <> {} holds FinJoin (B,f) = u by SETWISEO:24; theorem :: LATTICE2:31 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds for x being Element of A st x in B holds f . x [= u proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds for x being Element of A st x in B holds f . x [= u let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds for x being Element of A st x in B holds f . x [= u let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds for x being Element of A st x in B holds f . x [= u let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds for x being Element of A st x in B holds f . x [= u let f be Function of A, the carrier of L; ::_thesis: ( FinJoin (B,f) [= u implies for x being Element of A st x in B holds f . x [= u ) assume A1: FinJoin (B,f) [= u ; ::_thesis: for x being Element of A st x in B holds f . x [= u let x be Element of A; ::_thesis: ( x in B implies f . x [= u ) assume x in B ; ::_thesis: f . x [= u then f . x [= FinJoin (B,f) by Th28; hence f . x [= u by A1, LATTICES:7; ::_thesis: verum end; theorem Th32: :: LATTICE2:32 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let f be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds f . x [= u ) implies FinJoin (B,f) [= u ) assume that A1: B <> {} and A2: for x being Element of A st x in B holds f . x [= u ; ::_thesis: FinJoin (B,f) [= u set J = the L_join of L; A3: now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ (_the_L_join_of_L_[:]_(f,u))_._x_=_u let x be Element of A; ::_thesis: ( x in B implies ( the L_join of L [:] (f,u)) . x = u ) assume x in B ; ::_thesis: ( the L_join of L [:] (f,u)) . x = u then A4: f . x [= u by A2; thus ( the L_join of L [:] (f,u)) . x = (f . x) "\/" u by FUNCOP_1:48 .= u by A4, LATTICES:def_3 ; ::_thesis: verum end; (FinJoin (B,f)) "\/" u = the L_join of L \$\$ (B,( the L_join of L [:] (f,u))) by A1, Th20, SETWISEO:28 .= u by A1, A3, SETWISEO:24 ; hence FinJoin (B,f) [= u by LATTICES:def_3; ::_thesis: verum end; theorem :: LATTICE2:33 for L being Lattice for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) proof let L be Lattice; ::_thesis: for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) implies FinJoin (B,f) [= FinJoin (B,g) ) assume that A1: B <> {} and A2: for x being Element of A st x in B holds f . x [= g . x ; ::_thesis: FinJoin (B,f) [= FinJoin (B,g) now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ f_._x_[=_FinJoin_(B,g) let x be Element of A; ::_thesis: ( x in B implies f . x [= FinJoin (B,g) ) assume A3: x in B ; ::_thesis: f . x [= FinJoin (B,g) then f . x [= g . x by A2; hence f . x [= FinJoin (B,g) by A3, Th29; ::_thesis: verum end; hence FinJoin (B,f) [= FinJoin (B,g) by A1, Th32; ::_thesis: verum end; theorem Th34: :: LATTICE2:34 for L being Lattice for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) proof let L be Lattice; ::_thesis: for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) ) assume that A1: B <> {} and A2: f | B = g | B ; ::_thesis: FinJoin (B,f) = FinJoin (B,g) f .: B = g .: B by A2, RELAT_1:166; hence FinJoin (B,f) = FinJoin (B,g) by A1, SETWISEO:26; ::_thesis: verum end; theorem :: LATTICE2:35 for L being Lattice for v being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} holds v "\/" (FinJoin (B,f)) = FinJoin (B,( the L_join of L [;] (v,f))) by Th20, SETWISEO:27; registration let L be Lattice; clusterL .: -> strict Lattice-like ; coherence L .: is Lattice-like proof ( the L_join of (L .:) absorbs the L_meet of (L .:) & the L_meet of (L .:) absorbs the L_join of (L .:) ) by Th26, Th27; hence L .: is Lattice-like by Th11; ::_thesis: verum end; end; theorem :: LATTICE2:36 for A being non empty set for L being Lattice for B being Finite_Subset of A for f being Function of A, the carrier of L for f9 being Function of A, the carrier of (L .:) st f = f9 holds ( FinJoin (B,f) = FinMeet (B,f9) & FinMeet (B,f) = FinJoin (B,f9) ) ; theorem Th37: :: LATTICE2:37 for L being Lattice for a, b being Element of L for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds ( a "/\" b = a9 "\/" b9 & a "\/" b = a9 "/\" b9 ) ; theorem Th38: :: LATTICE2:38 for L being Lattice for a, b being Element of L st a [= b holds for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds b9 [= a9 proof let L be Lattice; ::_thesis: for a, b being Element of L st a [= b holds for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds b9 [= a9 let a, b be Element of L; ::_thesis: ( a [= b implies for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds b9 [= a9 ) assume a [= b ; ::_thesis: for a9, b9 being Element of (L .:) st a = a9 & b = b9 holds b9 [= a9 then A1: a "\/" b = b by LATTICES:def_3; let a9, b9 be Element of (L .:); ::_thesis: ( a = a9 & b = b9 implies b9 [= a9 ) assume ( a = a9 & b = b9 ) ; ::_thesis: b9 [= a9 then b9 "/\" a9 = b9 by A1, Th37; hence b9 [= a9 by LATTICES:4; ::_thesis: verum end; theorem Th39: :: LATTICE2:39 for L being Lattice for a, b being Element of L for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds b [= a proof let L be Lattice; ::_thesis: for a, b being Element of L for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds b [= a let a, b be Element of L; ::_thesis: for a9, b9 being Element of (L .:) st a9 [= b9 & a = a9 & b = b9 holds b [= a let a9, b9 be Element of (L .:); ::_thesis: ( a9 [= b9 & a = a9 & b = b9 implies b [= a ) assume that A1: a9 [= b9 and A2: ( a = a9 & b = b9 ) ; ::_thesis: b [= a a9 "\/" b9 = b9 by A1, LATTICES:def_3; then b "/\" a = b by A2, Th37; hence b [= a by LATTICES:4; ::_thesis: verum end; theorem Th40: :: LATTICE2:40 for L being Lattice for A being non empty set for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds FinMeet (B,f) [= f . x proof let L be Lattice; ::_thesis: for A being non empty set for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds FinMeet (B,f) [= f . x let A be non empty set ; ::_thesis: for x being Element of A for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds FinMeet (B,f) [= f . x let x be Element of A; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st x in B holds FinMeet (B,f) [= f . x let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st x in B holds FinMeet (B,f) [= f . x let f be Function of A, the carrier of L; ::_thesis: ( x in B implies FinMeet (B,f) [= f . x ) reconsider f9 = f as Function of A, the carrier of (L .:) ; assume x in B ; ::_thesis: FinMeet (B,f) [= f . x then f9 . x [= FinJoin (B,f9) by Th28; hence FinMeet (B,f) [= f . x by Th39; ::_thesis: verum end; theorem Th41: :: LATTICE2:41 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & f . x [= u ) holds FinMeet (B,f) [= u proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & f . x [= u ) holds FinMeet (B,f) [= u let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & f . x [= u ) holds FinMeet (B,f) [= u let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & f . x [= u ) holds FinMeet (B,f) [= u let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st ex x being Element of A st ( x in B & f . x [= u ) holds FinMeet (B,f) [= u let f be Function of A, the carrier of L; ::_thesis: ( ex x being Element of A st ( x in B & f . x [= u ) implies FinMeet (B,f) [= u ) given x being Element of A such that A1: x in B and A2: f . x [= u ; ::_thesis: FinMeet (B,f) [= u reconsider u9 = u as Element of (L .:) ; reconsider f9 = f as Function of A, the carrier of (L .:) ; u9 [= f9 . x by A2, Th38; then u9 [= FinJoin (B,f9) by A1, Th29; hence FinMeet (B,f) [= u by Th39; ::_thesis: verum end; theorem :: LATTICE2:42 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x = u ) & B <> {} holds FinMeet (B,f) = u by SETWISEO:24; theorem :: LATTICE2:43 for L being Lattice for v being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} holds v "/\" (FinMeet (B,f)) = FinMeet (B,( the L_meet of L [;] (v,f))) by Th25, SETWISEO:27; theorem :: LATTICE2:44 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds for x being Element of A st x in B holds u [= f . x proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds for x being Element of A st x in B holds u [= f . x let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds for x being Element of A st x in B holds u [= f . x let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds for x being Element of A st x in B holds u [= f . x let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st u [= FinMeet (B,f) holds for x being Element of A st x in B holds u [= f . x let f be Function of A, the carrier of L; ::_thesis: ( u [= FinMeet (B,f) implies for x being Element of A st x in B holds u [= f . x ) assume A1: u [= FinMeet (B,f) ; ::_thesis: for x being Element of A st x in B holds u [= f . x let x be Element of A; ::_thesis: ( x in B implies u [= f . x ) assume x in B ; ::_thesis: u [= f . x then FinMeet (B,f) [= f . x by Th40; hence u [= f . x by A1, LATTICES:7; ::_thesis: verum end; theorem :: LATTICE2:45 for L being Lattice for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) proof let L be Lattice; ::_thesis: for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) ) reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ; A1: ( FinMeet (B,f) = FinJoin (B,f9) & FinMeet (B,g) = FinJoin (B,g9) ) ; assume ( B <> {} & f | B = g | B ) ; ::_thesis: FinMeet (B,f) = FinMeet (B,g) hence FinMeet (B,f) = FinMeet (B,g) by A1, Th34; ::_thesis: verum end; theorem Th46: :: LATTICE2:46 for L being Lattice for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) proof let L be Lattice; ::_thesis: for u being Element of L for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let u be Element of L; ::_thesis: for A being non empty set for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let B be Finite_Subset of A; ::_thesis: for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let f be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds u [= f . x ) implies u [= FinMeet (B,f) ) assume that A1: B <> {} and A2: for x being Element of A st x in B holds u [= f . x ; ::_thesis: u [= FinMeet (B,f) reconsider u9 = u as Element of (L .:) ; reconsider f9 = f as Function of A, the carrier of (L .:) ; for x being Element of A st x in B holds f9 . x [= u9 by A2, Th38; then FinJoin (B,f9) [= u9 by A1, Th32; hence u [= FinMeet (B,f) by Th39; ::_thesis: verum end; theorem :: LATTICE2:47 for L being Lattice for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) proof let L be Lattice; ::_thesis: for A being non empty set for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let A be non empty set ; ::_thesis: for B being Finite_Subset of A for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let B be Finite_Subset of A; ::_thesis: for f, g being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( B <> {} & ( for x being Element of A st x in B holds f . x [= g . x ) implies FinMeet (B,f) [= FinMeet (B,g) ) assume that A1: B <> {} and A2: for x being Element of A st x in B holds f . x [= g . x ; ::_thesis: FinMeet (B,f) [= FinMeet (B,g) now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ FinMeet_(B,f)_[=_g_._x let x be Element of A; ::_thesis: ( x in B implies FinMeet (B,f) [= g . x ) assume A3: x in B ; ::_thesis: FinMeet (B,f) [= g . x then f . x [= g . x by A2; hence FinMeet (B,f) [= g . x by A3, Th41; ::_thesis: verum end; hence FinMeet (B,f) [= FinMeet (B,g) by A1, Th46; ::_thesis: verum end; theorem :: LATTICE2:48 for L being Lattice holds ( L is lower-bounded iff L .: is upper-bounded ) proof let L be Lattice; ::_thesis: ( L is lower-bounded iff L .: is upper-bounded ) thus ( L is lower-bounded implies L .: is upper-bounded ) ::_thesis: ( L .: is upper-bounded implies L is lower-bounded ) proof given c being Element of L such that A1: for a being Element of L holds ( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: L .: is upper-bounded reconsider c9 = c as Element of (L .:) ; take c9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( c9 "\/" b1 = c9 & b1 "\/" c9 = c9 ) let a9 be Element of (L .:); ::_thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 ) reconsider a = a9 as Element of L ; thus c9 "\/" a9 = c "/\" a .= c9 by A1 ; ::_thesis: a9 "\/" c9 = c9 hence a9 "\/" c9 = c9 ; ::_thesis: verum end; given c being Element of (L .:) such that A2: for a being Element of (L .:) holds ( c "\/" a = c & a "\/" c = c ) ; :: according to LATTICES:def_14 ::_thesis: L is lower-bounded reconsider c9 = c as Element of L ; take c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L holds ( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 ) let a9 be Element of L; ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 ) reconsider a = a9 as Element of (L .:) ; thus c9 "/\" a9 = c "\/" a .= c9 by A2 ; ::_thesis: a9 "/\" c9 = c9 hence a9 "/\" c9 = c9 ; ::_thesis: verum end; theorem Th49: :: LATTICE2:49 for L being Lattice holds ( L is upper-bounded iff L .: is lower-bounded ) proof let L be Lattice; ::_thesis: ( L is upper-bounded iff L .: is lower-bounded ) thus ( L is upper-bounded implies L .: is lower-bounded ) ::_thesis: ( L .: is lower-bounded implies L is upper-bounded ) proof given c being Element of L such that A1: for a being Element of L holds ( c "\/" a = c & a "\/" c = c ) ; :: according to LATTICES:def_14 ::_thesis: L .: is lower-bounded reconsider c9 = c as Element of (L .:) ; take c9 ; :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of (L .:) holds ( c9 "/\" b1 = c9 & b1 "/\" c9 = c9 ) let a9 be Element of (L .:); ::_thesis: ( c9 "/\" a9 = c9 & a9 "/\" c9 = c9 ) reconsider a = a9 as Element of L ; thus c9 "/\" a9 = c "\/" a .= c9 by A1 ; ::_thesis: a9 "/\" c9 = c9 hence a9 "/\" c9 = c9 ; ::_thesis: verum end; given c being Element of (L .:) such that A2: for a being Element of (L .:) holds ( c "/\" a = c & a "/\" c = c ) ; :: according to LATTICES:def_13 ::_thesis: L is upper-bounded reconsider c9 = c as Element of L ; take c9 ; :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds ( c9 "\/" b1 = c9 & b1 "\/" c9 = c9 ) let a9 be Element of L; ::_thesis: ( c9 "\/" a9 = c9 & a9 "\/" c9 = c9 ) reconsider a = a9 as Element of (L .:) ; thus c9 "\/" a9 = c "/\" a .= c9 by A2 ; ::_thesis: a9 "\/" c9 = c9 hence a9 "\/" c9 = c9 ; ::_thesis: verum end; theorem :: LATTICE2:50 for L being Lattice holds ( L is D_Lattice iff L .: is D_Lattice ) by Th22, Th23; theorem Th51: :: LATTICE2:51 for L being 0_Lattice holds Bottom L is_a_unity_wrt the L_join of L proof let L be 0_Lattice; ::_thesis: Bottom L is_a_unity_wrt the L_join of L now__::_thesis:_for_u_being_Element_of_L_holds_the_L_join_of_L_._((Bottom_L),u)_=_u let u be Element of L; ::_thesis: the L_join of L . ((Bottom L),u) = u thus the L_join of L . ((Bottom L),u) = (Bottom L) "\/" u .= u ; ::_thesis: verum end; hence Bottom L is_a_unity_wrt the L_join of L by BINOP_1:4; ::_thesis: verum end; registration let L be 0_Lattice; cluster the L_join of L -> having_a_unity ; coherence the L_join of L is having_a_unity proof Bottom L is_a_unity_wrt the L_join of L by Th51; hence the L_join of L is having_a_unity by SETWISEO:def_2; ::_thesis: verum end; end; theorem :: LATTICE2:52 for L being 0_Lattice holds Bottom L = the_unity_wrt the L_join of L by Th18; theorem Th53: :: LATTICE2:53 for A being non empty set for B being Finite_Subset of A for L being 0_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 0_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let L be 0_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds FinJoin (B,f) = FinJoin (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) ) set J = the L_join of L; A1: Bottom L = the_unity_wrt the L_join of L by Th18; assume A2: f | B = g | B ; ::_thesis: FinJoin (B,f) = FinJoin (B,g) now__::_thesis:_FinJoin_(B,f)_=_FinJoin_(B,g) percases ( B = {} or B <> {} ) ; supposeA3: B = {} ; ::_thesis: FinJoin (B,f) = FinJoin (B,g) hence FinJoin (B,f) = the L_join of L \$\$ (({}. A),f) .= Bottom L by A1, SETWISEO:31 .= the L_join of L \$\$ (({}. A),g) by A1, SETWISEO:31 .= FinJoin (B,g) by A3 ; ::_thesis: verum end; suppose B <> {} ; ::_thesis: FinJoin (B,f) = FinJoin (B,g) hence FinJoin (B,f) = FinJoin (B,g) by A2, Th34; ::_thesis: verum end; end; end; hence FinJoin (B,f) = FinJoin (B,g) ; ::_thesis: verum end; theorem Th54: :: LATTICE2:54 for A being non empty set for B being Finite_Subset of A for L being 0_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 0_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let L be 0_Lattice; ::_thesis: for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds f . x [= u ) holds FinJoin (B,f) [= u let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds f . x [= u ) implies FinJoin (B,f) [= u ) assume A1: for x being Element of A st x in B holds f . x [= u ; ::_thesis: FinJoin (B,f) [= u set J = the L_join of L; A2: Bottom L = the_unity_wrt the L_join of L by Th18; now__::_thesis:_FinJoin_(B,f)_[=_u percases ( B = {} or B <> {} ) ; suppose B = {} ; ::_thesis: FinJoin (B,f) [= u then FinJoin (B,f) = the L_join of L \$\$ (({}. A),f) .= Bottom L by A2, SETWISEO:31 ; hence FinJoin (B,f) [= u by LATTICES:16; ::_thesis: verum end; suppose B <> {} ; ::_thesis: FinJoin (B,f) [= u hence FinJoin (B,f) [= u by A1, Th32; ::_thesis: verum end; end; end; hence FinJoin (B,f) [= u ; ::_thesis: verum end; theorem :: LATTICE2:55 for A being non empty set for B being Finite_Subset of A for L being 0_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 0_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let B be Finite_Subset of A; ::_thesis: for L being 0_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let L be 0_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinJoin (B,f) [= FinJoin (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( ( for x being Element of A st x in B holds f . x [= g . x ) implies FinJoin (B,f) [= FinJoin (B,g) ) assume A1: for x being Element of A st x in B holds f . x [= g . x ; ::_thesis: FinJoin (B,f) [= FinJoin (B,g) now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ f_._x_[=_FinJoin_(B,g) let x be Element of A; ::_thesis: ( x in B implies f . x [= FinJoin (B,g) ) assume A2: x in B ; ::_thesis: f . x [= FinJoin (B,g) then f . x [= g . x by A1; hence f . x [= FinJoin (B,g) by A2, Th29; ::_thesis: verum end; hence FinJoin (B,f) [= FinJoin (B,g) by Th54; ::_thesis: verum end; theorem Th56: :: LATTICE2:56 for L being 1_Lattice holds Top L is_a_unity_wrt the L_meet of L proof let L be 1_Lattice; ::_thesis: Top L is_a_unity_wrt the L_meet of L now__::_thesis:_for_u_being_Element_of_L_holds_the_L_meet_of_L_._((Top_L),u)_=_u let u be Element of L; ::_thesis: the L_meet of L . ((Top L),u) = u thus the L_meet of L . ((Top L),u) = (Top L) "/\" u .= u ; ::_thesis: verum end; hence Top L is_a_unity_wrt the L_meet of L by BINOP_1:4; ::_thesis: verum end; registration let L be 1_Lattice; cluster the L_meet of L -> having_a_unity ; coherence the L_meet of L is having_a_unity proof Top L is_a_unity_wrt the L_meet of L by Th56; hence the L_meet of L is having_a_unity by SETWISEO:def_2; ::_thesis: verum end; end; theorem :: LATTICE2:57 for L being 1_Lattice holds Top L = the_unity_wrt the L_meet of L by Th19; theorem :: LATTICE2:58 for A being non empty set for B being Finite_Subset of A for L being 1_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 1_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice for f, g being Function of A, the carrier of L st f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let L be 1_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds FinMeet (B,f) = FinMeet (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) ) assume A1: f | B = g | B ; ::_thesis: FinMeet (B,f) = FinMeet (B,g) reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ; A2: FinMeet (B,g) = FinJoin (B,g9) ; ( L .: is 0_Lattice & FinMeet (B,f) = FinJoin (B,f9) ) by Th49; hence FinMeet (B,f) = FinMeet (B,g) by A1, A2, Th53; ::_thesis: verum end; theorem Th59: :: LATTICE2:59 for A being non empty set for B being Finite_Subset of A for L being 1_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 1_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let L be 1_Lattice; ::_thesis: for f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds u [= f . x ) holds u [= FinMeet (B,f) let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds u [= f . x ) implies u [= FinMeet (B,f) ) reconsider f9 = f as Function of A, the carrier of (L .:) ; reconsider u9 = u as Element of (L .:) ; assume for x being Element of A st x in B holds u [= f . x ; ::_thesis: u [= FinMeet (B,f) then A1: for x being Element of A st x in B holds f9 . x [= u9 by Th38; L .: is 0_Lattice by Th49; then FinJoin (B,f9) [= u9 by A1, Th54; hence u [= FinMeet (B,f) by Th39; ::_thesis: verum end; theorem :: LATTICE2:60 for A being non empty set for B being Finite_Subset of A for L being 1_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being 1_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let B be Finite_Subset of A; ::_thesis: for L being 1_Lattice for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let L be 1_Lattice; ::_thesis: for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds f . x [= g . x ) holds FinMeet (B,f) [= FinMeet (B,g) let f, g be Function of A, the carrier of L; ::_thesis: ( ( for x being Element of A st x in B holds f . x [= g . x ) implies FinMeet (B,f) [= FinMeet (B,g) ) assume A1: for x being Element of A st x in B holds f . x [= g . x ; ::_thesis: FinMeet (B,f) [= FinMeet (B,g) now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ FinMeet_(B,f)_[=_g_._x let x be Element of A; ::_thesis: ( x in B implies FinMeet (B,f) [= g . x ) assume A2: x in B ; ::_thesis: FinMeet (B,f) [= g . x then f . x [= g . x by A1; hence FinMeet (B,f) [= g . x by A2, Th41; ::_thesis: verum end; hence FinMeet (B,f) [= FinMeet (B,g) by Th59; ::_thesis: verum end; theorem :: LATTICE2:61 for L being 0_Lattice holds Bottom L = Top (L .:) proof let L be 0_Lattice; ::_thesis: Bottom L = Top (L .:) reconsider u = Bottom L as Element of (L .:) ; now__::_thesis:_for_v_being_Element_of_(L_.:)_holds_v_"\/"_u_=_u let v be Element of (L .:); ::_thesis: v "\/" u = u reconsider v9 = v as Element of L ; thus v "\/" u = (Bottom L) "/\" v9 by Th37 .= u ; ::_thesis: verum end; hence Bottom L = Top (L .:) by RLSUB_2:65; ::_thesis: verum end; theorem :: LATTICE2:62 for L being 1_Lattice holds Top L = Bottom (L .:) proof let L be 1_Lattice; ::_thesis: Top L = Bottom (L .:) reconsider u = Top L as Element of (L .:) ; now__::_thesis:_for_v_being_Element_of_(L_.:)_holds_v_"/\"_u_=_u let v be Element of (L .:); ::_thesis: v "/\" u = u reconsider v9 = v as Element of L ; thus v "/\" u = (Top L) "\/" v9 by Th37 .= u ; ::_thesis: verum end; hence Top L = Bottom (L .:) by RLSUB_2:64; ::_thesis: verum end; definition mode D0_Lattice is distributive lower-bounded Lattice; end; theorem :: LATTICE2:63 for L being D0_Lattice holds the L_meet of L is_distributive_wrt the L_join of L by Th23; theorem Th64: :: LATTICE2:64 for A being non empty set for B being Finite_Subset of A for L being D0_Lattice for f being Function of A, the carrier of L for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being D0_Lattice for f being Function of A, the carrier of L for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) let B be Finite_Subset of A; ::_thesis: for L being D0_Lattice for f being Function of A, the carrier of L for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) let L be D0_Lattice; ::_thesis: for f being Function of A, the carrier of L for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) let f be Function of A, the carrier of L; ::_thesis: for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) let u be Element of L; ::_thesis: the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) A1: the L_meet of L . (u,(Bottom L)) = u "/\" (Bottom L) .= Bottom L ; ( the L_meet of L is_distributive_wrt the L_join of L & Bottom L = the_unity_wrt the L_join of L ) by Th18, Th23; hence the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) by A1, SETWOP_2:12; ::_thesis: verum end; theorem :: LATTICE2:65 for A being non empty set for B being Finite_Subset of A for L being D0_Lattice for g, f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) holds u "/\" (FinJoin (B,f)) = FinJoin (B,g) proof let A be non empty set ; ::_thesis: for B being Finite_Subset of A for L being D0_Lattice for g, f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) holds u "/\" (FinJoin (B,f)) = FinJoin (B,g) let B be Finite_Subset of A; ::_thesis: for L being D0_Lattice for g, f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) holds u "/\" (FinJoin (B,f)) = FinJoin (B,g) let L be D0_Lattice; ::_thesis: for g, f being Function of A, the carrier of L for u being Element of L st ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) holds u "/\" (FinJoin (B,f)) = FinJoin (B,g) let g, f be Function of A, the carrier of L; ::_thesis: for u being Element of L st ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) holds u "/\" (FinJoin (B,f)) = FinJoin (B,g) let u be Element of L; ::_thesis: ( ( for x being Element of A st x in B holds g . x = u "/\" (f . x) ) implies u "/\" (FinJoin (B,f)) = FinJoin (B,g) ) reconsider G = ( the L_meet of L [;] (u,f)) +* (g | B) as Function of A, the carrier of L by Th3; dom (g | B) = B by Th9; then A1: G | B = g | B by FUNCT_4:23; assume A2: for x being Element of A st x in B holds g . x = u "/\" (f . x) ; ::_thesis: u "/\" (FinJoin (B,f)) = FinJoin (B,g) now__::_thesis:_for_x_being_Element_of_A_st_x_in_B_holds_ g_._x_=_(_the_L_meet_of_L_[;]_(u,f))_._x let x be Element of A; ::_thesis: ( x in B implies g . x = ( the L_meet of L [;] (u,f)) . x ) assume x in B ; ::_thesis: g . x = ( the L_meet of L [;] (u,f)) . x hence g . x = u "/\" (f . x) by A2 .= ( the L_meet of L [;] (u,f)) . x by FUNCOP_1:53 ; ::_thesis: verum end; then G = the L_meet of L [;] (u,f) by Th10; hence u "/\" (FinJoin (B,f)) = FinJoin (B,G) by Th64 .= FinJoin (B,g) by A1, Th53 ; ::_thesis: verum end; theorem :: LATTICE2:66 for A being non empty set for B being Finite_Subset of A for L being D0_Lattice for f being Function of A, the carrier of L for u being Element of L holds u "/\" (FinJoin (B,f)) = FinJoin (B,( the L_meet of L [;] (u,f))) by Th64; definition let IT be Lattice; attrIT is Heyting means :Def5: :: LATTICE2:def 5 ( IT is implicative & IT is lower-bounded ); end; :: deftheorem Def5 defines Heyting LATTICE2:def_5_:_ for IT being Lattice holds ( IT is Heyting iff ( IT is implicative & IT is lower-bounded ) ); registration cluster non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ; existence ex b1 being Lattice st b1 is Heyting proof set L = the B_Lattice; take the B_Lattice ; ::_thesis: the B_Lattice is Heyting thus ( the B_Lattice is implicative & the B_Lattice is lower-bounded ) ; :: according to LATTICE2:def_5 ::_thesis: verum end; end; registration cluster non empty Lattice-like Heyting -> lower-bounded implicative for LattStr ; coherence for b1 being Lattice st b1 is Heyting holds ( b1 is implicative & b1 is lower-bounded ) by Def5; cluster non empty Lattice-like lower-bounded implicative -> Heyting for LattStr ; coherence for b1 being Lattice st b1 is implicative & b1 is lower-bounded holds b1 is Heyting by Def5; end; definition mode H_Lattice is Heyting Lattice; end; registration cluster non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like Heyting for LattStr ; existence ex b1 being Lattice st ( b1 is Heyting & b1 is strict ) proof set L = the strict B_Lattice; the strict B_Lattice is I_Lattice ; hence ex b1 being Lattice st ( b1 is Heyting & b1 is strict ) ; ::_thesis: verum end; end; theorem :: LATTICE2:67 for L being 0_Lattice holds ( L is H_Lattice iff for x, z being Element of L ex y being Element of L st ( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds v [= y ) ) ) proof let L be 0_Lattice; ::_thesis: ( L is H_Lattice iff for x, z being Element of L ex y being Element of L st ( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds v [= y ) ) ) ( L is H_Lattice iff L is I_Lattice ) ; hence ( L is H_Lattice iff for x, z being Element of L ex y being Element of L st ( x "/\" y [= z & ( for v being Element of L st x "/\" v [= z holds v [= y ) ) ) by FILTER_0:def_6; ::_thesis: verum end; theorem :: LATTICE2:68 for L being Lattice holds ( L is finite iff L .: is finite ) ; registration cluster non empty finite Lattice-like -> lower-bounded for LattStr ; coherence for b1 being Lattice st b1 is finite holds b1 is lower-bounded proof let L be Lattice; ::_thesis: ( L is finite implies L is lower-bounded ) assume L is finite ; ::_thesis: L is lower-bounded then reconsider B = the carrier of L as Finite_Subset of the carrier of L by FINSUB_1:def_5; take c = FinMeet (B,(id the carrier of L)); :: according to LATTICES:def_13 ::_thesis: for b1 being Element of the carrier of L holds ( c "/\" b1 = c & b1 "/\" c = c ) let a be Element of L; ::_thesis: ( c "/\" a = c & a "/\" c = c ) (id the carrier of L) . a [= a by FUNCT_1:18; then A1: c [= a by Th41; hence c "/\" a = c by LATTICES:4; ::_thesis: a "/\" c = c thus a "/\" c = c by A1, LATTICES:4; ::_thesis: verum end; cluster non empty finite Lattice-like -> upper-bounded for LattStr ; coherence for b1 being Lattice st b1 is finite holds b1 is upper-bounded proof let L be Lattice; ::_thesis: ( L is finite implies L is upper-bounded ) assume L is finite ; ::_thesis: L is upper-bounded then reconsider B = the carrier of L as Finite_Subset of the carrier of L by FINSUB_1:def_5; take c = FinJoin (B,(id the carrier of L)); :: according to LATTICES:def_14 ::_thesis: for b1 being Element of the carrier of L holds ( c "\/" b1 = c & b1 "\/" c = c ) let a be Element of L; ::_thesis: ( c "\/" a = c & a "\/" c = c ) a [= (id the carrier of L) . a by FUNCT_1:18; then A2: a [= c by Th29; hence c "\/" a = c by LATTICES:def_3; ::_thesis: a "\/" c = c thus a "\/" c = c by A2, LATTICES:def_3; ::_thesis: verum end; end; registration cluster non empty finite Lattice-like -> bounded for LattStr ; coherence for b1 being Lattice st b1 is finite holds b1 is bounded ; end; registration cluster non empty finite Lattice-like distributive -> Heyting for LattStr ; coherence for b1 being Lattice st b1 is distributive & b1 is finite holds b1 is Heyting proof let L be Lattice; ::_thesis: ( L is distributive & L is finite implies L is Heyting ) assume A1: ( L is distributive & L is finite ) ; ::_thesis: L is Heyting then reconsider L = L as D0_Lattice ; set C = the carrier of L; L is implicative proof let p, q be Element of the carrier of L; :: according to FILTER_0:def_6 ::_thesis: ex b1 being Element of the carrier of L st ( p "/\" b1 [= q & ( for b2 being Element of the carrier of L holds ( not p "/\" b2 [= q or b2 [= b1 ) ) ) defpred S1[ Element of the carrier of L] means p "/\" c1 [= q; set B = { x where x is Element of the carrier of L : S1[x] } ; A2: { x where x is Element of the carrier of L : S1[x] } c= the carrier of L from FRAENKEL:sch_10(); then { x where x is Element of the carrier of L : S1[x] } is finite by A1, FINSET_1:1; then reconsider B = { x where x is Element of the carrier of L : S1[x] } as Finite_Subset of the carrier of L by A2, FINSUB_1:def_5; take r = FinJoin (B,(id the carrier of L)); ::_thesis: ( p "/\" r [= q & ( for b1 being Element of the carrier of L holds ( not p "/\" b1 [= q or b1 [= r ) ) ) A3: now__::_thesis:_for_x_being_Element_of_the_carrier_of_L_st_x_in_B_holds_ (_the_L_meet_of_L_[;]_(p,(id_the_carrier_of_L)))_._x_[=_q let x be Element of the carrier of L; ::_thesis: ( x in B implies ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q ) assume x in B ; ::_thesis: ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q then A4: ex x9 being Element of the carrier of L st ( x9 = x & p "/\" x9 [= q ) ; ( the L_meet of L [;] (p,(id the carrier of L))) . x = the L_meet of L . (p,((id the carrier of L) . x)) by FUNCOP_1:53 .= p "/\" x by FUNCT_1:18 ; hence ( the L_meet of L [;] (p,(id the carrier of L))) . x [= q by A4; ::_thesis: verum end; p "/\" r = FinJoin (B,( the L_meet of L [;] (p,(id the carrier of L)))) by Th64; hence p "/\" r [= q by A3, Th54; ::_thesis: for b1 being Element of the carrier of L holds ( not p "/\" b1 [= q or b1 [= r ) let r1 be Element of the carrier of L; ::_thesis: ( not p "/\" r1 [= q or r1 [= r ) assume p "/\" r1 [= q ; ::_thesis: r1 [= r then A5: r1 in B ; r1 = (id the carrier of L) . r1 by FUNCT_1:18; hence r1 [= r by A5, Th28; ::_thesis: verum end; hence L is Heyting ; ::_thesis: verum end; end;