:: by Jaros{\l}aw Gryko

::

:: Received November 13, 1997

:: Copyright (c) 1997-2018 Association of Mizar Users

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))

for F being Function-yielding Function st f = union (rng F) holds

dom f = union (rng (doms F))

proof end;

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 ) }

proof end;

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 }

[:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }

proof end;

:: deftheorem defines EqRelLATT LATTICE5:def 1 :

for A being set holds EqRelLATT A = LattPOSet (EqRelLatt A);

for A being set holds EqRelLATT A = LattPOSet (EqRelLatt A);

registration
end;

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

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

proof end;

definition

let L be non empty RelStr ;

( 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 ) ) )

end;
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 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 ) );

( 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 ) ) )

proof 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 ) ) );

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
end;

registration

let L1, L2 be LATTICE;

ex b_{1} being Function of L1,L2 st

( b_{1} is meet-preserving & b_{1} is join-preserving )

end;
cluster Relation-like the carrier of L1 -defined the carrier of L2 -valued Function-like quasi_total meet-preserving join-preserving for Function of ,;

existence ex b

( b

proof end;

definition

let L1, L2 be LATTICE;

mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1,L2;

end;
mode Homomorphism of L1,L2 is meet-preserving join-preserving Function of L1,L2;

registration

let L be LATTICE;

existence

ex b_{1} being SubRelStr of L st

( b_{1} is meet-inheriting & b_{1} is join-inheriting & b_{1} is strict )

end;
existence

ex b

( b

proof end;

definition
end;

registration

let L1, L2 be LATTICE;

let f be Homomorphism of L1,L2;

coherence

( Image f is meet-inheriting & Image f is join-inheriting )

end;
let f be Homomorphism of L1,L2;

coherence

( Image f is meet-inheriting & Image f is join-inheriting )

proof end;

definition

let X be non empty set ;

let f be non empty FinSequence of X;

let x, y be object ;

let R1, R2 be Relation;

end;
let f be non empty FinSequence of X;

let x, y be object ;

let R1, R2 be Relation;

:: deftheorem 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 object

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 ) ) ) ) );

for X being non empty set

for f being non empty FinSequence of X

for x, y being object

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

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

proof end;

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 )

( 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;
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

theorem Th12: :: LATTICE5:12

for X being non empty set

for x, y being object

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 )

for x, y being object

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 )

proof end;

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 object 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 ) ;

ex b_{1} being Element of NAT st

( ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 = b_{1} + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object 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 = b_{1} + 1 or not x,y are_joint_by F,e1,e2 ) ) ) )

for b_{1}, b_{2} being Element of NAT st ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 = b_{1} + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object 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 = b_{1} + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 = b_{2} + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object 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 = b_{2} + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds

b_{1} = b_{2}

end;
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 object 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 object 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 object 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 ( ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 object 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 ) ) ) );

ex b

( ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 = b

( 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 = b

proof end;

uniqueness for b

for x, y being object 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 = b

( 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 = b

for x, y being object 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 = b

( 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 = b

b

proof 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 object 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 b_{3} being Element of NAT holds

( b_{3} = type_of Y iff ( ( for e1, e2 being Equivalence_Relation of X

for x, y being object 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 = b_{3} + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being object 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 = b_{3} + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) );

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 object 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 b

( b

for x, y being object 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 = b

( 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 = b

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 object 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

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 object 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

proof end;

definition
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 func f . (x,y) -> Element of L;

coherence

f . (x,y) is Element of L

end;
let L be 1-sorted ;

let f be BiFunction of A,L;

let x, y be Element of A;

:: original: .

redefine func f . (x,y) -> Element of L;

coherence

f . (x,y) is Element of L

proof 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) );

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;

end;
let L be lower-bounded LATTICE;

let f be BiFunction of A,L;

:: 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 );

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) );

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;

ex b_{1} being BiFunction of A,L st

( b_{1} is symmetric & b_{1} is zeroed & b_{1} is u.t.i. )

end;
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 BiFunction of ,;

existence ex b

( b

proof 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;
let L be lower-bounded LATTICE;

mode distance_function of A,L is symmetric zeroed u.t.i. BiFunction of A,L;

definition

let A be non empty set ;

let L be lower-bounded LATTICE;

let d be distance_function of A,L;

ex b_{1} being Function of L,(EqRelLATT A) st

for e being Element of L ex E being Equivalence_Relation of A st

( E = b_{1} . e & ( for x, y being Element of A holds

( [x,y] in E iff d . (x,y) <= e ) ) )

for b_{1}, b_{2} being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st

( E = b_{1} . 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 = b_{2} . e & ( for x, y being Element of A holds

( [x,y] in E iff d . (x,y) <= e ) ) ) ) holds

b_{1} = b_{2}

end;
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 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 ) ) );

