:: J\'onsson Theorem
:: by Jaros{\l}aw Gryko
::
:: Received November 13, 1997
:: Copyright (c) 1997-2011 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))

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 }

proof end;

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 )

proof end;

theorem Th5: :: LATTICE5:5

for A being set
for x, y being Element of (EqRelLatt A) holds
( x [= y iff x c= y )

proof end;

theorem Th6: :: LATTICE5:6

for A being set
for a, b being Element of (EqRelLATT A) holds
( a <= b iff a c= b )

proof end;

theorem Th7: :: LATTICE5:7

for L being Lattice
for a, b being Element of (LattPOSet L) holds a "/\" b = (% a) "/\" (% b)

proof end;

theorem Th8: :: LATTICE5:8

for A being set
for a, b being Element of (EqRelLATT A) holds a "/\" b = a /\ b

proof end;

theorem Th9: :: LATTICE5:9

for L being Lattice
for a, b being Element of (LattPOSet L) holds a "\/" b = (% a) "\/" (% b)

proof 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

proof end;

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

proof end;

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

proof end;

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 Element of bool [: the carrier of L1, the carrier of L2:];
existence
ex b₁ being Function of L1,L2 st
( b₁ is meet-preserving & b₁ is join-preserving )

proof end;

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 SubRelStr of L;
existence
ex b₁ being SubRelStr of L st
( b₁ is meet-inheriting & b₁ is join-inheriting & b₁ is strict )

proof end;

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 )

proof end;

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;
pred x,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
( ( not i is even 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
( ( not i is even implies [(f . i),(f . (i + 1))] in R1 ) & ( i is even implies [(f . i),(f . (i + 1))] in R2 ) ) ) ) );

theorem :: LATTICE5:11

canceled;

theorem Th12: :: LATTICE5:12

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

proof end;

Lm1: now

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 :: LATTICE5:13

canceled;

theorem Th14: :: LATTICE5:14

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 )

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 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 b₁ 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 = b₁ + 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 = b₁ + 1 or not x,y are_joint_by F,e1,e2 ) ) ) )

proof end;

uniqueness
for b₁, b₂ 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 = b₁ + 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 = b₁ + 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 = b₂ + 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 = b₂ + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds
b₁ = b₂

proof end;

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 b₃ being Element of NAT holds
( b₃ = 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 = b₃ + 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 = b₃ + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) );

theorem Th15: :: LATTICE5:15

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

proof end;

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

proof end;

end;

definition

let A be non empty set ;
let L be 1-sorted ;
let f be BiFunction of A,L;
canceled;
attr f is symmetric means :Def6: :: LATTICE5:def 6
for x, y being Element of A holds f . (x,y) = f . (y,x);

end;

:: deftheorem LATTICE5:def 5 :
canceled;

:: deftheorem Def6 defines symmetric LATTICE5:def 6 :
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;
attr f is zeroed means :Def7: :: LATTICE5:def 7
for x being Element of A holds f . (x,x) = Bottom L;
attr f is u.t.i. means :Def8: :: LATTICE5:def 8
for x, y, z being Element of A holds (f . (x,y)) "\/" (f . (y,z)) >= f . (x,z);

end;

:: deftheorem Def7 defines zeroed 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 zeroed iff for x being Element of A holds f . (x,x) = Bottom L );

:: deftheorem Def8 defines u.t.i. LATTICE5:def 8 :
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) );

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. Element of bool [:[:A,A:], the carrier of L:];
existence
ex b₁ being BiFunction of A,L st
( b₁ is symmetric & b₁ is zeroed & b₁ is u.t.i. )

proof end;

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 :Def9: :: LATTICE5:def 9
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 b₁ being Function of L,(EqRelLATT A) st
for e being Element of L ex E being Equivalence_Relation of A st
( E = b₁ . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) )

proof end;

uniqueness
for b₁, b₂ being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b₁ . 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₂ . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines alpha LATTICE5:def 9 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for b₄ being Function of L,(EqRelLATT A) holds
( b₄ = alpha d iff for e being Element of L ex E being Equivalence_Relation of A st
( E = b₄ . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) );

theorem Th16: :: LATTICE5:16

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

proof end;

theorem Th17: :: LATTICE5:17

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

proof end;

begin

definition

let A be set ;
func new_set A -> set equals :: LATTICE5:def 10
A \/ {{A},{{A}},{{{A}}}};
correctness
coherence
A \/ {{A},{{A}},{{{A}}}} is set ;
;

end;

