:: J\'onsson Theorem :: by Jaros{\l}aw Gryko :: :: Received November 13, 1997 :: Copyright (c) 1997-2012 Association of Mizar Users begin theorem Th1: :: LATTICE5:1 for f being Function for F being Function-yielding Function st f = union (rng F) holds dom f = union (rng (doms F)) proofend; theorem Th2: :: LATTICE5:2 for A, B being non empty set holds [:(union A),(union B):] = union { [:a,b:] where a is Element of A, b is Element of B : ( a in A & b in B ) } proofend; theorem Th3: :: LATTICE5:3 for A being non empty set st A is c=-linear holds [:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A } proofend; begin definition let A be set ; func EqRelLATT A -> Poset equals :: LATTICE5:def 1 LattPOSet (EqRelLatt A); correctness coherence LattPOSet (EqRelLatt A) is Poset; ; end; :: deftheorem defines EqRelLATT LATTICE5:def_1_:_ for A being set holds EqRelLATT A = LattPOSet (EqRelLatt A); registration let A be set ; cluster EqRelLATT A -> with_suprema with_infima ; coherence ( EqRelLATT A is with_infima & EqRelLATT A is with_suprema ) ; end; theorem Th4: :: LATTICE5:4 for A, x being set holds ( x in the carrier of (EqRelLATT A) iff x is Equivalence_Relation of A ) proofend; theorem Th5: :: LATTICE5:5 for A being set for x, y being Element of (EqRelLatt A) holds ( x [= y iff x c= y ) proofend; theorem Th6: :: LATTICE5:6 for A being set for a, b being Element of (EqRelLATT A) holds ( a <= b iff a c= b ) proofend; theorem Th7: :: LATTICE5:7 for L being Lattice for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b) proofend; theorem Th8: :: LATTICE5:8 for A being set for a, b being Element of (EqRelLATT A) holds a "/\" b = a /\ b proofend; theorem Th9: :: LATTICE5:9 for L being Lattice for a, b being Element of (LattPOSet L) holds a "\/" b = (% a) "\/" (% b) proofend; theorem Th10: :: LATTICE5:10 for A being set for a, b being Element of (EqRelLATT A) for E1, E2 being Equivalence_Relation of A st a = E1 & b = E2 holds a "\/" b = E1 "\/" E2 proofend; definition let L be non empty RelStr ; redefine attr L is complete means :: LATTICE5:def 2 for X being Subset of L ex a being Element of L st ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds b <= a ) ); compatibility ( L is complete iff for X being Subset of L ex a being Element of L st ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds b <= a ) ) ) proofend; end; :: deftheorem defines complete LATTICE5:def_2_:_ for L being non empty RelStr holds ( L is complete iff for X being Subset of L ex a being Element of L st ( a is_<=_than X & ( for b being Element of L st b is_<=_than X holds b <= a ) ) ); registration let A be set ; cluster EqRelLATT A -> complete ; coherence EqRelLATT A is complete proofend; end; begin registration let L1, L2 be LATTICE; cluster Relation-like the carrier of L1 -defined the carrier of L2 -valued Function-like quasi_total meet-preserving join-preserving for Element of bool [: the carrier of L1, the carrier of L2:]; existence ex b1 being Function of L1,L2 st ( b1 is meet-preserving & b1 is join-preserving ) proofend; end; definition let L1, L2 be LATTICE; mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1,L2; end; registration let L be LATTICE; cluster strict meet-inheriting join-inheriting for SubRelStr of L; existence ex b1 being SubRelStr of L st ( b1 is meet-inheriting & b1 is join-inheriting & b1 is strict ) proofend; end; definition let L be non empty RelStr ; mode Sublattice of L is meet-inheriting join-inheriting SubRelStr of L; end; registration let L1, L2 be LATTICE; let f be Homomorphism of L1,L2; cluster Image f -> meet-inheriting join-inheriting ; coherence ( Image f is meet-inheriting & Image f is join-inheriting ) proofend; end; definition let X be non empty set ; let f be non empty FinSequence of X; let x, y be set ; let R1, R2 be Relation; predx,y are_joint_by f,R1,R2 means :Def3: :: LATTICE5:def 3 ( f . 1 = x & f . (len f) = y & ( for i being Element of NAT st 1 <= i & i < len f holds ( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ); end; :: deftheorem Def3 defines are_joint_by LATTICE5:def_3_:_ for X being non empty set for f being non empty FinSequence of X for x, y being set for R1, R2 being Relation holds ( x,y are_joint_by f,R1,R2 iff ( f . 1 = x & f . (len f) = y & ( for i being Element of NAT st 1 <= i & i < len f holds ( ( i is odd implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ) ); theorem Th11: :: LATTICE5:11 for X being non empty set for x being set for o being Element of NAT for R1, R2 being Relation for f being non empty FinSequence of X st R1 is_reflexive_in X & R2 is_reflexive_in X & f = o |-> x holds x,x are_joint_by f,R1,R2 proofend; Lm1: now__::_thesis:_for_i,_n,_m_being_Element_of_NAT_st_1_<=_i_&_i_<_n_+_m_&_not_(_1_<=_i_&_i_<_n_)_&_not_(_n_=_i_&_i_<_n_+_m_)_holds_ (_n_+_1_<=_i_&_i_<_n_+_m_) let i, n, m be Element of NAT ; ::_thesis: ( 1 <= i & i < n + m & not ( 1 <= i & i < n ) & not ( n = i & i < n + m ) implies ( n + 1 <= i & i < n + m ) ) assume ( 1 <= i & i < n + m ) ; ::_thesis: ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) ) then ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n < i & i < n + m ) ) by XXREAL_0:1; hence ( ( 1 <= i & i < n ) or ( n = i & i < n + m ) or ( n + 1 <= i & i < n + m ) ) by NAT_1:13; ::_thesis: verum end; theorem Th12: :: LATTICE5:12 for X being non empty set for x, y being set for R1, R2 being Relation for n, m being Element of NAT st n <= m & R1 is_reflexive_in X & R2 is_reflexive_in X & ex f being non empty FinSequence of X st ( len f = n & x,y are_joint_by f,R1,R2 ) holds ex h being non empty FinSequence of X st ( len h = m & x,y are_joint_by h,R1,R2 ) proofend; definition let X be non empty set ; let Y be Sublattice of EqRelLATT X; given e being Equivalence_Relation of X such that A1: e in the carrier of Y and A2: e <> id X ; given o being Element of NAT such that A3: for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = o & x,y are_joint_by F,e1,e2 ) ; func type_of Y -> Element of NAT means :Def4: :: LATTICE5:def 4 ( ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = it + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds ( not len F = it + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ); existence ex b1 being Element of NAT st ( ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds ( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) proofend; uniqueness for b1, b2 being Element of NAT st ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds ( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = b2 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds ( not len F = b2 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines type_of LATTICE5:def_4_:_ for X being non empty set for Y being Sublattice of EqRelLATT X st ex e being Equivalence_Relation of X st ( e in the carrier of Y & e <> id X ) & ex o being Element of NAT st for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = o & x,y are_joint_by F,e1,e2 ) holds for b3 being Element of NAT holds ( b3 = type_of Y iff ( ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = b3 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st ( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds ( not len F = b3 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) ); theorem Th13: :: LATTICE5:13 for X being non empty set for Y being Sublattice of EqRelLATT X for n being Element of NAT st ex e being Equivalence_Relation of X st ( e in the carrier of Y & e <> id X ) & ( for e1, e2 being Equivalence_Relation of X for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of X st ( len F = n + 2 & x,y are_joint_by F,e1,e2 ) ) holds type_of Y <= n proofend; begin definition let A be set ; let L be 1-sorted ; mode BiFunction of A,L is Function of [:A,A:], the carrier of L; end; definition let A be non empty set ; let L be 1-sorted ; let f be BiFunction of A,L; let x, y be Element of A; :: original:. redefine funcf . (x,y) -> Element of L; coherence f . (x,y) is Element of L proofend; end; definition let A be non empty set ; let L be 1-sorted ; let f be BiFunction of A,L; attrf is symmetric means :Def5: :: LATTICE5:def 5 for x, y being Element of A holds f . (x,y) = f . (y,x); end; :: deftheorem Def5 defines symmetric LATTICE5:def_5_:_ for A being non empty set for L being 1-sorted for f being BiFunction of A,L holds ( f is symmetric iff for x, y being Element of A holds f . (x,y) = f . (y,x) ); definition let A be non empty set ; let L be lower-bounded LATTICE; let f be BiFunction of A,L; attrf is zeroed means :Def6: :: LATTICE5:def 6 for x being Element of A holds f . (x,x) = Bottom L; attrf is u.t.i. means :Def7: :: LATTICE5:def 7 for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z); end; :: deftheorem Def6 defines zeroed LATTICE5:def_6_:_ for A being non empty set for L being lower-bounded LATTICE for f being BiFunction of A,L holds ( f is zeroed iff for x being Element of A holds f . (x,x) = Bottom L ); :: deftheorem Def7 defines u.t.i. LATTICE5:def_7_:_ for A being non empty set for L being lower-bounded LATTICE for f being BiFunction of A,L holds ( f is u.t.i. iff for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z) ); :: f is u.t.i. means that f satisfies the triangle inequality registration let A be non empty set ; let L be lower-bounded LATTICE; cluster Relation-like [:A,A:] -defined the carrier of L -valued Function-like quasi_total symmetric zeroed u.t.i. for Element of bool [:[:A,A:], the carrier of L:]; existence ex b1 being BiFunction of A,L st ( b1 is symmetric & b1 is zeroed & b1 is u.t.i. ) proofend; end; definition let A be non empty set ; let L be lower-bounded LATTICE; mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L; end; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be distance_function of A,L; func alpha d -> Function of L,(EqRelLATT A) means :Def8: :: LATTICE5:def 8 for e being Element of L ex E being Equivalence_Relation of A st ( E = it . e & ( for x, y being Element of A holds ( [x,y] in E iff d . (x,y) <= e ) ) ); existence ex b1 being Function of L,(EqRelLATT A) st for e being Element of L ex E being Equivalence_Relation of A st ( E = b1 . e & ( for x, y being Element of A holds ( [x,y] in E iff d . (x,y) <= e ) ) ) proofend; uniqueness for b1, b2 being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st ( E = b1 . e & ( for x, y being Element of A holds ( [x,y] in E iff d . (x,y) <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st ( E = b2 . e & ( for x, y being Element of A holds ( [x,y] in E iff d . (x,y) <= e ) ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines alpha LATTICE5:def_8_:_ for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for b4 being Function of L,(EqRelLATT A) holds ( b4 = alpha d iff for e being Element of L ex E being Equivalence_Relation of A st ( E = b4 . e & ( for x, y being Element of A holds ( [x,y] in E iff d . (x,y) <= e ) ) ) ); theorem Th14: :: LATTICE5:14 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L holds alpha d is meet-preserving proofend; theorem Th15: :: LATTICE5:15 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L st d is onto holds alpha d is one-to-one proofend; begin definition let A be set ; func new_set A -> set equals :: LATTICE5:def 9 A \/ {{A},{{A}},{{{A}}}}; correctness coherence A \/ {{A},{{A}},{{{A}}}} is set ; ; end; :: deftheorem defines new_set LATTICE5:def_9_:_ for A being set holds new_set A = A \/ {{A},{{A}},{{{A}}}}; registration let A be set ; cluster new_set A -> non empty ; coherence not new_set A is empty ; end; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be Element of [:A,A, the carrier of L, the carrier of L:]; func new_bi_fun (d,q) -> BiFunction of (new_set A),L means :Def10: :: LATTICE5:def 10 ( ( for u, v being Element of A holds it . (u,v) = d . (u,v) ) & it . ({A},{A}) = Bottom L & it . ({{A}},{{A}}) = Bottom L & it . ({{{A}}},{{{A}}}) = Bottom L & it . ({{A}},{{{A}}}) = q `3_4 & it . ({{{A}}},{{A}}) = q `3_4 & it . ({A},{{A}}) = q `4_4 & it . ({{A}},{A}) = q `4_4 & it . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & it . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds ( it . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & it . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & it . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & it . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & it . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & it . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ); existence ex b1 being BiFunction of (new_set A),L st ( ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({{{A}}},{{{A}}}) = Bottom L & b1 . ({{A}},{{{A}}}) = q `3_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds ( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) proofend; uniqueness for b1, b2 being BiFunction of (new_set A),L st ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({{{A}}},{{{A}}}) = Bottom L & b1 . ({{A}},{{{A}}}) = q `3_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds ( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) & ( for u, v being Element of A holds b2 . (u,v) = d . (u,v) ) & b2 . ({A},{A}) = Bottom L & b2 . ({{A}},{{A}}) = Bottom L & b2 . ({{{A}}},{{{A}}}) = Bottom L & b2 . ({{A}},{{{A}}}) = q `3_4 & b2 . ({{{A}}},{{A}}) = q `3_4 & b2 . ({A},{{A}}) = q `4_4 & b2 . ({{A}},{A}) = q `4_4 & b2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b2 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds ( b2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) holds b1 = b2 proofend; end; :: deftheorem Def10 defines new_bi_fun LATTICE5:def_10_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being Element of [:A,A, the carrier of L, the carrier of L:] for b5 being BiFunction of (new_set A),L holds ( b5 = new_bi_fun (d,q) iff ( ( for u, v being Element of A holds b5 . (u,v) = d . (u,v) ) & b5 . ({A},{A}) = Bottom L & b5 . ({{A}},{{A}}) = Bottom L & b5 . ({{{A}}},{{{A}}}) = Bottom L & b5 . ({{A}},{{{A}}}) = q `3_4 & b5 . ({{{A}}},{{A}}) = q `3_4 & b5 . ({A},{{A}}) = q `4_4 & b5 . ({{A}},{A}) = q `4_4 & b5 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b5 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds ( b5 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b5 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) ); theorem Th16: :: LATTICE5:16 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is zeroed holds for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is zeroed proofend; theorem Th17: :: LATTICE5:17 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is symmetric holds for q being Element of [:A,A, the carrier of L, the carrier of L:] holds new_bi_fun (d,q) is symmetric proofend; theorem Th18: :: LATTICE5:18 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds for q being Element of [:A,A, the carrier of L, the carrier of L:] st d . ((q `1_4),(q `2_4)) <= (q `3_4) "\/" (q `4_4) holds new_bi_fun (d,q) is u.t.i. proofend; theorem Th19: :: LATTICE5:19 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being Element of [:A,A, the carrier of L, the carrier of L:] holds d c= new_bi_fun (d,q) proofend; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; func DistEsti d -> Cardinal means :Def11: :: LATTICE5:def 11 it, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent ; existence ex b1 being Cardinal st b1, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent proofend; uniqueness for b1, b2 being Cardinal st b1, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent & b2, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent holds b1 = b2 proofend; end; :: deftheorem Def11 defines DistEsti LATTICE5:def_11_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for b4 being Cardinal holds ( b4 = DistEsti d iff b4, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent ); theorem Th20: :: LATTICE5:20 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L holds DistEsti d <> {} proofend; definition let A be non empty set ; let O be Ordinal; func ConsecutiveSet (A,O) -> set means :Def12: :: LATTICE5:def 12 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) holds b1 = b2; proofend; end; :: deftheorem Def12 defines ConsecutiveSet LATTICE5:def_12_:_ for A being non empty set for O being Ordinal for b3 being set holds ( b3 = ConsecutiveSet (A,O) iff ex L0 being T-Sequence st ( b3 = last L0 & dom L0 = succ O & L0 . {} = A & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) ); theorem Th21: :: LATTICE5:21 for A being non empty set holds ConsecutiveSet (A,{}) = A proofend; theorem Th22: :: LATTICE5:22 for A being non empty set for O being Ordinal holds ConsecutiveSet (A,(succ O)) = new_set (ConsecutiveSet (A,O)) proofend; theorem Th23: :: LATTICE5:23 for A being non empty set for T being T-Sequence for O being Ordinal st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds T . O1 = ConsecutiveSet (A,O1) ) holds ConsecutiveSet (A,O) = union (rng T) proofend; registration let A be non empty set ; let O be Ordinal; cluster ConsecutiveSet (A,O) -> non empty ; coherence not ConsecutiveSet (A,O) is empty proofend; end; theorem Th24: :: LATTICE5:24 for A being non empty set for O being Ordinal holds A c= ConsecutiveSet (A,O) proofend; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; mode QuadrSeq of d -> T-Sequence of [:A,A, the carrier of L, the carrier of L:] means :Def13: :: LATTICE5:def 13 ( dom it is Cardinal & it is one-to-one & rng it = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ); existence ex b1 being T-Sequence of [:A,A, the carrier of L, the carrier of L:] st ( dom b1 is Cardinal & b1 is one-to-one & rng b1 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ) proofend; end; :: deftheorem Def13 defines QuadrSeq LATTICE5:def_13_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for b4 being T-Sequence of [:A,A, the carrier of L, the carrier of L:] holds ( b4 is QuadrSeq of d iff ( dom b4 is Cardinal & b4 is one-to-one & rng b4 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ) ); definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; assume A1: O in dom q ; func Quadr (q,O) -> Element of [:(ConsecutiveSet (A,O)),(ConsecutiveSet (A,O)), the carrier of L, the carrier of L:] equals :Def14: :: LATTICE5:def 14 q . O; correctness coherence q . O is Element of [:(ConsecutiveSet (A,O)),(ConsecutiveSet (A,O)), the carrier of L, the carrier of L:]; proofend; end; :: deftheorem Def14 defines Quadr LATTICE5:def_14_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for O being Ordinal st O in dom q holds Quadr (q,O) = q . O; theorem Th25: :: LATTICE5:25 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d holds ( O in DistEsti d iff O in dom q ) proofend; definition let A be non empty set ; let L be lower-bounded LATTICE; let z be set ; assume A1: z is BiFunction of A,L ; func BiFun (z,A,L) -> BiFunction of A,L equals :Def15: :: LATTICE5:def 15 z; coherence z is BiFunction of A,L by A1; end; :: deftheorem Def15 defines BiFun LATTICE5:def_15_:_ for A being non empty set for L being lower-bounded LATTICE for z being set st z is BiFunction of A,L holds BiFun (z,A,L) = z; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; func ConsecutiveDelta (q,O) -> set means :Def16: :: LATTICE5:def 16 ex L0 being T-Sequence st ( it = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); correctness existence ex b1 being set ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ); uniqueness for b1, b2 being set st ex L0 being T-Sequence st ( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st ( b2 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) holds b1 = b2; proofend; end; :: deftheorem Def16 defines ConsecutiveDelta LATTICE5:def_16_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d for O being Ordinal for b6 being set holds ( b6 = ConsecutiveDelta (q,O) iff ex L0 being T-Sequence st ( b6 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds L0 . C = union (rng (L0 | C)) ) ) ); theorem Th26: :: LATTICE5:26 for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta (q,{}) = d proofend; theorem Th27: :: LATTICE5:27 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta (q,(succ O)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O)),(ConsecutiveSet (A,O)),L)),(Quadr (q,O))) proofend; theorem Th28: :: LATTICE5:28 for A being non empty set for L being lower-bounded LATTICE for T being T-Sequence for O being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d st O <> {} & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds T . O1 = ConsecutiveDelta (q,O1) ) holds ConsecutiveDelta (q,O) = union (rng T) proofend; theorem Th29: :: LATTICE5:29 for A being non empty set for O1, O2 being Ordinal st O1 c= O2 holds ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2) proofend; theorem Th30: :: LATTICE5:30 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L proofend; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; let O be Ordinal; :: original:ConsecutiveDelta redefine func ConsecutiveDelta (q,O) -> BiFunction of (ConsecutiveSet (A,O)),L; coherence ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L by Th30; end; theorem Th31: :: LATTICE5:31 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O) proofend; theorem Th32: :: LATTICE5:32 for A being non empty set for L being lower-bounded LATTICE for O1, O2 being Ordinal for d being BiFunction of A,L for q being QuadrSeq of d st O1 c= O2 holds ConsecutiveDelta (q,O1) c= ConsecutiveDelta (q,O2) proofend; theorem Th33: :: LATTICE5:33 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L st d is zeroed holds for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is zeroed proofend; theorem Th34: :: LATTICE5:34 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L st d is symmetric holds for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is symmetric proofend; theorem Th35: :: LATTICE5:35 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds for q being QuadrSeq of d st O c= DistEsti d holds ConsecutiveDelta (q,O) is u.t.i. proofend; theorem :: LATTICE5:36 for A being non empty set for L being lower-bounded LATTICE for O being Ordinal for d being distance_function of A,L for q being QuadrSeq of d st O c= DistEsti d holds ConsecutiveDelta (q,O) is distance_function of (ConsecutiveSet (A,O)),L by Th33, Th34, Th35; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; func NextSet d -> set equals :: LATTICE5:def 17 ConsecutiveSet (A,(DistEsti d)); correctness coherence ConsecutiveSet (A,(DistEsti d)) is set ; ; end; :: deftheorem defines NextSet LATTICE5:def_17_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L holds NextSet d = ConsecutiveSet (A,(DistEsti d)); registration let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; cluster NextSet d -> non empty ; coherence not NextSet d is empty ; end; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be BiFunction of A,L; let q be QuadrSeq of d; func NextDelta q -> set equals :: LATTICE5:def 18 ConsecutiveDelta (q,(DistEsti d)); correctness coherence ConsecutiveDelta (q,(DistEsti d)) is set ; ; end; :: deftheorem defines NextDelta LATTICE5:def_18_:_ for A being non empty set for L being lower-bounded LATTICE for d being BiFunction of A,L for q being QuadrSeq of d holds NextDelta q = ConsecutiveDelta (q,(DistEsti d)); definition let A be non empty set ; let L be lower-bounded LATTICE; let d be distance_function of A,L; let q be QuadrSeq of d; :: original:NextDelta redefine func NextDelta q -> distance_function of (NextSet d),L; coherence NextDelta q is distance_function of (NextSet d),L by Th33, Th34, Th35; end; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be distance_function of A,L; let Aq be non empty set ; let dq be distance_function of Aq,L; predAq,dq is_extension_of A,d means :Def19: :: LATTICE5:def 19 ex q being QuadrSeq of d st ( Aq = NextSet d & dq = NextDelta q ); end; :: deftheorem Def19 defines is_extension_of LATTICE5:def_19_:_ for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for Aq being non empty set for dq being distance_function of Aq,L holds ( Aq,dq is_extension_of A,d iff ex q being QuadrSeq of d st ( Aq = NextSet d & dq = NextDelta q ) ); theorem Th37: :: LATTICE5:37 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for Aq being non empty set for dq being distance_function of Aq,L st Aq,dq is_extension_of A,d holds for x, y being Element of A for a, b being Element of L st d . (x,y) <= a "\/" b holds ex z1, z2, z3 being Element of Aq st ( dq . (x,z1) = a & dq . (z2,z3) = a & dq . (z1,z2) = b & dq . (z3,y) = b ) proofend; definition let A be non empty set ; let L be lower-bounded LATTICE; let d be distance_function of A,L; mode ExtensionSeq of A,d -> Function means :Def20: :: LATTICE5:def 20 ( dom it = NAT & it . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) ); existence ex b1 being Function st ( dom b1 = NAT & b1 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension_of A9,d9 & b1 . n = [A9,d9] & b1 . (n + 1) = [Aq,dq] ) ) ) proofend; end; :: deftheorem Def20 defines ExtensionSeq LATTICE5:def_20_:_ for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for b4 being Function holds ( b4 is ExtensionSeq of A,d iff ( dom b4 = NAT & b4 . 0 = [A,d] & ( for n being Element of NAT ex A9 being non empty set ex d9 being distance_function of A9,L ex Aq being non empty set ex dq being distance_function of Aq,L st ( Aq,dq is_extension_of A9,d9 & b4 . n = [A9,d9] & b4 . (n + 1) = [Aq,dq] ) ) ) ); theorem Th38: :: LATTICE5:38 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for S being ExtensionSeq of A,d for k, l being Element of NAT st k <= l holds (S . k) `1 c= (S . l) `1 proofend; theorem Th39: :: LATTICE5:39 for A being non empty set for L being lower-bounded LATTICE for d being distance_function of A,L for S being ExtensionSeq of A,d for k, l being Element of NAT st k <= l holds (S . k) `2 c= (S . l) `2 proofend; definition let L be lower-bounded LATTICE; func BasicDF L -> distance_function of the carrier of L,L means :Def21: :: LATTICE5:def 21 for x, y being Element of L holds ( ( x <> y implies it . (x,y) = x "\/" y ) & ( x = y implies it . (x,y) = Bottom L ) ); existence ex b1 being distance_function of the carrier of L,L st for x, y being Element of L holds ( ( x <> y implies b1 . (x,y) = x "\/" y ) & ( x = y implies b1 . (x,y) = Bottom L ) ) proofend; uniqueness for b1, b2 being distance_function of the carrier of L,L st ( for x, y being Element of L holds ( ( x <> y implies b1 . (x,y) = x "\/" y ) & ( x = y implies b1 . (x,y) = Bottom L ) ) ) & ( for x, y being Element of L holds ( ( x <> y implies b2 . (x,y) = x "\/" y ) & ( x = y implies b2 . (x,y) = Bottom L ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def21 defines BasicDF LATTICE5:def_21_:_ for L being lower-bounded LATTICE for b2 being distance_function of the carrier of L,L holds ( b2 = BasicDF L iff for x, y being Element of L holds ( ( x <> y implies b2 . (x,y) = x "\/" y ) & ( x = y implies b2 . (x,y) = Bottom L ) ) ); theorem Th40: :: LATTICE5:40 for L being lower-bounded LATTICE holds BasicDF L is onto proofend; Lm2: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<_5_&_not_j_=_1_&_not_j_=_2_&_not_j_=_3_holds_ j_=_4 let j be Element of NAT ; ::_thesis: ( 1 <= j & j < 5 & not j = 1 & not j = 2 & not j = 3 implies j = 4 ) assume that A1: 1 <= j and A2: j < 5 ; ::_thesis: ( j = 1 or j = 2 or j = 3 or j = 4 ) j < 4 + 1 by A2; then j <= 4 by NAT_1:13; then ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:28; hence ( j = 1 or j = 2 or j = 3 or j = 4 ) by A1; ::_thesis: verum end; Lm3: now__::_thesis:_for_m_being_Element_of_NAT_holds_ (_not_m_in_Seg_5_or_m_=_1_or_m_=_2_or_m_=_3_or_m_=_4_or_m_=_5_) let m be Element of NAT ; ::_thesis: ( not m in Seg 5 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) assume A1: m in Seg 5 ; ::_thesis: ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) then m <= 5 by FINSEQ_1:1; then ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by NAT_1:29; hence ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by A1, FINSEQ_1:1; ::_thesis: verum end; Lm4: now__::_thesis:_for_A_being_non_empty_set_ for_L_being_lower-bounded_LATTICE for_d_being_distance_function_of_A,L_holds_succ_{}_c=_DistEsti_d let A be non empty set ; ::_thesis: for L being lower-bounded LATTICE for d being distance_function of A,L holds succ {} c= DistEsti d let L be lower-bounded LATTICE; ::_thesis: for d being distance_function of A,L holds succ {} c= DistEsti d let d be distance_function of A,L; ::_thesis: succ {} c= DistEsti d ( succ {} c= DistEsti d or DistEsti d in succ {} ) by ORDINAL1:16; then ( succ {} c= DistEsti d or DistEsti d c= {} ) by ORDINAL1:22; hence succ {} c= DistEsti d by Th20, XBOOLE_1:3; ::_thesis: verum end; theorem Th41: :: LATTICE5:41 for L being lower-bounded LATTICE for S being ExtensionSeq of the carrier of L, BasicDF L for FS being non empty set st FS = union { ((S . i) `1) where i is Element of NAT : verum } holds union { ((S . i) `2) where i is Element of NAT : verum } is distance_function of FS,L proofend; theorem Th42: :: LATTICE5:42 for L being lower-bounded LATTICE for S being ExtensionSeq of the carrier of L, BasicDF L for FS being non empty set for FD being distance_function of FS,L for x, y being Element of FS for a, b being Element of L st FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & FD . (x,y) <= a "\/" b holds ex z1, z2, z3 being Element of FS st ( FD . (x,z1) = a & FD . (z2,z3) = a & FD . (z1,z2) = b & FD . (z3,y) = b ) proofend; theorem Th43: :: LATTICE5:43 for L being lower-bounded LATTICE for S being ExtensionSeq of the carrier of L, BasicDF L for FS being non empty set for FD being distance_function of FS,L for f being Homomorphism of L,(EqRelLATT FS) for x, y being Element of FS for e1, e2 being Equivalence_Relation of FS for x, y being set st f = alpha FD & FS = union { ((S . i) `1) where i is Element of NAT : verum } & FD = union { ((S . i) `2) where i is Element of NAT : verum } & e1 in the carrier of (Image f) & e2 in the carrier of (Image f) & [x,y] in e1 "\/" e2 holds ex F being non empty FinSequence of FS st ( len F = 3 + 2 & x,y are_joint_by F,e1,e2 ) proofend; :: [WP: ] Jonsson_Theorem_for_lattices theorem :: LATTICE5:44 for L being lower-bounded LATTICE ex A being non empty set ex f being Homomorphism of L,(EqRelLATT A) st ( f is one-to-one & type_of (Image f) <= 3 ) proofend;