begin
begin
begin
Lm1:
now for i, n, m being Element of NAT st 1 <= i & i < n + m & not ( 1 <= i & i < n ) & not ( n = i & i < n + m ) holds
( n + 1 <= i & i < n + m )
let i,
n,
m be
Element of
NAT ;
( 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 )
;
( ( 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;
verum
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:
( ( for
e1,
e2 being
Equivalence_Relation of
X for
x,
y being
set st
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 holds
ex
F being non
empty FinSequence of
X st
(
len F = it + 2 &
x,
y are_joint_by F,
e1,
e2 ) ) & ex
e1,
e2 being
Equivalence_Relation of
X ex
x,
y being
set st
(
e1 in the
carrier of
Y &
e2 in the
carrier of
Y &
[x,y] in e1 "\/" e2 & ( for
F being non
empty FinSequence of
X holds
( not
len F = it + 1 or not
x,
y are_joint_by F,
e1,
e2 ) ) ) );
existence
ex b1 being Element of NAT st
( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) )
uniqueness
for b1, b2 being Element of NAT st ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b1 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b1 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) & ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b2 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b2 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) holds
b1 = b2
end;
::
deftheorem Def4 defines
type_of LATTICE5:def 4 :
for X being non empty set
for Y being Sublattice of EqRelLATT X st ex e being Equivalence_Relation of X st
( e in the carrier of Y & e <> id X ) & ex o being Element of NAT st
for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = o & x,y are_joint_by F,e1,e2 ) holds
for b3 being Element of NAT holds
( b3 = type_of Y iff ( ( for e1, e2 being Equivalence_Relation of X
for x, y being set st e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 holds
ex F being non empty FinSequence of X st
( len F = b3 + 2 & x,y are_joint_by F,e1,e2 ) ) & ex e1, e2 being Equivalence_Relation of X ex x, y being set st
( e1 in the carrier of Y & e2 in the carrier of Y & [x,y] in e1 "\/" e2 & ( for F being non empty FinSequence of X holds
( not len F = b3 + 1 or not x,y are_joint_by F,e1,e2 ) ) ) ) );
begin
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
distance_function of
A,
L;
existence
ex b1 being Function of L,(EqRelLATT A) st
for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) )
uniqueness
for b1, b2 being Function of L,(EqRelLATT A) st ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b1 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) ) & ( for e being Element of L ex E being Equivalence_Relation of A st
( E = b2 . e & ( for x, y being Element of A holds
( [x,y] in E iff d . (x,y) <= e ) ) ) ) holds
b1 = b2
end;
begin
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
BiFunction of
A,
L;
let q be
Element of
[:A,A, the carrier of L, the carrier of L:];
func new_bi_fun (
d,
q)
-> BiFunction of
(new_set A),
L means :
Def10:
( ( for
u,
v being
Element of
A holds
it . (
u,
v)
= d . (
u,
v) ) &
it . (
{A},
{A})
= Bottom L &
it . (
{{A}},
{{A}})
= Bottom L &
it . (
{{{A}}},
{{{A}}})
= Bottom L &
it . (
{{A}},
{{{A}}})
= q `3_4 &
it . (
{{{A}}},
{{A}})
= q `3_4 &
it . (
{A},
{{A}})
= q `4_4 &
it . (
{{A}},
{A})
= q `4_4 &
it . (
{A},
{{{A}}})
= (q `3_4) "\/" (q `4_4) &
it . (
{{{A}}},
{A})
= (q `3_4) "\/" (q `4_4) & ( for
u being
Element of
A holds
(
it . (
u,
{A})
= (d . (u,(q `1_4))) "\/" (q `3_4) &
it . (
{A},
u)
= (d . (u,(q `1_4))) "\/" (q `3_4) &
it . (
u,
{{A}})
= ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) &
it . (
{{A}},
u)
= ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) &
it . (
u,
{{{A}}})
= (d . (u,(q `2_4))) "\/" (q `4_4) &
it . (
{{{A}}},
u)
= (d . (u,(q `2_4))) "\/" (q `4_4) ) ) );
existence
ex b1 being BiFunction of (new_set A),L st
( ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({{{A}}},{{{A}}}) = Bottom L & b1 . ({{A}},{{{A}}}) = q `3_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) )
uniqueness
for b1, b2 being BiFunction of (new_set A),L st ( for u, v being Element of A holds b1 . (u,v) = d . (u,v) ) & b1 . ({A},{A}) = Bottom L & b1 . ({{A}},{{A}}) = Bottom L & b1 . ({{{A}}},{{{A}}}) = Bottom L & b1 . ({{A}},{{{A}}}) = q `3_4 & b1 . ({{{A}}},{{A}}) = q `3_4 & b1 . ({A},{{A}}) = q `4_4 & b1 . ({{A}},{A}) = q `4_4 & b1 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b1 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b1 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b1 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b1 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b1 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) & ( for u, v being Element of A holds b2 . (u,v) = d . (u,v) ) & b2 . ({A},{A}) = Bottom L & b2 . ({{A}},{{A}}) = Bottom L & b2 . ({{{A}}},{{{A}}}) = Bottom L & b2 . ({{A}},{{{A}}}) = q `3_4 & b2 . ({{{A}}},{{A}}) = q `3_4 & b2 . ({A},{{A}}) = q `4_4 & b2 . ({{A}},{A}) = q `4_4 & b2 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b2 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b2 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b2 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b2 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b2 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) holds
b1 = b2
end;
::
deftheorem Def10 defines
new_bi_fun LATTICE5:def 10 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for q being Element of [:A,A, the carrier of L, the carrier of L:]
for b5 being BiFunction of (new_set A),L holds
( b5 = new_bi_fun (d,q) iff ( ( for u, v being Element of A holds b5 . (u,v) = d . (u,v) ) & b5 . ({A},{A}) = Bottom L & b5 . ({{A}},{{A}}) = Bottom L & b5 . ({{{A}}},{{{A}}}) = Bottom L & b5 . ({{A}},{{{A}}}) = q `3_4 & b5 . ({{{A}}},{{A}}) = q `3_4 & b5 . ({A},{{A}}) = q `4_4 & b5 . ({{A}},{A}) = q `4_4 & b5 . ({A},{{{A}}}) = (q `3_4) "\/" (q `4_4) & b5 . ({{{A}}},{A}) = (q `3_4) "\/" (q `4_4) & ( for u being Element of A holds
( b5 . (u,{A}) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . ({A},u) = (d . (u,(q `1_4))) "\/" (q `3_4) & b5 . (u,{{A}}) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . ({{A}},u) = ((d . (u,(q `1_4))) "\/" (q `3_4)) "\/" (q `4_4) & b5 . (u,{{{A}}}) = (d . (u,(q `2_4))) "\/" (q `4_4) & b5 . ({{{A}}},u) = (d . (u,(q `2_4))) "\/" (q `4_4) ) ) ) );
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
BiFunction of
A,
L;
existence
ex b1 being Cardinal st b1, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent
uniqueness
for b1, b2 being Cardinal st b1, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent & b2, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent holds
b1 = b2
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 :
Def13:
(
dom it is
Cardinal &
it is
one-to-one &
rng it = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } );
existence
ex b1 being T-Sequence of [:A,A, the carrier of L, the carrier of L:] st
( dom b1 is Cardinal & b1 is one-to-one & rng b1 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } )
end;
::
deftheorem Def13 defines
QuadrSeq LATTICE5:def 13 :
for A being non empty set
for L being lower-bounded LATTICE
for d being BiFunction of A,L
for b4 being T-Sequence of [:A,A, the carrier of L, the carrier of L:] holds
( b4 is QuadrSeq of d iff ( dom b4 is Cardinal & b4 is one-to-one & rng b4 = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } ) );
definition
let A be non
empty set ;
let L be
lower-bounded LATTICE;
let d be
BiFunction of
A,
L;
let q be
QuadrSeq of
d;
let O be
Ordinal;
correctness
existence
ex b1 being set ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) );
uniqueness
for b1, b2 being set st ex L0 being T-Sequence st
( b1 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) & ex L0 being T-Sequence st
( b2 = last L0 & dom L0 = succ O & L0 . {} = d & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_bi_fun ((BiFun ((L0 . C),(ConsecutiveSet (A,C)),L)),(Quadr (q,C))) ) & ( for C being Ordinal st C in succ O & C <> {} & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) holds
b1 = b2;
end;
theorem Th37:
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 )
definition
let L be
lower-bounded LATTICE;
existence
ex b1 being distance_function of the carrier of L,L st
for x, y being Element of L holds
( ( x <> y implies b1 . (x,y) = x "\/" y ) & ( x = y implies b1 . (x,y) = Bottom L ) )
uniqueness
for b1, b2 being distance_function of the carrier of L,L st ( for x, y being Element of L holds
( ( x <> y implies b1 . (x,y) = x "\/" y ) & ( x = y implies b1 . (x,y) = Bottom L ) ) ) & ( for x, y being Element of L holds
( ( x <> y implies b2 . (x,y) = x "\/" y ) & ( x = y implies b2 . (x,y) = Bottom L ) ) ) holds
b1 = b2
end;
Lm2:
now for j being Element of NAT st 1 <= j & j < 5 & not j = 1 & not j = 2 & not j = 3 holds
j = 4
let j be
Element of
NAT ;
( 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
;
( j = 1 or j = 2 or j = 3 or j = 4 )
j < 4
+ 1
by A2;
then
j <= 4
by NAT_1:13;
then
(
j = 0 or
j = 1 or
j = 2 or
j = 3 or
j = 4 )
by NAT_1:28;
hence
(
j = 1 or
j = 2 or
j = 3 or
j = 4 )
by A1;
verum
end;
theorem Th42:
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 )
theorem Th43:
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 )