:: deftheorem defines new_set LATTICE5:def 10 :
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 :Def11: :: LATTICE5:def 11
( ( 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 & it . ({{{A}}},{{A}}) = q `3 & it . ({A},{{A}}) = q `4 & it . ({{A}},{A}) = q `4 & it . ({A},{{{A}}}) = (q `3) "\/" (q `4) & it . ({{{A}}},{A}) = (q `3) "\/" (q `4) & ( for u being Element of A holds
( it . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & it . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & it . (u,{{A}}) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & it . ({{A}},u) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & it . (u,{{{A}}}) = (d . (u,(q `2))) "\/" (q `4) & it . ({{{A}}},u) = (d . (u,(q `2))) "\/" (q `4) ) ) );
existence
ex b₁ being BiFunction of (new_set A),L st
( ( for u, v being Element of A holds b₁ . (u,v) = d . (u,v) ) & b₁ . ({A},{A}) = Bottom L & b₁ . ({{A}},{{A}}) = Bottom L & b₁ . ({{{A}}},{{{A}}}) = Bottom L & b₁ . ({{A}},{{{A}}}) = q `3 & b<sub>1</sub> . ({{{A}}},{{A}}) = q `3 & b₁ . ({A},{{A}}) = q `4 & b<sub>1</sub> . ({{A}},{A}) = q `4 & b₁ . ({A},{{{A}}}) = (q `3) "\/" (q `4) & b₁ . ({{{A}}},{A}) = (q `3) "\/" (q `4) & ( for u being Element of A holds
( b₁ . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b₁ . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b₁ . (u,{{A}}) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b<sub>1</sub> . ({{A}},u) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b₁ . (u,{{{A}}}) = (d . (u,(q `2))) "\/" (q `4) & b₁ . ({{{A}}},u) = (d . (u,(q `2))) "\/" (q `4) ) ) )

proof end;

uniqueness
for b₁, b₂ being BiFunction of (new_set A),L st ( for u, v being Element of A holds b₁ . (u,v) = d . (u,v) ) & b₁ . ({A},{A}) = Bottom L & b₁ . ({{A}},{{A}}) = Bottom L & b₁ . ({{{A}}},{{{A}}}) = Bottom L & b₁ . ({{A}},{{{A}}}) = q `3 & b<sub>1</sub> . ({{{A}}},{{A}}) = q `3 & b₁ . ({A},{{A}}) = q `4 & b<sub>1</sub> . ({{A}},{A}) = q `4 & b₁ . ({A},{{{A}}}) = (q `3) "\/" (q `4) & b₁ . ({{{A}}},{A}) = (q `3) "\/" (q `4) & ( for u being Element of A holds
( b₁ . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b₁ . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b₁ . (u,{{A}}) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b<sub>1</sub> . ({{A}},u) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b₁ . (u,{{{A}}}) = (d . (u,(q `2))) "\/" (q `4) & b₁ . ({{{A}}},u) = (d . (u,(q `2))) "\/" (q `4) ) ) & ( for u, v being Element of A holds b₂ . (u,v) = d . (u,v) ) & b₂ . ({A},{A}) = Bottom L & b₂ . ({{A}},{{A}}) = Bottom L & b₂ . ({{{A}}},{{{A}}}) = Bottom L & b₂ . ({{A}},{{{A}}}) = q `3 & b<sub>2</sub> . ({{{A}}},{{A}}) = q `3 & b₂ . ({A},{{A}}) = q `4 & b<sub>2</sub> . ({{A}},{A}) = q `4 & b₂ . ({A},{{{A}}}) = (q `3) "\/" (q `4) & b₂ . ({{{A}}},{A}) = (q `3) "\/" (q `4) & ( for u being Element of A holds
( b₂ . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b₂ . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b₂ . (u,{{A}}) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b<sub>2</sub> . ({{A}},u) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b₂ . (u,{{{A}}}) = (d . (u,(q `2))) "\/" (q `4) & b₂ . ({{{A}}},u) = (d . (u,(q `2))) "\/" (q `4) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines new_bi_fun LATTICE5:def 11 :
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₅ being BiFunction of (new_set A),L holds
( b₅ = new_bi_fun (d,q) iff ( ( for u, v being Element of A holds b₅ . (u,v) = d . (u,v) ) & b₅ . ({A},{A}) = Bottom L & b₅ . ({{A}},{{A}}) = Bottom L & b₅ . ({{{A}}},{{{A}}}) = Bottom L & b₅ . ({{A}},{{{A}}}) = q `3 & b<sub>5</sub> . ({{{A}}},{{A}}) = q `3 & b₅ . ({A},{{A}}) = q `4 & b<sub>5</sub> . ({{A}},{A}) = q `4 & b₅ . ({A},{{{A}}}) = (q `3) "\/" (q `4) & b₅ . ({{{A}}},{A}) = (q `3) "\/" (q `4) & ( for u being Element of A holds
( b₅ . (u,{A}) = (d . (u,(q `1))) "\/" (q `3) & b₅ . ({A},u) = (d . (u,(q `1))) "\/" (q `3) & b₅ . (u,{{A}}) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b<sub>5</sub> . ({{A}},u) = ((d . (u,(q `1))) "\/" (q `3)) "\/" (q `4) & b₅ . (u,{{{A}}}) = (d . (u,(q `2))) "\/" (q `4) & b₅ . ({{{A}}},u) = (d . (u,(q `2))) "\/" (q `4) ) ) ) );

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 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 Th19: :: LATTICE5:19

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

