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 23;
A2:
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #)
by CONLAT_1:def 23;
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
set ;
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, Lm4;
then A6:
ConceptStr(#
O,
A #)
.: in the
carrier of
(ConceptLattice (C .: ))
by A1, CONLAT_1:35;
ConceptStr(#
O,
A #)
in the
carrier of
((ConceptLattice C) .: )
by A3, A5, CONLAT_1:35;
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
set ;
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:35;
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, Lm4;
then reconsider z =
ConceptStr(#
O9,
A9 #)
.: as
Element of
(ConceptLattice (C .: )) by A1, CONLAT_1:35;
[y,z] in f
by A7, A8;
hence
y in dom f
by RELAT_1:def 4;
verum
end;
then A9:
the carrier of ((ConceptLattice C) .: ) = dom f
by XBOOLE_0:def 10;
for x, y1, y2 being set st [x,y1] in f & [x,y2] in f holds
y1 = y2
proof
let x,
y1,
y2 be
set ;
( [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;
ConceptStr(#
O,
A #) =
[x,y1] `1
by A13, MCART_1:def 1
.=
x
by MCART_1:def 1
.=
[x,y2] `1
by MCART_1:def 1
.=
ConceptStr(#
O9,
A9 #)
by A12, MCART_1:def 1
;
hence y1 =
[x,y2] `2
by A13, A12, MCART_1:def 2
.=
y2
by MCART_1:def 2
;
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;
A14:
(ConceptLattice C) .: = LattStr(# the carrier of (ConceptLattice C),the L_meet of (ConceptLattice C),the L_join of (ConceptLattice C) #)
by LATTICE2:def 2;
A15:
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 A14;
reconsider a9 =
a,
b9 =
b as
Element of
(ConceptLattice C) by A14;
A16:
dom f = the
carrier of
((ConceptLattice C) .: )
by FUNCT_2:def 1;
then consider fa being
set such that A17:
[a,fa] in f
by RELAT_1:def 4;
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 9;
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 A18:
bb <= aa
by ORDERS_2:def 9;
(
(% aa) % = aa &
(% bb) % = bb )
;
then
% bb [= % aa
by A18, LATTICE3:7;
then A19:
(% bb) @ is-SubConcept-of (% aa) @
by CONLAT_1:47;
consider fb being
set such that A20:
[b,fb] in f
by A16, RELAT_1:def 4;
A21:
fb in rng f
by A20, RELAT_1:def 5;
A22:
f . b = fb
by A20, FUNCT_1:8;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A23:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A20;
A24:
b =
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )] `1
by A23, MCART_1:def 1
.=
ConceptStr(#
O9,
A9 #)
by MCART_1:def 1
;
A25:
fa in rng f
by A17, RELAT_1:def 5;
A26:
f . a = fa
by A17, FUNCT_1:8;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A27:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A17;
reconsider fa =
fa as
Element of
(ConceptLattice (C .: )) by A25;
A28:
a =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )] `1
by A27, MCART_1:def 1
.=
ConceptStr(#
O,
A #)
by MCART_1:def 1
;
reconsider fb =
fb as
Element of
(ConceptLattice (C .: )) by A21;
fb =
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )] `2
by A23, MCART_1:def 2
.=
ConceptStr(#
O9,
A9 #)
.:
by MCART_1:def 2
;
then A29: the
Intent of
(fb @ ) =
the
Intent of
(ConceptStr(# O9,A9 #) .: )
by CONLAT_1:def 24
.=
the
Extent of
ConceptStr(#
O9,
A9 #)
by Def8
.=
the
Extent of
(b9 @ )
by A24, CONLAT_1:def 24
;
fa =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )] `2
by A27, MCART_1:def 2
.=
ConceptStr(#
O,
A #)
.:
by MCART_1:def 2
;
then the
Intent of
(fa @ ) =
the
Intent of
(ConceptStr(# O,A #) .: )
by CONLAT_1:def 24
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
.=
the
Extent of
(a9 @ )
by A28, CONLAT_1:def 24
;
then
the
Intent of
(fb @ ) c= the
Intent of
(fa @ )
by A19, A29, CONLAT_1:def 19;
then
fa @ is-SubConcept-of fb @
by CONLAT_1:31;
hence
f . a [= f . b
by A26, A22, CONLAT_1:47;
verum
end;
the carrier of (ConceptLattice (C .: )) c= rng f
proof
let u be
set ;
TARSKI:def 3 ( not u in the carrier of (ConceptLattice (C .: )) or u in rng f )
A30:
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 #);
A31:
( not the
Extent of
(u @ ) is
empty or not the
Intent of
(u @ ) is
empty )
by CONLAT_1:def 11;
A32:
(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 13
;
(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 13
;
then
ConceptStr(#
A9,
O9 #) is
FormalConcept of
C
by A32, A31, CONLAT_1:def 11, CONLAT_1:def 13;
then
ConceptStr(#
A9,
O9 #)
in dom f
by A14, A2, A30, CONLAT_1:35;
then consider v being
set such that A33:
[ConceptStr(# A9,O9 #),v] in f
by RELAT_1:def 4;
consider Ov being
Subset of the
carrier of
C,
Av being
Subset of the
carrier' of
C such that A34:
[ConceptStr(# A9,O9 #),v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )]
and
ConceptStr(#
Ov,
Av #) is
FormalConcept of
C
by A33;
A35:
ConceptStr(#
A9,
O9 #) =
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )] `1
by A34, MCART_1:def 1
.=
ConceptStr(#
Ov,
Av #)
by MCART_1:def 1
;
A36:
v in rng f
by A33, RELAT_1:def 5;
then reconsider v =
v as
strict FormalConcept of
C .: by A1, CONLAT_1:35;
v =
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )] `2
by A34, MCART_1:def 2
.=
ConceptStr(#
Ov,
Av #)
.:
by MCART_1:def 2
;
then
( the
Extent of
v = the
Extent of
(u @ ) & the
Intent of
v = the
Intent of
(u @ ) )
by A35, Def8;
hence
u in rng f
by A36, CONLAT_1:def 24;
verum
end;
then A37:
rng f = the carrier of (ConceptLattice (C .: ))
by XBOOLE_0:def 10;
A38:
f is one-to-one
proof
let a,
b be
set ;
FUNCT_1:def 8 ( not a in K40(f) or not b in K40(f) or not f . a = f . b or a = b )
assume that A39:
a in dom f
and A40:
b in dom f
and A41:
f . a = f . b
;
a = b
reconsider a =
a,
b =
b as
Element of
((ConceptLattice C) .: ) by A39, A40;
consider fa being
set such that A42:
[a,fa] in f
by A39, RELAT_1:def 4;
consider fb being
set such that A43:
[b,fb] in f
by A40, RELAT_1:def 4;
A44:
f . b = fb
by A43, FUNCT_1:8;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A45:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A42;
A46:
a =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )] `1
by A45, MCART_1:def 1
.=
ConceptStr(#
O,
A #)
by MCART_1:def 1
;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A47:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A43;
A48:
b =
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )] `1
by A47, MCART_1:def 1
.=
ConceptStr(#
O9,
A9 #)
by MCART_1:def 1
;
A49:
ConceptStr(#
O9,
A9 #)
.: =
[b,fb] `2
by A47, MCART_1:def 2
.=
fb
by MCART_1:def 2
.=
fa
by A41, A42, A44, FUNCT_1:8
.=
[a,fa] `2
by MCART_1:def 2
.=
ConceptStr(#
O,
A #)
.:
by A45, MCART_1:def 2
;
then A50: 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 A49, Def8
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
;
hence
a = b
by A46, A48, A50;
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 )
A51:
dom f = the
carrier of
((ConceptLattice C) .: )
by FUNCT_2:def 1;
then consider fa being
set such that A52:
[a,fa] in f
by RELAT_1:def 4;
reconsider a9 =
a,
b9 =
b as
Element of
(ConceptLattice C) by A14;
assume
f . a [= f . b
;
a [= b
then A53:
(f . a) @ is-SubConcept-of (f . b) @
by CONLAT_1:47;
consider O being
Subset of the
carrier of
C,
A being
Subset of the
carrier' of
C such that A54:
[a,fa] = [ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )]
and
ConceptStr(#
O,
A #) is
FormalConcept of
C
by A52;
A55:
a =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )] `1
by A54, MCART_1:def 1
.=
ConceptStr(#
O,
A #)
by MCART_1:def 1
;
A56:
fa in rng f
by A52, RELAT_1:def 5;
consider fb being
set such that A57:
[b,fb] in f
by A51, RELAT_1:def 4;
A58:
fb in rng f
by A57, RELAT_1:def 5;
consider O9 being
Subset of the
carrier of
C,
A9 being
Subset of the
carrier' of
C such that A59:
[b,fb] = [ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )]
and
ConceptStr(#
O9,
A9 #) is
FormalConcept of
C
by A57;
A60:
b =
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )] `1
by A59, MCART_1:def 1
.=
ConceptStr(#
O9,
A9 #)
by MCART_1:def 1
;
reconsider fb =
fb as
Element of
(ConceptLattice (C .: )) by A58;
A61:
fb =
[ConceptStr(# O9,A9 #),(ConceptStr(# O9,A9 #) .: )] `2
by A59, MCART_1:def 2
.=
ConceptStr(#
O9,
A9 #)
.:
by MCART_1:def 2
;
A62: the
Intent of
((f . b) @ ) =
the
Intent of
(fb @ )
by A57, FUNCT_1:8
.=
the
Intent of
(ConceptStr(# O9,A9 #) .: )
by A61, CONLAT_1:def 24
.=
the
Extent of
ConceptStr(#
O9,
A9 #)
by Def8
.=
the
Extent of
(b9 @ )
by A60, CONLAT_1:def 24
;
reconsider fa =
fa as
Element of
(ConceptLattice (C .: )) by A56;
A63:
fa =
[ConceptStr(# O,A #),(ConceptStr(# O,A #) .: )] `2
by A54, MCART_1:def 2
.=
ConceptStr(#
O,
A #)
.:
by MCART_1:def 2
;
the
Intent of
((f . a) @ ) =
the
Intent of
(fa @ )
by A52, FUNCT_1:8
.=
the
Intent of
(ConceptStr(# O,A #) .: )
by A63, CONLAT_1:def 24
.=
the
Extent of
ConceptStr(#
O,
A #)
by Def8
.=
the
Extent of
(a9 @ )
by A55, CONLAT_1:def 24
;
then
the
Extent of
(b9 @ ) c= the
Extent of
(a9 @ )
by A53, A62, CONLAT_1:31;
then
b9 @ is-SubConcept-of a9 @
by CONLAT_1:def 19;
then
b9 [= a9
by CONLAT_1:47;
then
b9 % <= a9 %
by LATTICE3:7;
then
[(b9 % ),(a9 % )] in the
InternalRel of
(LattPOSet (ConceptLattice C))
by ORDERS_2:def 9;
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 9;
hence
a [= b
by LATTICE3:7;
verum
end;
then reconsider f = f as Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .: ) by A15, A37, A38, 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:35;
then
CP in dom f
by A3, FUNCT_2:def 1;
then consider v being
set such that A64:
[CP,v] in f
by RELAT_1:def 4;
A65:
v in rng f
by A64, RELAT_1:def 5;
consider Ov being
Subset of the
carrier of
C,
Av being
Subset of the
carrier' of
C such that A66:
[CP,v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )]
and
ConceptStr(#
Ov,
Av #) is
FormalConcept of
C
by A64;
reconsider v =
v as
strict FormalConcept of
C .: by A1, A65, CONLAT_1:35;
A67:
CP =
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )] `1
by A66, MCART_1:def 1
.=
ConceptStr(#
Ov,
Av #)
by MCART_1:def 1
;
v =
[ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .: )] `2
by A66, MCART_1:def 2
.=
ConceptStr(#
Ov,
Av #)
.:
by MCART_1:def 2
;
hence
f . CP = CP .:
by A64, A67, FUNCT_1:8;
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