ex b

for e being Element of L ex E being Equivalence_Relation of A st

( E = b

( [x,y] in E iff d . (x,y) <= e ) ) )

proof end;

uniqueness for b

( E = b

( [x,y] in E iff d . (x,y) <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st

( E = b

( [x,y] in E iff d . (x,y) <= e ) ) ) ) holds

b

proof 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 b_{4} being Function of L,(EqRelLATT A) holds

( b_{4} = alpha d iff for e being Element of L ex E being Equivalence_Relation of A st

( E = b_{4} . e & ( for x, y being Element of A holds

( [x,y] in E iff d . (x,y) <= e ) ) ) );

for A being non empty set

for L being lower-bounded LATTICE

for d being distance_function of A,L

for b

( b

( E = b

( [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

for L being lower-bounded LATTICE

for d being distance_function of A,L holds alpha d is meet-preserving

proof end;

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

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

proof end;

:: deftheorem defines new_set LATTICE5:def 9 :

for A being set holds new_set A = A \/ {{A},{{A}},{{{A}}}};

for A being set holds new_set A = A \/ {{A},{{A}},{{{A}}}};

registration
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:];

ex b_{1} being BiFunction of (new_set A),L st

( ( for u, v being Element of A holds b_{1} . (u,v) = d . (u,v) ) & b_{1} . ({A},{A}) = Bottom L & b_{1} . ({{A}},{{A}}) = Bottom L & b_{1} . ({{{A}}},{{{A}}}) = Bottom L & b_{1} . ({{A}},{{{A}}}) = q `3_4 & b_{1} . ({{{A}}},{{A}}) = q `3_4 & b_{1} . ({A},{{A}}) = q `4_4 & b_{1} . ({{A}},{A}) = q `4_4 & b_{1} . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b_{1} . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds

( b_{1} . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{1} . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{1} . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{1} . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{1} . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b_{1} . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) )

for b_{1}, b_{2} being BiFunction of (new_set A),L st ( for u, v being Element of A holds b_{1} . (u,v) = d . (u,v) ) & b_{1} . ({A},{A}) = Bottom L & b_{1} . ({{A}},{{A}}) = Bottom L & b_{1} . ({{{A}}},{{{A}}}) = Bottom L & b_{1} . ({{A}},{{{A}}}) = q `3_4 & b_{1} . ({{{A}}},{{A}}) = q `3_4 & b_{1} . ({A},{{A}}) = q `4_4 & b_{1} . ({{A}},{A}) = q `4_4 & b_{1} . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b_{1} . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds

( b_{1} . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{1} . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{1} . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{1} . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{1} . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b_{1} . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) & ( for u, v being Element of A holds b_{2} . (u,v) = d . (u,v) ) & b_{2} . ({A},{A}) = Bottom L & b_{2} . ({{A}},{{A}}) = Bottom L & b_{2} . ({{{A}}},{{{A}}}) = Bottom L & b_{2} . ({{A}},{{{A}}}) = q `3_4 & b_{2} . ({{{A}}},{{A}}) = q `3_4 & b_{2} . ({A},{{A}}) = q `4_4 & b_{2} . ({{A}},{A}) = q `4_4 & b_{2} . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b_{2} . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds

( b_{2} . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{2} . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{2} . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{2} . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{2} . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b_{2} . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) holds

b_{1} = b_{2}

end;
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 ( ( 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) ) ) );

ex b

( ( for u, v being Element of A holds b

( b

proof end;

uniqueness for b

( b

( b

b

proof 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 b_{5} being BiFunction of (new_set A),L holds

( b_{5} = new_bi_fun (d,q) iff ( ( for u, v being Element of A holds b_{5} . (u,v) = d . (u,v) ) & b_{5} . ({A},{A}) = Bottom L & b_{5} . ({{A}},{{A}}) = Bottom L & b_{5} . ({{{A}}},{{{A}}}) = Bottom L & b_{5} . ({{A}},{{{A}}}) = q `3_4 & b_{5} . ({{{A}}},{{A}}) = q `3_4 & b_{5} . ({A},{{A}}) = q `4_4 & b_{5} . ({{A}},{A}) = q `4_4 & b_{5} . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b_{5} . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds

( b_{5} . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{5} . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b_{5} . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{5} . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b_{5} . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b_{5} . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) );

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 b

( b

( b

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

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

proof end;

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

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

proof end;

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.

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.

proof end;

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)

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)

proof end;

definition

let A be non empty set ;

let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

ex b_{1} being Cardinal st b_{1}, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent

for b_{1}, b_{2} being Cardinal st b_{1}, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent & b_{2}, { [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

b_{1} = b_{2}
by WELLORD2:15, CARD_1:2;

end;
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 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 ;

ex b

proof end;

uniqueness for b

b

:: 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 b_{4} being Cardinal holds

( b_{4} = DistEsti d iff b_{4}, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent );

for A being non empty set

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for b

( b

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 <> {}

for L being lower-bounded LATTICE

for d being distance_function of A,L holds DistEsti d <> {}

proof end;

definition

let A be non empty set ;

let O be Ordinal;

existence

ex b_{1} being set ex L0 being Sequence st

( b_{1} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

uniqueness

for b_{1}, b_{2} being set st ex L0 being Sequence st

( b_{1} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st

( b_{2} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) holds

b_{1} = b_{2};

end;
let O be Ordinal;

func ConsecutiveSet (A,O) -> set means :Def12: :: LATTICE5:def 12

ex L0 being Sequence st

( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

correctness ex L0 being Sequence st

( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

existence

ex b

( b

L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

uniqueness

for b

( b

L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st

( b

L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) holds

b

proof end;

:: deftheorem Def12 defines ConsecutiveSet LATTICE5:def 12 :

for A being non empty set

for O being Ordinal

for b_{3} being set holds

( b_{3} = ConsecutiveSet (A,O) iff ex L0 being Sequence st

( b_{3} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) );

for A being non empty set

for O being Ordinal

for b

( b

( b

L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) );

theorem Th22: :: LATTICE5:22

for A being non empty set

for O being Ordinal holds ConsecutiveSet (A,(succ O)) = new_set (ConsecutiveSet (A,O))

for O being Ordinal holds ConsecutiveSet (A,(succ O)) = new_set (ConsecutiveSet (A,O))

proof end;

theorem Th23: :: LATTICE5:23

for A being non empty set

for T being Sequence

for O being Ordinal st O <> 0 & 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)

for T being Sequence

for O being Ordinal st O <> 0 & 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)

proof end;

registration
end;

definition

let A be non empty set ;

let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

ex b_{1} being Sequence of [:A,A, the carrier of L, the carrier of L:] st

( dom b_{1} is Cardinal & b_{1} is one-to-one & rng b_{1} = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } )

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

mode QuadrSeq of d -> 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 ( 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 } );

ex b

( dom b

proof 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 b_{4} being Sequence of [:A,A, the carrier of L, the carrier of L:] holds

( b_{4} is QuadrSeq of d iff ( dom b_{4} is Cardinal & b_{4} is one-to-one & rng b_{4} = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ) );

for A being non empty set

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for b

( 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 ;

coherence

q . O is Element of [:(ConsecutiveSet (A,O)),(ConsecutiveSet (A,O)), the carrier of L, the carrier of L:];

end;
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 q . O;

coherence

q . O is Element of [:(ConsecutiveSet (A,O)),(ConsecutiveSet (A,O)), the carrier of L, the carrier of L:];

proof 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;

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 )

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 )

proof end;

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 ;

coherence

z is BiFunction of A,L by A1;

end;
let L be lower-bounded LATTICE;

let z be set ;

assume A1: z is BiFunction of A,L ;

coherence

z is BiFunction of A,L by A1;

:: 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;

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;

existence

ex b_{1} being set ex L0 being Sequence st

( b_{1} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

uniqueness

for b_{1}, b_{2} being set st ex L0 being Sequence st

( b_{1} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st

( b_{2} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) holds

b_{1} = b_{2};

end;
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 Sequence st

( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

correctness ex L0 being Sequence st

( it = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

existence

ex b

( b

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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) );

uniqueness

for b

( b

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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) & ex L0 being Sequence st

( b

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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) holds

b

proof 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 b_{6} being set holds

( b_{6} = ConsecutiveDelta (q,O) iff ex L0 being Sequence st

( b_{6} = last L0 & dom L0 = succ O & L0 . 0 = 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 <> 0 & C is limit_ordinal holds

L0 . C = union (rng (L0 | C)) ) ) );

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 b

( b

( b

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 <> 0 & 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,0) = d

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for q being QuadrSeq of d holds ConsecutiveDelta (q,0) = d

proof end;

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)))

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)))

proof end;

theorem Th28: :: LATTICE5:28

for A being non empty set

for L being lower-bounded LATTICE

for T being Sequence

for O being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O <> 0 & 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)

for L being lower-bounded LATTICE

for T being Sequence

for O being Ordinal

for d being BiFunction of A,L

for q being QuadrSeq of d st O <> 0 & 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)

proof end;

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)

for O1, O2 being Ordinal st O1 c= O2 holds

ConsecutiveSet (A,O1) c= ConsecutiveSet (A,O2)

proof end;

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

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

proof 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;

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;
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;

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)

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)

proof end;

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)

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)

proof end;

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

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

proof end;

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

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

proof end;

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.

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.

proof end;

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;

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;

correctness

coherence

ConsecutiveSet (A,(DistEsti d)) is set ;

;

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

correctness

coherence

ConsecutiveSet (A,(DistEsti d)) is set ;

;

:: 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));

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;