proof end;

theorem Th20: :: LATTICE5:20

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),(q `2)) <= (q `3) "\/" (q `4) holds
new_bi_fun (d,q) is u.t.i.

proof end;

theorem :: LATTICE5:21

canceled;

theorem Th22: :: LATTICE5:22

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)

proof end;

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 :Def12: :: LATTICE5:def 12
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 b₁ being Cardinal st b₁, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent

proof end;

uniqueness
for b₁, b₂ being Cardinal st b₁, { [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₂, { [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₁ = b₂

proof end;

end;

:: deftheorem Def12 defines DistEsti LATTICE5:def 12 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b₄ being Cardinal holds
( b₄ = DistEsti d iff b₄, { [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 Th23: :: LATTICE5:23

for A being non empty set
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;
func ConsecutiveSet (A,O) -> set means :Def13: :: LATTICE5:def 13
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 b₁ being set ex L0 being T-Sequence st
( b₁ = 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 b₁, b₂ being set st ex L0 being T-Sequence st
( b₁ = 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
( b₂ = 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
b₁ = b₂;

proof end;

end;

:: deftheorem Def13 defines ConsecutiveSet LATTICE5:def 13 :
for A being non empty set
for O being Ordinal
for b₃ being set holds
( b₃ = ConsecutiveSet (A,O) iff ex L0 being T-Sequence st
( b₃ = 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 Th24: :: LATTICE5:24

for A being non empty set holds ConsecutiveSet (A,{}) = A

proof end;

theorem Th25: :: LATTICE5:25

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

proof end;

theorem Th26: :: LATTICE5:26

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)

proof end;

registration

let A be non empty set ;
let O be Ordinal;
cluster ConsecutiveSet (A,O) -> non empty ;
coherence
not ConsecutiveSet (A,O) is empty

proof end;

end;

theorem Th27: :: LATTICE5:27

for A being non empty set
for O being Ordinal holds A c= ConsecutiveSet (A,O)

proof end;

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 :Def14: :: LATTICE5:def 14
( 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 b₁ being T-Sequence of [:A,A, the carrier of L, the carrier of L:] st
( dom b₁ is Cardinal & b₁ is one-to-one & rng b₁ = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } )

proof end;

end;

:: deftheorem Def14 defines QuadrSeq LATTICE5:def 14 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b₄ being T-Sequence of [:A,A, the carrier of L, the carrier of L:] holds
( b₄ is QuadrSeq of d iff ( dom b₄ is Cardinal & b₄ is one-to-one & rng b₄ = { [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 :Def15: :: LATTICE5:def 15
q . O;
correctness
coherence
q . O is Element of [:(ConsecutiveSet (A,O)),(ConsecutiveSet (A,O)), the carrier of L, the carrier of L:];

proof end;

end;

:: deftheorem Def15 defines Quadr LATTICE5:def 15 :
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 Th28: :: LATTICE5:28

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 )

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 ;
func BiFun (z,A,L) -> BiFunction of A,L equals :Def16: :: LATTICE5:def 16
z;
coherence
z is BiFunction of A,L by A1;

end;

:: deftheorem Def16 defines BiFun LATTICE5:def 16 :
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 :Def17: :: LATTICE5:def 17
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 b₁ being set ex L0 being T-Sequence st
( b₁ = 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 b₁, b₂ being set st ex L0 being T-Sequence st
( b₁ = 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
( b₂ = 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
b₁ = b₂;

proof end;

end;

:: deftheorem Def17 defines ConsecutiveDelta LATTICE5:def 17 :
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₆ being set holds
( b₆ = ConsecutiveDelta (q,O) iff ex L0 being T-Sequence st
( b₆ = 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 Th29: :: LATTICE5:29

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

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,(succ O)) = new_bi_fun ((BiFun ((ConsecutiveDelta (q,O)),(ConsecutiveSet (A,O)),L)),(Quadr (q,O)))

proof end;

theorem Th31: :: LATTICE5:31

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)

proof end;

theorem Th32: :: LATTICE5:32

for A being non empty set
for O1, O2 being Ordinal st O1 c= O2 holds
ConsecutiveSet (A,O1) c= ConsecutiveSet (A,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
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 Th33;

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
for q being QuadrSeq of d holds d c= ConsecutiveDelta (q,O)

proof end;

theorem Th35: :: LATTICE5:35

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)

proof end;

theorem Th36: :: LATTICE5:36

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

proof end;

theorem Th37: :: LATTICE5:37

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

proof end;

theorem Th38: :: LATTICE5:38

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.

proof end;

theorem :: LATTICE5:39

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 Th36, Th37, Th38;

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 18
ConsecutiveSet (A,(DistEsti d));
correctness
coherence
ConsecutiveSet (A,(DistEsti d)) is set ;
;

end;

:: deftheorem defines NextSet LATTICE5:def 18 :
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 19
ConsecutiveDelta (q,(DistEsti d));
correctness
coherence
ConsecutiveDelta (q,(DistEsti d)) is set ;
;

end;

:: deftheorem defines NextDelta LATTICE5:def 19 :
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 Th36, Th37, Th38;

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;
pred Aq,dq is_extension_of A,d means :Def20: :: LATTICE5:def 20
ex q being QuadrSeq of d st
( Aq = NextSet d & dq = NextDelta q );

end;

:: deftheorem Def20 defines is_extension_of LATTICE5:def 20 :
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 Th40: :: LATTICE5:40

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 )

proof end;

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 :Def21: :: LATTICE5:def 21
( 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 b₁ being Function st
( dom b₁ = NAT & b₁ . 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 & b₁ . n = [A9,d9] & b₁ . (n + 1) = [Aq,dq] ) ) )

proof end;

end;

:: deftheorem Def21 defines ExtensionSeq LATTICE5:def 21 :
for A being non empty set
for L being lower-bounded LATTICE
for d being distance_function of A,L
for b₄ being Function holds
( b₄ is ExtensionSeq of A,d iff ( dom b₄ = NAT & b₄ . 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 & b₄ . n = [A9,d9] & b₄ . (n + 1) = [Aq,dq] ) ) ) );

theorem Th41: :: LATTICE5:41

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

proof end;

theorem Th42: :: LATTICE5:42

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

proof end;

definition

let L be lower-bounded LATTICE;
func BasicDF L -> distance_function of the carrier of L,L means :Def22: :: LATTICE5:def 22
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 b₁ being distance_function of the carrier of L,L st
for x, y being Element of L holds
( ( x <> y implies b₁ . (x,y) = x "\/" y ) & ( x = y implies b₁ . (x,y) = Bottom L ) )

proof end;

uniqueness
for b₁, b₂ being distance_function of the carrier of L,L st ( for x, y being Element of L holds
( ( x <> y implies b₁ . (x,y) = x "\/" y ) & ( x = y implies b₁ . (x,y) = Bottom L ) ) ) & ( for x, y being Element of L holds
( ( x <> y implies b₂ . (x,y) = x "\/" y ) & ( x = y implies b₂ . (x,y) = Bottom L ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines BasicDF LATTICE5:def 22 :
for L being lower-bounded LATTICE
for b₂ being distance_function of the carrier of L,L holds
( b₂ = BasicDF L iff for x, y being Element of L holds
( ( x <> y implies b₂ . (x,y) = x "\/" y ) & ( x = y implies b₂ . (x,y) = Bottom L ) ) );

theorem Th43: :: LATTICE5:43

for L being lower-bounded LATTICE holds BasicDF L is onto

proof end;

Lm2: now

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:29;
hence ( j = 1 or j = 2 or j = 3 or j = 4 ) by A1; :: thesis: verum

end;

Lm3: now

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:3;
then ( m = 0 or m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by NAT_1:30;
hence ( m = 1 or m = 2 or m = 3 or m = 4 or m = 5 ) by A1, FINSEQ_1:3; :: thesis: verum

end;

Lm4: now

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:26;
then ( succ {} c= DistEsti d or DistEsti d c= {} ) by ORDINAL1:34;
hence succ {} c= DistEsti d by Th23, XBOOLE_1:3; :: thesis: verum

end;

theorem Th44: :: LATTICE5:44

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

proof end;

theorem Th45: :: LATTICE5:45

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 )

proof end;

theorem Th46: :: LATTICE5:46

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 )

proof end;

theorem :: LATTICE5:47

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 )

proof end;