:: by Mariusz {\L}api\'nski

::

:: Received June 29, 2000

:: Copyright (c) 2000-2016 Association of Mizar Users

definition

let L be RelStr ;

end;
attr L is finitely_typed means :Def1: :: LATTICE8:def 1

ex A being non empty set st

( ( for e being object st e in the carrier of L holds

e is Equivalence_Relation of A ) & ex o being Element of NAT st

for e1, e2 being Equivalence_Relation of A

for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of A st

( len F = o & x,y are_joint_by F,e1,e2 ) );

ex A being non empty set st

( ( for e being object st e in the carrier of L holds

e is Equivalence_Relation of A ) & ex o being Element of NAT st

for e1, e2 being Equivalence_Relation of A

for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of A st

( len F = o & x,y are_joint_by F,e1,e2 ) );

:: deftheorem Def1 defines finitely_typed LATTICE8:def 1 :

for L being RelStr holds

( L is finitely_typed iff ex A being non empty set st

( ( for e being object st e in the carrier of L holds

e is Equivalence_Relation of A ) & ex o being Element of NAT st

for e1, e2 being Equivalence_Relation of A

for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of A st

( len F = o & x,y are_joint_by F,e1,e2 ) ) );

for L being RelStr holds

( L is finitely_typed iff ex A being non empty set st

( ( for e being object st e in the carrier of L holds

e is Equivalence_Relation of A ) & ex o being Element of NAT st

for e1, e2 being Equivalence_Relation of A

for x, y being object st e1 in the carrier of L & e2 in the carrier of L & [x,y] in e1 "\/" e2 holds

ex F being non empty FinSequence of A st

( len F = o & x,y are_joint_by F,e1,e2 ) ) );

definition

let L be lower-bounded LATTICE;

let n be Element of NAT ;

end;
let n be Element of NAT ;

pred L has_a_representation_of_type<= n means :: LATTICE8:def 2

ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st

( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st

( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n );

ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st

( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st

( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n );

:: deftheorem defines has_a_representation_of_type<= LATTICE8:def 2 :

for L being lower-bounded LATTICE

for n being Element of NAT holds

( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st

( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st

( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n ) );

for L being lower-bounded LATTICE

for n being Element of NAT holds

( L has_a_representation_of_type<= n iff ex A being non trivial set ex f being Homomorphism of L,(EqRelLATT A) st

( f is V17() & Image f is finitely_typed & ex e being Equivalence_Relation of A st

( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= n ) );

registration

ex b_{1} being LATTICE st

( b_{1} is lower-bounded & b_{1} is distributive & b_{1} is finite )
end;

cluster non empty finite reflexive transitive antisymmetric lower-bounded distributive with_suprema with_infima for RelStr ;

existence ex b

( b

proof end;

Lm1: 1 is odd

proof end;

Lm2: 2 is even

proof end;

registration

let A be non trivial set ;

ex b_{1} being non empty Sublattice of EqRelLATT A st

( not b_{1} is trivial & b_{1} is finitely_typed & b_{1} is full )

end;
cluster non empty non trivial full meet-inheriting join-inheriting finitely_typed for SubRelStr of EqRelLATT A;

existence ex b

( not b

proof end;

theorem Th1: :: LATTICE8:1

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

proof end;

theorem :: LATTICE8:3

for A being non empty set

for L being non empty Sublattice of EqRelLATT A holds

( L is trivial or ex e being Equivalence_Relation of A st

( e in the carrier of L & e <> id A ) )

for L being non empty Sublattice of EqRelLATT A holds

( L is trivial or ex e being Equivalence_Relation of A st

( e in the carrier of L & e <> id A ) )

proof end;

theorem :: LATTICE8:4

for L1, L2 being lower-bounded LATTICE

for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds

( f is meet-preserving & f is join-preserving ) ;

for f being Function of L1,L2 st f is infs-preserving & f is sups-preserving holds

( f is meet-preserving & f is join-preserving ) ;

theorem Th6: :: LATTICE8:6

for S being non empty lower-bounded Poset

for T being non empty Poset

for f being monotone Function of S,T holds Image f is lower-bounded

for T being non empty Poset

for f being monotone Function of S,T holds Image f is lower-bounded

proof end;

theorem Th7: :: LATTICE8:7

for L being lower-bounded LATTICE

for x, y being Element of L

for A being non empty set

for f being Homomorphism of L,(EqRelLATT A) st f is V17() & (corestr f) . x <= (corestr f) . y holds

x <= y

for x, y being Element of L

for A being non empty set

for f being Homomorphism of L,(EqRelLATT A) st f is V17() & (corestr f) . x <= (corestr f) . y holds

x <= y

proof end;

theorem Th8: :: LATTICE8:8

for A being non trivial set

for L being non empty full finitely_typed Sublattice of EqRelLATT A

for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds

L is modular

for L being non empty full finitely_typed Sublattice of EqRelLATT A

for e being Equivalence_Relation of A st e in the carrier of L & e <> id A & type_of L <= 2 holds

L is modular

proof end;

:: <= :: L is modular implies L has_a_representation_of_type<= 2

:: deftheorem defines new_set2 LATTICE8:def 3 :

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

for A being set holds new_set2 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_set2 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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b_{1} . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & b_{1} . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) )

for b_{1}, b_{2} being BiFunction of (new_set2 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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b_{1} . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & b_{1} . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b_{2} . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & b_{2} . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_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_fun2 (d,q) -> BiFunction of (new_set2 A),L means :Def4: :: LATTICE8:def 4

( ( 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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & it . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & it . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & it . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & it . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_4) ) ) );

ex b

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

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def4 defines new_bi_fun2 LATTICE8:def 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_{5} being BiFunction of (new_set2 A),L holds

( b_{5} = new_bi_fun2 (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}}) = ((d . ((q `1_4),(q `2_4))) "\/" (q `3_4)) "/\" (q `4_4) & b_{5} . ({{A}},{A}) = ((d . ((q `1_4),(q `2_4))) "\/" (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 `2_4))) "\/" (q `3_4) & b_{5} . ({{A}},u) = (d . (u,(q `2_4))) "\/" (q `3_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 Th10: :: LATTICE8:10

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_fun2 (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_fun2 (d,q) is zeroed

proof end;

theorem Th11: :: LATTICE8:11

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_fun2 (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_fun2 (d,q) is symmetric

proof end;

theorem Th12: :: LATTICE8:12

for A being non empty set

for L being lower-bounded LATTICE st L is modular holds

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_fun2 (d,q) is u.t.i.

for L being lower-bounded LATTICE st L is modular holds

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_fun2 (d,q) is u.t.i.

proof end;

theorem Th13: :: LATTICE8:13

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_fun2 (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_fun2 (d,q)

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_set2 (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_set2 (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_set2 (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 ConsecutiveSet2 (A,O) -> set means :Def5: :: LATTICE8:def 5

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_set2 (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_set2 (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_set2 (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_set2 (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_set2 (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 Def5 defines ConsecutiveSet2 LATTICE8:def 5 :

for A being non empty set

for O being Ordinal

for b_{3} being set holds

( b_{3} = ConsecutiveSet2 (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_set2 (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_set2 (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 Th15: :: LATTICE8:15

for A being non empty set

for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O))

for O being Ordinal holds ConsecutiveSet2 (A,(succ O)) = new_set2 (ConsecutiveSet2 (A,O))

proof end;

theorem Th16: :: LATTICE8:16

for A being non empty set

for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds

T . O1 = ConsecutiveSet2 (A,O1) ) holds

ConsecutiveSet2 (A,O) = union (rng T)

for O being Ordinal

for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds

T . O1 = ConsecutiveSet2 (A,O1) ) holds

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

let q be QuadrSeq of d;

let O be Ordinal;

assume A1: O in dom q ;

coherence

q . O is Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (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 Quadr2 (q,O) -> Element of [:(ConsecutiveSet2 (A,O)),(ConsecutiveSet2 (A,O)), the carrier of L, the carrier of L:] equals :Def6: :: LATTICE8:def 6

q . O;

correctness q . O;

coherence

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

proof end;

:: deftheorem Def6 defines Quadr2 LATTICE8:def 6 :

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

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

Quadr2 (q,O) = q . O;

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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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 ConsecutiveDelta2 (q,O) -> set means :Def7: :: LATTICE8:def 7

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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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 Def7 defines ConsecutiveDelta2 LATTICE8:def 7 :

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} = ConsecutiveDelta2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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_fun2 ((BiFun ((L0 . C),(ConsecutiveSet2 (A,C)),L)),(Quadr2 (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 Th18: :: LATTICE8: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 ConsecutiveDelta2 (q,0) = d

for L being lower-bounded LATTICE

for d being BiFunction of A,L

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

proof end;

theorem Th19: :: LATTICE8: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

for O being Ordinal holds ConsecutiveDelta2 (q,(succ O)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O)),(ConsecutiveSet2 (A,O)),L)),(Quadr2 (q,O)))

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for q being QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,(succ O)) = new_bi_fun2 ((BiFun ((ConsecutiveDelta2 (q,O)),(ConsecutiveSet2 (A,O)),L)),(Quadr2 (q,O)))

proof end;

theorem Th20: :: LATTICE8:20

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 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 = ConsecutiveDelta2 (q,O1) ) holds

ConsecutiveDelta2 (q,O) = union (rng T)

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for q being QuadrSeq of d

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 = ConsecutiveDelta2 (q,O1) ) holds

ConsecutiveDelta2 (q,O) = union (rng T)

proof end;

theorem Th21: :: LATTICE8:21

for A being non empty set

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

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

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

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

proof end;

theorem Th22: :: LATTICE8:22

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 holds ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for q being QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (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: ConsecutiveDelta2

redefine func ConsecutiveDelta2 (q,O) -> BiFunction of (ConsecutiveSet2 (A,O)),L;

coherence

ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L by Th22;

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

redefine func ConsecutiveDelta2 (q,O) -> BiFunction of (ConsecutiveSet2 (A,O)),L;

coherence

ConsecutiveDelta2 (q,O) is BiFunction of (ConsecutiveSet2 (A,O)),L by Th22;

theorem Th23: :: LATTICE8:23

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 holds d c= ConsecutiveDelta2 (q,O)

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for q being QuadrSeq of d

for O being Ordinal holds d c= ConsecutiveDelta2 (q,O)

proof end;

theorem Th24: :: LATTICE8:24

for A being non empty set

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for O1, O2 being Ordinal

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)

for L being lower-bounded LATTICE

for d being BiFunction of A,L

for O1, O2 being Ordinal

for q being QuadrSeq of d st O1 c= O2 holds

ConsecutiveDelta2 (q,O1) c= ConsecutiveDelta2 (q,O2)

proof end;

theorem Th25: :: LATTICE8:25

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 QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed

for L being lower-bounded LATTICE

for d being BiFunction of A,L st d is zeroed holds

for q being QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,O) is zeroed

proof end;

theorem Th26: :: LATTICE8:26

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 QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric

for L being lower-bounded LATTICE

for d being BiFunction of A,L st d is symmetric holds

for q being QuadrSeq of d

for O being Ordinal holds ConsecutiveDelta2 (q,O) is symmetric

proof end;

theorem Th27: :: LATTICE8:27

for A being non empty set

for L being lower-bounded LATTICE st L is modular holds

for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds

for O being Ordinal

for q being QuadrSeq of d st O c= DistEsti d holds

ConsecutiveDelta2 (q,O) is u.t.i.

for L being lower-bounded LATTICE st L is modular holds

for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds

for O being Ordinal

for q being QuadrSeq of d st O c= DistEsti d holds

ConsecutiveDelta2 (q,O) is u.t.i.

proof end;

theorem :: LATTICE8:28

for A being non empty set

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for O being Ordinal

for q being QuadrSeq of d st O c= DistEsti d holds

ConsecutiveDelta2 (q,O) is distance_function of (ConsecutiveSet2 (A,O)),L by Th25, Th26, Th27;

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for O being Ordinal

for q being QuadrSeq of d st O c= DistEsti d holds

ConsecutiveDelta2 (q,O) is distance_function of (ConsecutiveSet2 (A,O)),L by Th25, Th26, Th27;

definition

let A be non empty set ;

let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

correctness

coherence

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

;

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

correctness

coherence

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

;

:: deftheorem defines NextSet2 LATTICE8:def 8 :

for A being non empty set

for L being lower-bounded LATTICE

for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 (A,(DistEsti d));

for A being non empty set

for L being lower-bounded LATTICE

for d being BiFunction of A,L holds NextSet2 d = ConsecutiveSet2 (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 NextSet2 d is empty ;

end;
let L be lower-bounded LATTICE;

let d be BiFunction of A,L;

coherence

not NextSet2 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

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

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

;

:: deftheorem defines NextDelta2 LATTICE8:def 9 :

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 NextDelta2 q = ConsecutiveDelta2 (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 NextDelta2 q = ConsecutiveDelta2 (q,(DistEsti d));

definition

let A be non empty set ;

let L be lower-bounded modular LATTICE;

let d be distance_function of A,L;

let q be QuadrSeq of d;

:: original: NextDelta2

redefine func NextDelta2 q -> distance_function of (NextSet2 d),L;

coherence

NextDelta2 q is distance_function of (NextSet2 d),L by Th25, Th26, Th27;

end;
let L be lower-bounded modular LATTICE;

let d be distance_function of A,L;

let q be QuadrSeq of d;

:: original: NextDelta2

redefine func NextDelta2 q -> distance_function of (NextSet2 d),L;

coherence

NextDelta2 q is distance_function of (NextSet2 d),L by Th25, Th26, Th27;

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_extension2_of A,d means :: LATTICE8:def 10

ex q being QuadrSeq of d st

( Aq = NextSet2 d & dq = NextDelta2 q );

ex q being QuadrSeq of d st

( Aq = NextSet2 d & dq = NextDelta2 q );

:: deftheorem defines is_extension2_of LATTICE8:def 10 :

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_extension2_of A,d iff ex q being QuadrSeq of d st

( Aq = NextSet2 d & dq = NextDelta2 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_extension2_of A,d iff ex q being QuadrSeq of d st

( Aq = NextSet2 d & dq = NextDelta2 q ) );

theorem Th29: :: LATTICE8:29

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_extension2_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 being Element of Aq st

( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )

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_extension2_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 being Element of Aq st

( dq . (x,z1) = a & dq . (z1,z2) = ((d . (x,y)) "\/" a) "/\" b & dq . (z2,y) = a )

proof end;

definition

let A be non empty set ;

let L be lower-bounded modular 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_extension2_of A9,d9 & b_{1} . n = [A9,d9] & b_{1} . (n + 1) = [Aq,dq] ) ) )

end;
let L be lower-bounded modular LATTICE;

let d be distance_function of A,L;

mode ExtensionSeq2 of A,d -> Function means :Def11: :: LATTICE8:def 11

( 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_extension2_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_extension2_of A9,d9 & it . n = [A9,d9] & it . (n + 1) = [Aq,dq] ) ) );

ex b

( dom b

( Aq,dq is_extension2_of A9,d9 & b

proof end;

:: deftheorem Def11 defines ExtensionSeq2 LATTICE8:def 11 :

for A being non empty set

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for b_{4} being Function holds

( b_{4} is ExtensionSeq2 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_extension2_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 modular LATTICE

for d being distance_function of A,L

for b

( b

( Aq,dq is_extension2_of A9,d9 & b

theorem Th30: :: LATTICE8:30

for A being non empty set

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for S being ExtensionSeq2 of A,d

for k, l being Nat st k <= l holds

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

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for S being ExtensionSeq2 of A,d

for k, l being Nat st k <= l holds

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

proof end;

theorem Th31: :: LATTICE8:31

for A being non empty set

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for S being ExtensionSeq2 of A,d

for k, l being Nat st k <= l holds

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

for L being lower-bounded modular LATTICE

for d being distance_function of A,L

for S being ExtensionSeq2 of A,d

for k, l being Nat st k <= l holds

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

proof end;

theorem Th32: :: LATTICE8:32

for L being lower-bounded modular LATTICE

for S being ExtensionSeq2 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 ExtensionSeq2 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 Th33: :: LATTICE8:33

for L being lower-bounded modular LATTICE

for S being ExtensionSeq2 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 being Element of FS st

( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )

for S being ExtensionSeq2 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 being Element of FS st

( FD . (x,z1) = a & FD . (z1,z2) = ((FD . (x,y)) "\/" a) "/\" b & FD . (z2,y) = a )

proof end;

Lm3: for m being Element of NAT holds

( not m in Seg 4 or m = 1 or m = 2 or m = 3 or m = 4 )

proof end;

Lm4: for j being Nat st 1 <= j & j < 4 & not j = 1 & not j = 2 holds

j = 3

proof end;

theorem Th34: :: LATTICE8:34

for L being lower-bounded modular LATTICE

for S being ExtensionSeq2 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 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 = 2 + 2 & x,y are_joint_by F,e1,e2 )

for S being ExtensionSeq2 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 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 = 2 + 2 & x,y are_joint_by F,e1,e2 )

proof end;

:: <=> :: L has_a_representation_of_type<= 2 iff L is modular

:: Jonsson Theorem for modular lattices

:: Jonsson Theorem for modular lattices

theorem :: LATTICE8:36

for L being lower-bounded LATTICE holds

( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th35;

( L has_a_representation_of_type<= 2 iff L is modular ) by Th9, Th35;