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