coherence

not NextSet d is empty ;

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

coherence

not NextSet d is empty ;

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;

correctness

coherence

ConsecutiveDelta (q,(DistEsti d)) is set ;

;

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

let q be QuadrSeq of d;

correctness

coherence

ConsecutiveDelta (q,(DistEsti d)) is set ;

;

:: 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));

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;
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;

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;

end;
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;

pred Aq,dq is_extension_of A,d means :: LATTICE5:def 19

ex q being QuadrSeq of d st

( Aq = NextSet d & dq = NextDelta q );

ex q being QuadrSeq of d st

( Aq = NextSet d & dq = NextDelta q );

:: deftheorem 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 ) );

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 )

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 )

proof end;

definition

let A be non empty set ;

let L be lower-bounded LATTICE;

let d be distance_function of A,L;

ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = [A,d] & ( for n being 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 & b_{1} . n = [A9,d9] & b_{1} . (n + 1) = [Aq,dq] ) ) )

end;
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 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 ( dom it = NAT & it . 0 = [A,d] & ( for n being 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] ) ) );

ex b

( dom b

( Aq,dq is_extension_of A9,d9 & b

proof 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 b_{4} being Function holds

( b_{4} is ExtensionSeq of A,d iff ( dom b_{4} = NAT & b_{4} . 0 = [A,d] & ( for n being 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 & b_{4} . n = [A9,d9] & b_{4} . (n + 1) = [Aq,dq] ) ) ) );

for A being non empty set

for L being lower-bounded LATTICE

for d being distance_function of A,L

for b

( b

( Aq,dq is_extension_of A9,d9 & b

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 Nat st k <= l holds

(S . k) `1 c= (S . l) `1

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 Nat st k <= l holds

(S . k) `1 c= (S . l) `1

proof end;

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 Nat st k <= l holds

(S . k) `2 c= (S . l) `2

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 Nat st k <= l holds

(S . k) `2 c= (S . l) `2

proof end;

definition

let L be lower-bounded LATTICE;

ex b_{1} being distance_function of the carrier of L,L st

for x, y being Element of L holds

( ( x <> y implies b_{1} . (x,y) = x "\/" y ) & ( x = y implies b_{1} . (x,y) = Bottom L ) )

for b_{1}, b_{2} being distance_function of the carrier of L,L st ( for x, y being Element of L holds

( ( x <> y implies b_{1} . (x,y) = x "\/" y ) & ( x = y implies b_{1} . (x,y) = Bottom L ) ) ) & ( for x, y being Element of L holds

( ( x <> y implies b_{2} . (x,y) = x "\/" y ) & ( x = y implies b_{2} . (x,y) = Bottom L ) ) ) holds

b_{1} = b_{2}

end;
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 for x, y being Element of L holds

( ( x <> y implies it . (x,y) = x "\/" y ) & ( x = y implies it . (x,y) = Bottom L ) );

ex b

for x, y being Element of L holds

( ( x <> y implies b

proof end;

uniqueness for b

( ( x <> y implies b

( ( x <> y implies b

b

proof end;

:: deftheorem Def21 defines BasicDF LATTICE5:def 21 :

for L being lower-bounded LATTICE

for b_{2} being distance_function of the carrier of L,L holds

( b_{2} = BasicDF L iff for x, y being Element of L holds

( ( x <> y implies b_{2} . (x,y) = x "\/" y ) & ( x = y implies b_{2} . (x,y) = Bottom L ) ) );

for L being lower-bounded LATTICE

for b

( b

( ( x <> y implies b

Lm2: now :: thesis: for j being Nat st 1 <= j & j < 5 holds

not not j = 1 & ... & not j = 4

not not j = 1 & ... & not j = 4

let j be Nat; :: thesis: ( 1 <= j & j < 5 implies not not j = 1 & ... & not j = 4 )

assume that

A1: 1 <= j and

A2: j < 5 ; :: thesis: not not j = 1 & ... & not j = 4

j < 4 + 1 by A2;

then j <= 4 by NAT_1:13;

then not not j = 0 & ... & not j = 4 by NAT_1:60;

hence not not j = 1 & ... & not j = 4 by A1; :: thesis: verum

end;
assume that

A1: 1 <= j and

A2: j < 5 ; :: thesis: not not j = 1 & ... & not j = 4

j < 4 + 1 by A2;

then j <= 4 by NAT_1:13;

then not not j = 0 & ... & not j = 4 by NAT_1:60;

hence not not j = 1 & ... & not j = 4 by A1; :: thesis: verum

Lm3: now :: thesis: for m being Element of NAT st m in Seg 5 holds

not not m = 1 & ... & not m = 5

not not m = 1 & ... & not m = 5

let m be Element of NAT ; :: thesis: ( m in Seg 5 implies not not m = 1 & ... & not m = 5 )

assume A1: m in Seg 5 ; :: thesis: not not m = 1 & ... & not m = 5

then m <= 5 by FINSEQ_1:1;

then not not m = 0 & ... & not m = 5 by NAT_1:60;

hence not not m = 1 & ... & not m = 5 by A1, FINSEQ_1:1; :: thesis: verum

end;
assume A1: m in Seg 5 ; :: thesis: not not m = 1 & ... & not m = 5

then m <= 5 by FINSEQ_1:1;

then not not m = 0 & ... & not m = 5 by NAT_1:60;

hence not not m = 1 & ... & not m = 5 by A1, FINSEQ_1:1; :: thesis: verum

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

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;
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

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

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

proof end;

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 )

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 )

proof end;

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 object 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 )

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 object 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 )

proof end;

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 )

( f is one-to-one & type_of (Image f) <= 3 )

proof end;