set f = { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } ;
A1:
ConceptLattice (C .:) = LattStr(# (B-carrier (C .:)),(B-join (C .:)),(B-meet (C .:)) #)
by CONLAT_1:def 20;
A2:
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #)
by CONLAT_1:def 20;
then A3:
(ConceptLattice C) .: = LattStr(# (B-carrier C),(B-meet C),(B-join C) #)
by LATTICE2:def 2;
{ [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } c= [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
proof
let y be
object ;
TARSKI:def 3 ( not y in { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } or y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] )
assume
y in { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C }
;
y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
then consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A4:
y = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)]
and A5:
ConceptStr(#
O,
A #) is
FormalConcept of
C
;
ConceptStr(#
O,
A #)
.: is
strict FormalConcept of
C .:
by A5;
then A6:
ConceptStr(#
O,
A #)
.: in the
carrier of
(ConceptLattice (C .:))
by A1, CONLAT_1:31;
ConceptStr(#
O,
A #)
in the
carrier of
((ConceptLattice C) .:)
by A3, A5, CONLAT_1:31;
hence
y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
by A4, A6, ZFMISC_1:def 2;
verum
end;
then reconsider f = { [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] where O is Subset of the carrier of C, A is Subset of the carrier' of C : ConceptStr(# O,A #) is FormalConcept of C } as Relation of the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)) ;
the carrier of ((ConceptLattice C) .:) c= dom f
proof
let y be
object ;
TARSKI:def 3 ( not y in the carrier of ((ConceptLattice C) .:) or y in dom f )
assume
y in the
carrier of
((ConceptLattice C) .:)
;
y in dom f
then A7:
y is
strict FormalConcept of
C
by A3, CONLAT_1:31;
then consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A8:
y = ConceptStr(#
O9,
A9 #)
;
set z =
ConceptStr(#
O9,
A9 #)
.: ;
ConceptStr(#
O9,
A9 #)
.: is
strict FormalConcept of
C .:
by A7, A8;
then reconsider z =
ConceptStr(#
O9,
A9 #)
.: as
Element of
(ConceptLattice (C .:)) by A1, CONLAT_1:31;
[y,z] in f
by A7, A8;
hence
y in dom f
by XTUPLE_0:def 12;
verum
end;
then A9:
the carrier of ((ConceptLattice C) .:) = dom f
;
for x, y1, y2 being object st [x,y1] in f & [x,y2] in f holds
y1 = y2
proof
let x,
y1,
y2 be
object ;
( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume that A10:
[x,y1] in f
and A11:
[x,y2] in f
;
y1 = y2
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A12:
[x,y2] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A11;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A13:
[x,y1] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A10;
A14:
ConceptStr(#
O,
A #) =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `1
.=
[x,y1] `1
by A13
.=
x
.=
[x,y2] `1
.=
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `1
by A12
.=
ConceptStr(#
O9,
A9 #)
;
thus y1 =
[x,y1] `2
.=
[x,y2] `2
by A13, A12, A14
.=
y2
;
verum
end;
then reconsider f = f as Function of the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)) by A9, FUNCT_1:def 1, FUNCT_2:def 1;
A15:
(ConceptLattice C) .: = LattStr(# the carrier of (ConceptLattice C), the L_meet of (ConceptLattice C), the L_join of (ConceptLattice C) #)
by LATTICE2:def 2;
A16:
for a, b being Element of ((ConceptLattice C) .:) st a [= b holds
f . a [= f . b
proof
let a,
b be
Element of
((ConceptLattice C) .:);
( a [= b implies f . a [= f . b )
reconsider aa =
a % ,
bb =
b % as
Element of
(LattPOSet (ConceptLattice C)) by A15;
reconsider a9 =
a,
b9 =
b as
Element of
(ConceptLattice C) by A15;
A17:
dom f = the
carrier of
((ConceptLattice C) .:)
by FUNCT_2:def 1;
then consider fa being
object such that A18:
[a,fa] in f
by XTUPLE_0:def 12;
assume
a [= b
;
f . a [= f . b
then
a % <= b %
by LATTICE3:7;
then
[(a %),(b %)] in the
InternalRel of
(LattPOSet ((ConceptLattice C) .:))
by ORDERS_2:def 5;
then
[(a %),(b %)] in the
InternalRel of
(LattPOSet (ConceptLattice C)) ~
by LATTICE3:20;
then
[(b %),(a %)] in the
InternalRel of
(LattPOSet (ConceptLattice C))
by RELAT_1:def 7;
then A19:
bb <= aa
by ORDERS_2:def 5;
(
(% aa) % = aa &
(% bb) % = bb )
;
then
% bb [= % aa
by A19, LATTICE3:7;
then A20:
(% bb) @ is-SubConcept-of (% aa) @
by CONLAT_1:43;
consider fb being
object such that A21:
[b,fb] in f
by A17, XTUPLE_0:def 12;
A22:
fb in rng f
by A21, XTUPLE_0:def 13;
A23:
f . b = fb
by A21, FUNCT_1:1;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A24:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A21;
A25:
b =
[b,fb] `1
.=
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `1
by A24
.=
ConceptStr(#
O9,
A9 #)
;
A26:
fa in rng f
by A18, XTUPLE_0:def 13;
A27:
f . a = fa
by A18, FUNCT_1:1;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A28:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A18;
reconsider fa =
fa as
Element of
(ConceptLattice (C .:)) by A26;
A29:
a =
[a,fa] `1
.=
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `1
by A28
.=
ConceptStr(#
O,
A #)
;
reconsider fb =
fb as
Element of
(ConceptLattice (C .:)) by A22;
fb =
[b,fb] `2
.=
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)] `2
by A24
.=
ConceptStr(#
O9,
A9 #)
.:
;
then A30: the
Intent of
(fb @) =
the
Intent of
(ConceptStr(# O9,A9 #) .:)
by CONLAT_1:def 21
.=
the
Extent of
ConceptStr(#
O9,
A9 #)
by Def8
.=
the
Extent of
(b9 @)
by A25, CONLAT_1:def 21
;
fa =
[a,fa] `2
.=
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)] `2
by A28
.=
ConceptStr(#
O,
A #)
.:
;
then the
Intent of
(fa @) =
the
Intent of
(ConceptStr(# O,A #) .:)
by CONLAT_1:def 21
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
.=
the
Extent of
(a9 @)
by A29, CONLAT_1:def 21
;
then
the
Intent of
(fb @) c= the
Intent of
(fa @)
by A20, A30, CONLAT_1:def 16;
then
fa @ is-SubConcept-of fb @
by CONLAT_1:28;
hence
f . a [= f . b
by A27, A23, CONLAT_1:43;
verum
end;
the carrier of (ConceptLattice (C .:)) c= rng f
proof
let u be
object ;
TARSKI:def 3 ( not u in the carrier of (ConceptLattice (C .:)) or u in rng f )
A31:
dom f = the
carrier of
((ConceptLattice C) .:)
by FUNCT_2:def 1;
assume
u in the
carrier of
(ConceptLattice (C .:))
;
u in rng f
then reconsider u =
u as
Element of
(ConceptLattice (C .:)) ;
reconsider A9 = the
Intent of
(u @) as
Subset of the
carrier of
C ;
reconsider O9 = the
Extent of
(u @) as
Subset of the
carrier' of
C ;
set CP =
ConceptStr(#
A9,
O9 #);
A32:
( not the
Extent of
(u @) is
empty or not the
Intent of
(u @) is
empty )
by CONLAT_1:def 8;
A33:
(AttributeDerivation C) . the
Intent of
ConceptStr(#
A9,
O9 #) =
(ObjectDerivation (C .:)) . the
Extent of
(u @)
by Th19
.=
the
Extent of
ConceptStr(#
A9,
O9 #)
by CONLAT_1:def 10
;
(ObjectDerivation C) . the
Extent of
ConceptStr(#
A9,
O9 #) =
(AttributeDerivation (C .:)) . the
Intent of
(u @)
by Th18
.=
the
Intent of
ConceptStr(#
A9,
O9 #)
by CONLAT_1:def 10
;
then
ConceptStr(#
A9,
O9 #) is
FormalConcept of
C
by A33, A32, CONLAT_1:def 8, CONLAT_1:def 10;
then
ConceptStr(#
A9,
O9 #)
in dom f
by A15, A2, A31, CONLAT_1:31;
then consider v being
object such that A34:
[ConceptStr(# A9,O9 #),v] in f
by XTUPLE_0:def 12;
consider Ov being
Subset of the
carrier of
C,
Av being
Subset of the
carrier' of
C such that A35:
[ConceptStr(# A9,O9 #),v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)]
and
ConceptStr(#
Ov,
Av #) is
FormalConcept of
C
by A34;
A36:
ConceptStr(#
A9,
O9 #) =
[ConceptStr(# A9,O9 #),v] `1
.=
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] `1
by A35
.=
ConceptStr(#
Ov,
Av #)
;
A37:
v in rng f
by A34, XTUPLE_0:def 13;
then reconsider v =
v as
strict FormalConcept of
C .: by A1, CONLAT_1:31;
v =
[ConceptStr(# A9,O9 #),v] `2
.=
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] `2
by A35
.=
ConceptStr(#
Ov,
Av #)
.:
;
then
( the
Extent of
v = the
Extent of
(u @) & the
Intent of
v = the
Intent of
(u @) )
by A36, Def8;
hence
u in rng f
by A37, CONLAT_1:def 21;
verum
end;
then A38:
rng f = the carrier of (ConceptLattice (C .:))
;
A39:
f is one-to-one
proof
let a,
b be
object ;
FUNCT_1:def 4 ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that A40:
a in dom f
and A41:
b in dom f
and A42:
f . a = f . b
;
a = b
reconsider a =
a,
b =
b as
Element of
((ConceptLattice C) .:) by A40, A41;
consider fa being
object such that A43:
[a,fa] in f
by A40, XTUPLE_0:def 12;
consider fb being
object such that A44:
[b,fb] in f
by A41, XTUPLE_0:def 12;
A45:
f . b = fb
by A44, FUNCT_1:1;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A46:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A43;
A47:
a = ConceptStr(#
O,
A #)
by A46, XTUPLE_0:1;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A48:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A44;
A49:
b = ConceptStr(#
O9,
A9 #)
by A48, XTUPLE_0:1;
A50:
ConceptStr(#
O9,
A9 #)
.: =
fb
by A48, XTUPLE_0:1
.=
fa
by A42, A43, A45, FUNCT_1:1
.=
ConceptStr(#
O,
A #)
.:
by A46, XTUPLE_0:1
;
then A51: the
Intent of
ConceptStr(#
O9,
A9 #) =
the
Extent of
(ConceptStr(# O,A #) .:)
by Def8
.=
the
Intent of
ConceptStr(#
O,
A #)
by Def8
;
the
Extent of
ConceptStr(#
O9,
A9 #) =
the
Intent of
(ConceptStr(# O,A #) .:)
by A50, Def8
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
;
hence
a = b
by A47, A49, A51;
verum
end;
for a, b being Element of ((ConceptLattice C) .:) st f . a [= f . b holds
a [= b
proof
let a,
b be
Element of
((ConceptLattice C) .:);
( f . a [= f . b implies a [= b )
A52:
dom f = the
carrier of
((ConceptLattice C) .:)
by FUNCT_2:def 1;
then consider fa being
object such that A53:
[a,fa] in f
by XTUPLE_0:def 12;
reconsider a9 =
a,
b9 =
b as
Element of
(ConceptLattice C) by A15;
assume
f . a [= f . b
;
a [= b
then A54:
(f . a) @ is-SubConcept-of (f . b) @
by CONLAT_1:43;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A55:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .:)]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A53;
A56:
a = ConceptStr(#
O,
A #)
by A55, XTUPLE_0:1;
A57:
fa in rng f
by A53, XTUPLE_0:def 13;
consider fb being
object such that A58:
[b,fb] in f
by A52, XTUPLE_0:def 12;
A59:
fb in rng f
by A58, XTUPLE_0:def 13;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A60:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .:)]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A58;
A61:
b = ConceptStr(#
O9,
A9 #)
by A60, XTUPLE_0:1;
reconsider fb =
fb as
Element of
(ConceptLattice (C .:)) by A59;
A62:
fb = ConceptStr(#
O9,
A9 #)
.:
by A60, XTUPLE_0:1;
A63: the
Intent of
((f . b) @) =
the
Intent of
(fb @)
by A58, FUNCT_1:1
.=
the
Intent of
(ConceptStr(# O9,A9 #) .:)
by A62, CONLAT_1:def 21
.=
the
Extent of
ConceptStr(#
O9,
A9 #)
by Def8
.=
the
Extent of
(b9 @)
by A61, CONLAT_1:def 21
;
reconsider fa =
fa as
Element of
(ConceptLattice (C .:)) by A57;
A64:
fa = ConceptStr(#
O,
A #)
.:
by A55, XTUPLE_0:1;
the
Intent of
((f . a) @) =
the
Intent of
(fa @)
by A53, FUNCT_1:1
.=
the
Intent of
(ConceptStr(# O,A #) .:)
by A64, CONLAT_1:def 21
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
.=
the
Extent of
(a9 @)
by A56, CONLAT_1:def 21
;
then
the
Extent of
(b9 @) c= the
Extent of
(a9 @)
by A54, A63, CONLAT_1:28;
then
b9 @ is-SubConcept-of a9 @
by CONLAT_1:def 16;
then
b9 [= a9
by CONLAT_1:43;
then
b9 % <= a9 %
by LATTICE3:7;
then
[(b9 %),(a9 %)] in the
InternalRel of
(LattPOSet (ConceptLattice C))
by ORDERS_2:def 5;
then
[(a %),(b %)] in the
InternalRel of
((LattPOSet (ConceptLattice C)) ~)
by RELAT_1:def 7;
then
[(a %),(b %)] in the
InternalRel of
(LattPOSet ((ConceptLattice C) .:))
by LATTICE3:20;
then
a % <= b %
by ORDERS_2:def 5;
hence
a [= b
by LATTICE3:7;
verum
end;
then reconsider f = f as Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) by A16, A38, A39, Lm2;
for CP being strict FormalConcept of C holds f . CP = CP .:
proof
let CP be
strict FormalConcept of
C;
f . CP = CP .:
CP in B-carrier C
by CONLAT_1:31;
then
CP in dom f
by A3, FUNCT_2:def 1;
then consider v being
object such that A65:
[CP,v] in f
by XTUPLE_0:def 12;
A66:
v in rng f
by A65, XTUPLE_0:def 13;
consider Ov being
Subset of the
carrier of
C,
Av being
Subset of the
carrier' of
C such that A67:
[CP,v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)]
and
ConceptStr(#
Ov,
Av #) is
FormalConcept of
C
by A65;
reconsider v =
v as
strict FormalConcept of
C .: by A1, A66, CONLAT_1:31;
A68:
CP = ConceptStr(#
Ov,
Av #)
by A67, XTUPLE_0:1;
v = ConceptStr(#
Ov,
Av #)
.:
by A67, XTUPLE_0:1;
hence
f . CP = CP .:
by A65, A68, FUNCT_1:1;
verum
end;
hence
ex b1 being Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) st
for CP being strict FormalConcept of C holds b1 . CP = CP .:
; verum