conlat_2.miz
begin
definition
let C be
FormalContext;
let CP be
strict
FormalConcept of C;
::
CONLAT_2:def1
func
@ CP ->
Element of (
ConceptLattice C) equals CP;
coherence
proof
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
hence thesis by
CONLAT_1: 31;
end;
end
registration
let C be
FormalContext;
cluster (
ConceptLattice C) ->
bounded;
coherence
proof
A1: ((
@ (
Concept-with-all-Objects C))
@ )
= (
Concept-with-all-Objects C) by
CONLAT_1:def 21;
A2: for a be
Element of (
ConceptLattice C) holds a
[= (
@ (
Concept-with-all-Objects C))
proof
let a be
Element of (
ConceptLattice C);
(a
@ )
is-SubConcept-of ((
@ (
Concept-with-all-Objects C))
@ ) by
A1,
CONLAT_1: 30;
hence thesis by
CONLAT_1: 43;
end;
for a be
Element of (
ConceptLattice C) holds ((
@ (
Concept-with-all-Objects C))
"\/" a)
= (
@ (
Concept-with-all-Objects C)) & (a
"\/" (
@ (
Concept-with-all-Objects C)))
= (
@ (
Concept-with-all-Objects C)) by
A2,
LATTICES:def 3;
then
A3: (
ConceptLattice C) is
upper-bounded by
LATTICES:def 14;
A4: ((
@ (
Concept-with-all-Attributes C))
@ )
= (
Concept-with-all-Attributes C) by
CONLAT_1:def 21;
A5: for a be
Element of (
ConceptLattice C) holds (
@ (
Concept-with-all-Attributes C))
[= a
proof
let a be
Element of (
ConceptLattice C);
((
@ (
Concept-with-all-Attributes C))
@ )
is-SubConcept-of (a
@ ) by
A4,
CONLAT_1: 30;
hence thesis by
CONLAT_1: 43;
end;
for a be
Element of (
ConceptLattice C) holds ((
@ (
Concept-with-all-Attributes C))
"/\" a)
= (
@ (
Concept-with-all-Attributes C)) & (a
"/\" (
@ (
Concept-with-all-Attributes C)))
= (
@ (
Concept-with-all-Attributes C)) by
A5,
LATTICES: 4;
then (
ConceptLattice C) is
lower-bounded by
LATTICES:def 13;
hence thesis by
A3;
end;
end
theorem ::
CONLAT_2:1
Th1: for C be
FormalContext holds (
Bottom (
ConceptLattice C))
= (
Concept-with-all-Attributes C) & (
Top (
ConceptLattice C))
= (
Concept-with-all-Objects C)
proof
let C be
FormalContext;
A1: ((
@ (
Concept-with-all-Objects C))
@ )
= (
Concept-with-all-Objects C) by
CONLAT_1:def 21;
A2: for a be
Element of (
ConceptLattice C) holds a
[= (
@ (
Concept-with-all-Objects C))
proof
let a be
Element of (
ConceptLattice C);
(a
@ )
is-SubConcept-of ((
@ (
Concept-with-all-Objects C))
@ ) by
A1,
CONLAT_1: 30;
hence thesis by
CONLAT_1: 43;
end;
A3: for a be
Element of (
ConceptLattice C) holds ((
@ (
Concept-with-all-Objects C))
"\/" a)
= (
@ (
Concept-with-all-Objects C)) & (a
"\/" (
@ (
Concept-with-all-Objects C)))
= (
@ (
Concept-with-all-Objects C)) by
A2,
LATTICES:def 3;
A4: ((
@ (
Concept-with-all-Attributes C))
@ )
= (
Concept-with-all-Attributes C) by
CONLAT_1:def 21;
A5: for a be
Element of (
ConceptLattice C) holds (
@ (
Concept-with-all-Attributes C))
[= a
proof
let a be
Element of (
ConceptLattice C);
((
@ (
Concept-with-all-Attributes C))
@ )
is-SubConcept-of (a
@ ) by
A4,
CONLAT_1: 30;
hence thesis by
CONLAT_1: 43;
end;
for a be
Element of (
ConceptLattice C) holds ((
@ (
Concept-with-all-Attributes C))
"/\" a)
= (
@ (
Concept-with-all-Attributes C)) & (a
"/\" (
@ (
Concept-with-all-Attributes C)))
= (
@ (
Concept-with-all-Attributes C)) by
A5,
LATTICES: 4;
hence thesis by
A3,
LATTICES:def 16,
LATTICES:def 17;
end;
theorem ::
CONLAT_2:2
Th2: for C be
FormalContext holds for D be non
empty
Subset-Family of the
carrier of C holds ((
ObjectDerivation C)
. (
union D))
= (
meet { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D })
proof
let C be
FormalContext;
let D be non
empty
Subset-Family of the
carrier of C;
reconsider D9 = D as non
empty
Subset-Family of the
carrier of C;
set OU = ((
ObjectDerivation C)
. (
union D));
set M = (
meet { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D });
per cases ;
suppose
A1: { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D }
<>
{} ;
thus OU
c= M
proof
let x be
object;
assume x
in OU;
then x
in { a9 where a9 be
Attribute of C : for o be
Object of C st o
in (
union D9) holds o
is-connected-with a9 } by
CONLAT_1:def 3;
then
A2: ex x9 be
Attribute of C st x9
= x & for o be
Object of C st o
in (
union D) holds o
is-connected-with x9;
then
reconsider x as
Attribute of C;
A3: for O be
Subset of the
carrier of C st O
in D holds for o be
Object of C st o
in O holds o
is-connected-with x
proof
let O be
Subset of the
carrier of C;
assume
A4: O
in D;
let o be
Object of C;
assume o
in O;
then o
in (
union D) by
A4,
TARSKI:def 4;
hence thesis by
A2;
end;
A5: for O be
Subset of the
carrier of C st O
in D holds x
in ((
ObjectDerivation C)
. O)
proof
let O be
Subset of the
carrier of C;
assume O
in D;
then for o be
Object of C st o
in O holds o
is-connected-with x by
A3;
then x
in { a where a be
Attribute of C : for o be
Object of C st o
in O holds o
is-connected-with a };
hence thesis by
CONLAT_1:def 3;
end;
for Y be
set holds Y
in { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D } implies x
in Y
proof
let Y be
set;
assume Y
in { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D };
then ex O be
Subset of the
carrier of C st Y
= ((
ObjectDerivation C)
. O) & O
in D;
hence thesis by
A5;
end;
hence thesis by
A1,
SETFAM_1:def 1;
end;
thus M
c= OU
proof
set d = the
Element of { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D };
let x be
object;
assume
A6: x
in M;
then
A7: x
in d by
A1,
SETFAM_1:def 1;
d
in { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D } by
A1;
then ex X be
Subset of the
carrier of C st d
= ((
ObjectDerivation C)
. X) & X
in D;
then
reconsider x as
Attribute of C by
A7;
A8: for O be
Subset of the
carrier of C st O
in D holds x
in ((
ObjectDerivation C)
. O)
proof
let O be
Subset of the
carrier of C;
assume O
in D;
then ((
ObjectDerivation C)
. O)
in { ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in D };
hence thesis by
A6,
SETFAM_1:def 1;
end;
A9: for O be
Subset of the
carrier of C st O
in D holds for o be
Object of C st o
in O holds o
is-connected-with x
proof
let O be
Subset of the
carrier of C;
assume O
in D;
then x
in ((
ObjectDerivation C)
. O) by
A8;
then x
in { a where a be
Attribute of C : for o be
Object of C st o
in O holds o
is-connected-with a } by
CONLAT_1:def 3;
then
A10: ex x9 be
Attribute of C st x9
= x & for o be
Object of C st o
in O holds o
is-connected-with x9;
let o be
Object of C;
assume o
in O;
hence thesis by
A10;
end;
for o be
Object of C st o
in (
union D) holds o
is-connected-with x
proof
let o be
Object of C;
assume o
in (
union D);
then ex Y be
set st o
in Y & Y
in D by
TARSKI:def 4;
hence thesis by
A9;
end;
then x
in { a9 where a9 be
Attribute of C : for o be
Object of C st o
in (
union D9) holds o
is-connected-with a9 };
hence thesis by
CONLAT_1:def 3;
end;
end;
suppose
A11: { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D }
=
{} ;
D
=
{}
proof
set x = the
Element of D;
assume D
<>
{} ;
((
ObjectDerivation C)
. x)
in { ((
ObjectDerivation C)
. O) where O be
Subset of the
carrier of C : O
in D };
hence thesis by
A11;
end;
hence thesis;
end;
end;
theorem ::
CONLAT_2:3
Th3: for C be
FormalContext holds for D be non
empty
Subset-Family of the
carrier' of C holds ((
AttributeDerivation C)
. (
union D))
= (
meet { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D })
proof
let C be
FormalContext;
let D be non
empty
Subset-Family of the
carrier' of C;
reconsider D9 = D as non
empty
Subset-Family of the
carrier' of C;
set OU = ((
AttributeDerivation C)
. (
union D));
set M = (
meet { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D });
now
per cases ;
case
A1: { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D }
<>
{} ;
thus OU
= M
proof
thus OU
c= M
proof
let x be
object;
assume x
in OU;
then x
in { o9 where o9 be
Object of C : for a be
Attribute of C st a
in (
union D9) holds o9
is-connected-with a } by
CONLAT_1:def 4;
then
A2: ex x9 be
Object of C st x9
= x & for a be
Attribute of C st a
in (
union D) holds x9
is-connected-with a;
then
reconsider x as
Object of C;
A3: for A be
Subset of the
carrier' of C st A
in D holds for a be
Attribute of C st a
in A holds x
is-connected-with a
proof
let A be
Subset of the
carrier' of C;
assume
A4: A
in D;
let a be
Attribute of C;
assume a
in A;
then a
in (
union D) by
A4,
TARSKI:def 4;
hence thesis by
A2;
end;
A5: for A be
Subset of the
carrier' of C st A
in D holds x
in ((
AttributeDerivation C)
. A)
proof
let A be
Subset of the
carrier' of C;
assume A
in D;
then for a be
Attribute of C st a
in A holds x
is-connected-with a by
A3;
then x
in { o where o be
Object of C : for a be
Attribute of C st a
in A holds o
is-connected-with a };
hence thesis by
CONLAT_1:def 4;
end;
for Y be
set holds Y
in { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D } implies x
in Y
proof
let Y be
set;
assume Y
in { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D };
then ex A be
Subset of the
carrier' of C st Y
= ((
AttributeDerivation C)
. A) & A
in D;
hence thesis by
A5;
end;
hence thesis by
A1,
SETFAM_1:def 1;
end;
set d = the
Element of { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D };
let x be
object;
assume
A6: x
in M;
then
A7: x
in d by
A1,
SETFAM_1:def 1;
d
in { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D } by
A1;
then ex X be
Subset of the
carrier' of C st d
= ((
AttributeDerivation C)
. X) & X
in D;
then
reconsider x as
Object of C by
A7;
A8: for A be
Subset of the
carrier' of C st A
in D holds x
in ((
AttributeDerivation C)
. A)
proof
let A be
Subset of the
carrier' of C;
assume A
in D;
then ((
AttributeDerivation C)
. A)
in { ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in D };
hence thesis by
A6,
SETFAM_1:def 1;
end;
A9: for A be
Subset of the
carrier' of C st A
in D holds for a be
Attribute of C st a
in A holds x
is-connected-with a
proof
let A be
Subset of the
carrier' of C;
assume A
in D;
then x
in ((
AttributeDerivation C)
. A) by
A8;
then x
in { o where o be
Object of C : for a be
Attribute of C st a
in A holds o
is-connected-with a } by
CONLAT_1:def 4;
then
A10: ex x9 be
Object of C st x9
= x & for a be
Attribute of C st a
in A holds x9
is-connected-with a;
let a be
Attribute of C;
assume a
in A;
hence thesis by
A10;
end;
for a be
Attribute of C st a
in (
union D) holds x
is-connected-with a
proof
let a be
Attribute of C;
assume a
in (
union D);
then ex Y be
set st a
in Y & Y
in D by
TARSKI:def 4;
hence thesis by
A9;
end;
then x
in { o9 where o9 be
Object of C : for a be
Attribute of C st a
in (
union D9) holds o9
is-connected-with a };
hence thesis by
CONLAT_1:def 4;
end;
end;
case
A11: { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D }
=
{} ;
D
=
{}
proof
set x = the
Element of D;
assume D
<>
{} ;
((
AttributeDerivation C)
. x)
in { ((
AttributeDerivation C)
. A) where A be
Subset of the
carrier' of C : A
in D };
hence thesis by
A11;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem ::
CONLAT_2:4
Th4: for C be
FormalContext holds for D be
Subset of (
ConceptLattice C) holds (
"/\" (D,(
ConceptLattice C))) is
FormalConcept of C & (
"\/" (D,(
ConceptLattice C))) is
FormalConcept of C
proof
let C be
FormalContext;
let D be
Subset of (
ConceptLattice C);
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
hence thesis by
CONLAT_1: 31;
end;
definition
let C be
FormalContext;
let D be
Subset of (
ConceptLattice C);
::
CONLAT_2:def2
func
"/\" (D,C) ->
FormalConcept of C equals (
"/\" (D,(
ConceptLattice C)));
coherence by
Th4;
::
CONLAT_2:def3
func
"\/" (D,C) ->
FormalConcept of C equals (
"\/" (D,(
ConceptLattice C)));
coherence by
Th4;
end
theorem ::
CONLAT_2:5
for C be
FormalContext holds (
"\/" ((
{} (
ConceptLattice C)),C))
= (
Concept-with-all-Attributes C) & (
"/\" ((
{} (
ConceptLattice C)),C))
= (
Concept-with-all-Objects C)
proof
let C be
FormalContext;
A1: for b be
Element of (
ConceptLattice C) st b
is_less_than
{} holds b
[= (
@ (
Concept-with-all-Objects C))
proof
let b be
Element of (
ConceptLattice C);
assume b
is_less_than
{} ;
(b
@ )
is-SubConcept-of (
Concept-with-all-Objects C) & (
Concept-with-all-Objects C)
= ((
@ (
Concept-with-all-Objects C))
@ ) by
CONLAT_1: 30,
CONLAT_1:def 21;
hence thesis by
CONLAT_1: 43;
end;
(
"\/" ((
{} (
ConceptLattice C)),C))
= (
Bottom (
ConceptLattice C)) & (
@ (
Concept-with-all-Objects C))
is_less_than
{} by
LATTICE3: 49;
hence thesis by
A1,
Th1,
LATTICE3: 34;
end;
theorem ::
CONLAT_2:6
for C be
FormalContext holds (
"\/" ((
[#] the
carrier of (
ConceptLattice C)),C))
= (
Concept-with-all-Objects C) & (
"/\" ((
[#] the
carrier of (
ConceptLattice C)),C))
= (
Concept-with-all-Attributes C)
proof
let C be
FormalContext;
A1: (
@ (
Concept-with-all-Attributes C))
is_less_than (
[#] the
carrier of (
ConceptLattice C))
proof
let q be
Element of (
ConceptLattice C);
assume q
in (
[#] the
carrier of (
ConceptLattice C));
(
Concept-with-all-Attributes C)
is-SubConcept-of (q
@ ) & (
Concept-with-all-Attributes C)
= ((
@ (
Concept-with-all-Attributes C))
@ ) by
CONLAT_1: 30,
CONLAT_1:def 21;
hence thesis by
CONLAT_1: 43;
end;
(
"\/" (the
carrier of (
ConceptLattice C),(
ConceptLattice C)))
= (
Top (
ConceptLattice C)) & for b be
Element of (
ConceptLattice C) st b
is_less_than (
[#] the
carrier of (
ConceptLattice C)) holds b
[= (
@ (
Concept-with-all-Attributes C)) by
LATTICE3: 50;
hence thesis by
A1,
Th1,
LATTICE3: 34;
end;
theorem ::
CONLAT_2:7
for C be
FormalContext holds for D be non
empty
Subset of (
ConceptLattice C) holds the
Extent of (
"\/" (D,C))
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
. (
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }))) & the
Intent of (
"\/" (D,C))
= (
meet { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })
proof
let C be
FormalContext;
let D be non
empty
Subset of (
ConceptLattice C);
set O = ((
AttributeDerivation C)
. ((
ObjectDerivation C)
. (
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })));
set A9 = ((
ObjectDerivation C)
. (
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }));
set y = the
Element of D;
{ the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
c= (
bool the
carrier of C)
proof
let x be
object;
assume x
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st x
= the
Extent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D;
hence thesis;
end;
then
reconsider OO = { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } as
Subset-Family of the
carrier of C;
O
c= the
carrier of C
proof
set u = (
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D });
u
c= the
carrier of C
proof
let x be
object;
assume x
in u;
then
consider Y be
set such that
A1: x
in Y and
A2: Y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
TARSKI:def 4;
ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st Y
= the
Extent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D by
A2;
hence thesis by
A1;
end;
then
reconsider u as
Subset of the
carrier of C;
let x be
object;
A3: ((
AttributeDerivation C)
. ((
ObjectDerivation C)
. u)) is
Element of (
bool the
carrier of C);
assume x
in O;
hence thesis by
A3;
end;
then
reconsider o = O as
Subset of the
carrier of C;
A4: (
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
A5: for x be
object holds x
in D implies x is
strict
FormalConcept of C & ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st x
=
ConceptStr (# E, I #)
proof
let x be
object;
assume x
in D;
then x is
strict
FormalConcept of C by
A4,
CONLAT_1: 31;
hence thesis;
end;
then ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #);
then the
Extent of y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
reconsider OO as non
empty
Subset-Family of the
carrier of C;
A6: { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
c= { ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
proof
let x be
object;
assume x
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
consider E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C such that
A7: x
= the
Intent of
ConceptStr (# E, I #) and
A8:
ConceptStr (# E, I #)
in D;
ConceptStr (# E, I #) is
FormalConcept of C by
A5,
A8;
then
A9: x
= ((
ObjectDerivation C)
. the
Extent of
ConceptStr (# E, I #)) by
A7,
CONLAT_1:def 10;
the
Extent of
ConceptStr (# E, I #)
in { the
Extent of
ConceptStr (# EE, II #) where EE be
Subset of the
carrier of C, II be
Subset of the
carrier' of C :
ConceptStr (# EE, II #)
in D } by
A8;
hence thesis by
A9;
end;
{ ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
c= { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
proof
let x be
object;
assume x
in { ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } };
then
consider O9 be
Subset of the
carrier of C such that
A10: x
= ((
ObjectDerivation C)
. O9) and
A11: O9
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
consider E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C such that
A12: O9
= the
Extent of
ConceptStr (# E, I #) and
A13:
ConceptStr (# E, I #)
in D by
A11;
ConceptStr (# E, I #) is
FormalConcept of C by
A5,
A13;
then x
= the
Intent of
ConceptStr (# E, I #) by
A10,
A12,
CONLAT_1:def 10;
hence thesis by
A13;
end;
then
A14: { ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
= { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
A6;
A15: A9
= (
meet { ((
ObjectDerivation C)
. O9) where O9 be
Subset of the
carrier of C : O9
in OO }) by
Th2;
A9
c= the
carrier' of C
proof
set y = the
Element of D;
set Y = the
Element of { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
let x be
object;
ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #) by
A5;
then
A16: the
Intent of y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then Y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
A17: ex E1 be
Subset of the
carrier of C, I1 be
Subset of the
carrier' of C st Y
= the
Intent of
ConceptStr (# E1, I1 #) &
ConceptStr (# E1, I1 #)
in D;
assume x
in A9;
then x
in Y by
A15,
A14,
A16,
SETFAM_1:def 1;
hence thesis by
A17;
end;
then
reconsider a = A9 as
Subset of the
carrier' of C;
(
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })
c= the
carrier of C
proof
let x be
object;
assume x
in (
union { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D });
then
consider Y be
set such that
A18: x
in Y and
A19: Y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
TARSKI:def 4;
ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st Y
= the
Extent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D by
A19;
hence thesis by
A18;
end;
then
reconsider CP9 =
ConceptStr (# o, a #) as
strict
FormalConcept of C by
CONLAT_1: 19;
reconsider CP = CP9 as
Element of (
ConceptLattice C) by
A4,
CONLAT_1: 31;
A20: the
Intent of (CP
@ )
= (
meet { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }) by
A15,
A14,
CONLAT_1:def 21;
A21: for r be
Element of (
ConceptLattice C) st D
is_less_than r holds CP
[= r
proof
let r be
Element of (
ConceptLattice C);
assume
A22: D
is_less_than r;
A23: for q be
Element of (
ConceptLattice C) st q
in D holds the
Intent of (r
@ )
c= the
Intent of (q
@ )
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then q
[= r by
A22;
then (q
@ )
is-SubConcept-of (r
@ ) by
CONLAT_1: 43;
hence thesis by
CONLAT_1: 28;
end;
the
Intent of (r
@ )
c= (
meet { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })
proof
set y = the
Element of D;
let x be
object;
assume
A24: x
in the
Intent of (r
@ );
A25: for Y be
set holds Y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } implies x
in Y
proof
let Y be
set;
assume Y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
consider Ey be
Subset of the
carrier of C, Iy be
Subset of the
carrier' of C such that
A26: Y
= the
Intent of
ConceptStr (# Ey, Iy #) and
A27:
ConceptStr (# Ey, Iy #)
in D;
reconsider C1 =
ConceptStr (# Ey, Iy #) as
Element of (
ConceptLattice C) by
A27;
the
Intent of (r
@ )
c= the
Intent of (C1
@ ) by
A23,
A27;
then x
in the
Intent of (C1
@ ) by
A24;
hence thesis by
A26,
CONLAT_1:def 21;
end;
ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #) by
A5;
then the
Intent of y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
hence thesis by
A25,
SETFAM_1:def 1;
end;
then (CP
@ )
is-SubConcept-of (r
@ ) by
A20,
CONLAT_1: 28;
hence thesis by
CONLAT_1: 43;
end;
D
is_less_than CP
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then (q
@ )
in D by
CONLAT_1:def 21;
then the
Intent of (q
@ )
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then the
Intent of (CP
@ )
c= the
Intent of (q
@ ) by
A20,
SETFAM_1: 3;
then (q
@ )
is-SubConcept-of (CP
@ ) by
CONLAT_1: 28;
hence thesis by
CONLAT_1: 43;
end;
hence thesis by
A15,
A14,
A21,
LATTICE3:def 21;
end;
theorem ::
CONLAT_2:8
for C be
FormalContext holds for D be non
empty
Subset of (
ConceptLattice C) holds the
Extent of (
"/\" (D,C))
= (
meet { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }) & the
Intent of (
"/\" (D,C))
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
. (
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })))
proof
let C be
FormalContext;
let D be non
empty
Subset of (
ConceptLattice C);
set A = ((
ObjectDerivation C)
. ((
AttributeDerivation C)
. (
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })));
set O9 = ((
AttributeDerivation C)
. (
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }));
set y = the
Element of D;
{ the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
c= (
bool the
carrier' of C)
proof
let x be
object;
assume x
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st x
= the
Intent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D;
hence thesis;
end;
then
reconsider AA = { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } as
Subset-Family of the
carrier' of C;
A
c= the
carrier' of C
proof
set u = (
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D });
u
c= the
carrier' of C
proof
let x be
object;
assume x
in u;
then
consider Y be
set such that
A1: x
in Y and
A2: Y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
TARSKI:def 4;
ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st Y
= the
Intent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D by
A2;
hence thesis by
A1;
end;
then
reconsider u as
Subset of the
carrier' of C;
let x be
object;
A3: ((
ObjectDerivation C)
. ((
AttributeDerivation C)
. u)) is
Element of (
bool the
carrier' of C);
assume x
in A;
hence thesis by
A3;
end;
then
reconsider a = A as
Subset of the
carrier' of C;
A4: (
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
A5: for x be
object holds x
in D implies x is
strict
FormalConcept of C & ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st x
=
ConceptStr (# E, I #)
proof
let x be
object;
assume x
in D;
then x is
strict
FormalConcept of C by
A4,
CONLAT_1: 31;
hence thesis;
end;
then ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #);
then the
Intent of y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
reconsider AA as non
empty
Subset-Family of the
carrier' of C;
A6: { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
c= { ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
proof
let x be
object;
assume x
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
consider E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C such that
A7: x
= the
Extent of
ConceptStr (# E, I #) and
A8:
ConceptStr (# E, I #)
in D;
ConceptStr (# E, I #) is
FormalConcept of C by
A5,
A8;
then
A9: x
= ((
AttributeDerivation C)
. the
Intent of
ConceptStr (# E, I #)) by
A7,
CONLAT_1:def 10;
the
Intent of
ConceptStr (# E, I #)
in { the
Intent of
ConceptStr (# EE, II #) where EE be
Subset of the
carrier of C, II be
Subset of the
carrier' of C :
ConceptStr (# EE, II #)
in D } by
A8;
hence thesis by
A9;
end;
{ ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
c= { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }
proof
let x be
object;
assume x
in { ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } };
then
consider A9 be
Subset of the
carrier' of C such that
A10: x
= ((
AttributeDerivation C)
. A9) and
A11: A9
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
consider E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C such that
A12: A9
= the
Intent of
ConceptStr (# E, I #) and
A13:
ConceptStr (# E, I #)
in D by
A11;
ConceptStr (# E, I #) is
FormalConcept of C by
A5,
A13;
then x
= the
Extent of
ConceptStr (# E, I #) by
A10,
A12,
CONLAT_1:def 10;
hence thesis by
A13;
end;
then
A14: { ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } }
= { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
A6;
A15: O9
= (
meet { ((
AttributeDerivation C)
. A9) where A9 be
Subset of the
carrier' of C : A9
in AA }) by
Th3;
O9
c= the
carrier of C
proof
set y = the
Element of D;
set Y = the
Element of { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
let x be
object;
ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #) by
A5;
then
A16: the
Extent of y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then Y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
A17: ex E1 be
Subset of the
carrier of C, I1 be
Subset of the
carrier' of C st Y
= the
Extent of
ConceptStr (# E1, I1 #) &
ConceptStr (# E1, I1 #)
in D;
assume x
in O9;
then x
in Y by
A15,
A14,
A16,
SETFAM_1:def 1;
hence thesis by
A17;
end;
then
reconsider o = O9 as
Subset of the
carrier of C;
(
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })
c= the
carrier' of C
proof
let x be
object;
assume x
in (
union { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D });
then
consider Y be
set such that
A18: x
in Y and
A19: Y
in { the
Intent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } by
TARSKI:def 4;
ex E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C st Y
= the
Intent of
ConceptStr (# E, I #) &
ConceptStr (# E, I #)
in D by
A19;
hence thesis by
A18;
end;
then
reconsider CP9 =
ConceptStr (# o, a #) as
strict
FormalConcept of C by
CONLAT_1: 21;
reconsider CP = CP9 as
Element of (
ConceptLattice C) by
A4,
CONLAT_1: 31;
A20: the
Extent of (CP
@ )
= (
meet { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D }) by
A15,
A14,
CONLAT_1:def 21;
A21: for r be
Element of (
ConceptLattice C) st r
is_less_than D holds r
[= CP
proof
let r be
Element of (
ConceptLattice C);
assume
A22: r
is_less_than D;
A23: for q be
Element of (
ConceptLattice C) st q
in D holds the
Extent of (r
@ )
c= the
Extent of (q
@ )
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then r
[= q by
A22;
then (r
@ )
is-SubConcept-of (q
@ ) by
CONLAT_1: 43;
hence thesis by
CONLAT_1:def 16;
end;
the
Extent of (r
@ )
c= (
meet { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D })
proof
set y = the
Element of D;
let x be
object;
assume
A24: x
in the
Extent of (r
@ );
A25: for Y be
set holds Y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D } implies x
in Y
proof
let Y be
set;
assume Y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then
consider Ey be
Subset of the
carrier of C, Iy be
Subset of the
carrier' of C such that
A26: Y
= the
Extent of
ConceptStr (# Ey, Iy #) and
A27:
ConceptStr (# Ey, Iy #)
in D;
reconsider C1 =
ConceptStr (# Ey, Iy #) as
Element of (
ConceptLattice C) by
A27;
the
Extent of (r
@ )
c= the
Extent of (C1
@ ) by
A23,
A27;
then x
in the
Extent of (C1
@ ) by
A24;
hence thesis by
A26,
CONLAT_1:def 21;
end;
ex E9 be
Subset of the
carrier of C, I9 be
Subset of the
carrier' of C st y
=
ConceptStr (# E9, I9 #) by
A5;
then the
Extent of y
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
hence thesis by
A25,
SETFAM_1:def 1;
end;
then (r
@ )
is-SubConcept-of (CP
@ ) by
A20,
CONLAT_1:def 16;
hence thesis by
CONLAT_1: 43;
end;
CP
is_less_than D
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then (q
@ )
in D by
CONLAT_1:def 21;
then the
Extent of (q
@ )
in { the
Extent of
ConceptStr (# E, I #) where E be
Subset of the
carrier of C, I be
Subset of the
carrier' of C :
ConceptStr (# E, I #)
in D };
then the
Extent of (CP
@ )
c= the
Extent of (q
@ ) by
A20,
SETFAM_1: 3;
then (CP
@ )
is-SubConcept-of (q
@ ) by
CONLAT_1:def 16;
hence thesis by
CONLAT_1: 43;
end;
hence thesis by
A15,
A14,
A21,
LATTICE3: 34;
end;
theorem ::
CONLAT_2:9
Th9: for C be
FormalContext holds for CP be
strict
FormalConcept of C holds (
"\/" ({
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of CP & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) },(
ConceptLattice C)))
= CP
proof
let C be
FormalContext;
let CP be
strict
FormalConcept of C;
set D = {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of CP & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) };
A1: for CP9 be
Element of (
ConceptLattice C) st D
is_less_than CP9 holds (
@ CP)
[= CP9
proof
let CP9 be
Element of (
ConceptLattice C);
assume
A2: D
is_less_than CP9;
A3: the
Extent of CP
c= the
Extent of (CP9
@ )
proof
let x be
object;
assume
A4: x
in the
Extent of CP;
then
reconsider x as
Element of C;
set Ax = ((
ObjectDerivation C)
.
{x});
set Ox = ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{x}));
reconsider Cx =
ConceptStr (# Ox, Ax #) as
strict
FormalConcept of C by
CONLAT_1: 19;
Cx
in {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of CP & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) } by
A4;
then (
@ Cx)
[= CP9 by
A2;
then
A5: ((
@ Cx)
@ )
is-SubConcept-of (CP9
@ ) by
CONLAT_1: 43;
{x}
c= Ox by
CONLAT_1: 5;
then
A6: x
in the
Extent of Cx by
ZFMISC_1: 31;
Cx
= ((
@ Cx)
@ ) by
CONLAT_1:def 21;
then the
Extent of Cx
c= the
Extent of (CP9
@ ) by
A5,
CONLAT_1:def 16;
hence thesis by
A6;
end;
CP
= ((
@ CP)
@ ) by
CONLAT_1:def 21;
then ((
@ CP)
@ )
is-SubConcept-of (CP9
@ ) by
A3,
CONLAT_1:def 16;
hence thesis by
CONLAT_1: 43;
end;
D
is_less_than (
@ CP)
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A7: q
=
ConceptStr (# O, A #) and
A8: ex o be
Object of C st o
in the
Extent of CP & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o});
consider o be
Object of C such that
A9: o
in the
Extent of CP and O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) and
A10: A
= ((
ObjectDerivation C)
.
{o}) by
A8;
A11:
{o}
c= the
Extent of CP by
A9,
ZFMISC_1: 31;
((
ObjectDerivation C)
. the
Extent of CP)
= the
Intent of CP & the
Intent of (q
@ )
= ((
ObjectDerivation C)
.
{o}) by
A7,
A10,
CONLAT_1:def 10,
CONLAT_1:def 21;
then the
Intent of CP
c= the
Intent of (q
@ ) by
A11,
CONLAT_1: 3;
then
A12: (q
@ )
is-SubConcept-of CP by
CONLAT_1: 28;
CP
= ((
@ CP)
@ ) by
CONLAT_1:def 21;
hence thesis by
A12,
CONLAT_1: 43;
end;
hence thesis by
A1,
LATTICE3:def 21;
end;
theorem ::
CONLAT_2:10
Th10: for C be
FormalContext holds for CP be
strict
FormalConcept of C holds (
"/\" ({
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of CP & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) },(
ConceptLattice C)))
= CP
proof
let C be
FormalContext;
let CP be
strict
FormalConcept of C;
set D = {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of CP & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) };
A1: for CP9 be
Element of (
ConceptLattice C) st CP9
is_less_than D holds CP9
[= (
@ CP)
proof
let CP9 be
Element of (
ConceptLattice C);
assume
A2: CP9
is_less_than D;
A3: the
Intent of CP
c= the
Intent of (CP9
@ )
proof
let x be
object;
assume
A4: x
in the
Intent of CP;
then
reconsider x as
Element of the
carrier' of C;
set Ax = ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{x}));
set Ox = ((
AttributeDerivation C)
.
{x});
reconsider Cx =
ConceptStr (# Ox, Ax #) as
strict
FormalConcept of C by
CONLAT_1: 21;
Cx
in {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of CP & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) } by
A4;
then CP9
[= (
@ Cx) by
A2;
then
A5: (CP9
@ )
is-SubConcept-of ((
@ Cx)
@ ) by
CONLAT_1: 43;
{x}
c= Ax by
CONLAT_1: 6;
then
A6: x
in the
Intent of Cx by
ZFMISC_1: 31;
Cx
= ((
@ Cx)
@ ) by
CONLAT_1:def 21;
then the
Intent of Cx
c= the
Intent of (CP9
@ ) by
A5,
CONLAT_1: 28;
hence thesis by
A6;
end;
CP
= ((
@ CP)
@ ) by
CONLAT_1:def 21;
then (CP9
@ )
is-SubConcept-of ((
@ CP)
@ ) by
A3,
CONLAT_1: 28;
hence thesis by
CONLAT_1: 43;
end;
(
@ CP)
is_less_than D
proof
let q be
Element of (
ConceptLattice C);
assume q
in D;
then
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A7: q
=
ConceptStr (# O, A #) and
A8: ex a be
Attribute of C st a
in the
Intent of CP & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}));
consider a be
Attribute of C such that
A9: a
in the
Intent of CP and
A10: O
= ((
AttributeDerivation C)
.
{a}) and A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
A8;
A11:
{a}
c= the
Intent of CP by
A9,
ZFMISC_1: 31;
((
AttributeDerivation C)
. the
Intent of CP)
= the
Extent of CP & the
Extent of (q
@ )
= ((
AttributeDerivation C)
.
{a}) by
A7,
A10,
CONLAT_1:def 10,
CONLAT_1:def 21;
then the
Extent of CP
c= the
Extent of (q
@ ) by
A11,
CONLAT_1: 4;
then
A12: CP
is-SubConcept-of (q
@ ) by
CONLAT_1:def 16;
CP
= ((
@ CP)
@ ) by
CONLAT_1:def 21;
hence thesis by
A12,
CONLAT_1: 43;
end;
hence thesis by
A1,
LATTICE3: 34;
end;
definition
let C be
FormalContext;
::
CONLAT_2:def4
func
gamma (C) ->
Function of the
carrier of C, the
carrier of (
ConceptLattice C) means
:
Def4: for o be
Element of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (it
. o)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o});
existence
proof
defpred
P[
object,
object] means ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st $2
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{$1})) & A
= ((
ObjectDerivation C)
.
{$1});
A1: for e be
object st e
in the
carrier of C holds ex u be
object st u
in the
carrier of (
ConceptLattice C) &
P[e, u]
proof
let e be
object;
assume e
in the
carrier of C;
then
reconsider se =
{e} as
Subset of the
carrier of C by
ZFMISC_1: 31;
set A = ((
ObjectDerivation C)
. se);
set O = ((
AttributeDerivation C)
. ((
ObjectDerivation C)
. se));
take
ConceptStr (# O, A #);
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) &
ConceptStr (# O, A #) is
FormalConcept of C by
CONLAT_1: 19,
CONLAT_1:def 20;
hence thesis by
CONLAT_1: 31;
end;
consider f be
Function of the
carrier of C, the
carrier of (
ConceptLattice C) such that
A2: for e be
object st e
in the
carrier of C holds
P[e, (f
. e)] from
FUNCT_2:sch 1(
A1);
take f;
let o be
Element of C;
thus thesis by
A2;
end;
uniqueness
proof
let F1,F2 be
Function of the
carrier of C, the
carrier of (
ConceptLattice C);
assume
A3: for o be
Element of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F1
. o)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o});
assume
A4: for o be
Element of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F2
. o)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o});
A5: for o be
object st o
in the
carrier of C holds (F1
. o)
= (F2
. o)
proof
let o be
object;
assume o
in the
carrier of C;
then
reconsider o as
Element of C;
(ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F1
. o)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o})) & ex O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C st (F2
. o)
=
ConceptStr (# O9, A9 #) & O9
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A9
= ((
ObjectDerivation C)
.
{o}) by
A3,
A4;
hence thesis;
end;
(
dom F1)
= the
carrier of C & (
dom F2)
= the
carrier of C by
FUNCT_2:def 1;
hence thesis by
A5;
end;
end
definition
let C be
FormalContext;
::
CONLAT_2:def5
func
delta (C) ->
Function of the
carrier' of C, the
carrier of (
ConceptLattice C) means
:
Def5: for a be
Element of the
carrier' of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (it
. a)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}));
existence
proof
defpred
P[
object,
object] means ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st $2
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
.
{$1}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{$1}));
A1: for e be
object st e
in the
carrier' of C holds ex u be
object st u
in the
carrier of (
ConceptLattice C) &
P[e, u]
proof
let e be
object;
assume e
in the
carrier' of C;
then
reconsider se =
{e} as
Subset of the
carrier' of C by
ZFMISC_1: 31;
set A = ((
ObjectDerivation C)
. ((
AttributeDerivation C)
. se));
set O = ((
AttributeDerivation C)
. se);
take
ConceptStr (# O, A #);
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) &
ConceptStr (# O, A #) is
FormalConcept of C by
CONLAT_1: 21,
CONLAT_1:def 20;
hence thesis by
CONLAT_1: 31;
end;
consider f be
Function of the
carrier' of C, the
carrier of (
ConceptLattice C) such that
A2: for e be
object st e
in the
carrier' of C holds
P[e, (f
. e)] from
FUNCT_2:sch 1(
A1);
take f;
let o be
Element of the
carrier' of C;
thus thesis by
A2;
end;
uniqueness
proof
let F1,F2 be
Function of the
carrier' of C, the
carrier of (
ConceptLattice C);
assume
A3: for a be
Element of the
carrier' of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F1
. a)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}));
assume
A4: for a be
Element of the
carrier' of C holds ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F2
. a)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}));
A5: for a be
object st a
in the
carrier' of C holds (F1
. a)
= (F2
. a)
proof
let a be
object;
assume a
in the
carrier' of C;
then
reconsider a as
Element of the
carrier' of C;
(ex O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C st (F1
. a)
=
ConceptStr (# O, A #) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}))) & ex O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C st (F2
. a)
=
ConceptStr (# O9, A9 #) & O9
= ((
AttributeDerivation C)
.
{a}) & A9
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
A3,
A4;
hence thesis;
end;
(
dom F1)
= the
carrier' of C & (
dom F2)
= the
carrier' of C by
FUNCT_2:def 1;
hence thesis by
A5;
end;
end
theorem ::
CONLAT_2:11
for C be
FormalContext holds for o be
Object of C holds for a be
Attribute of C holds ((
gamma C)
. o) is
FormalConcept of C & ((
delta C)
. a) is
FormalConcept of C
proof
let C be
FormalContext;
let o be
Object of C;
let a be
Attribute of C;
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
hence thesis by
CONLAT_1:def 15;
end;
theorem ::
CONLAT_2:12
Th12: for C be
FormalContext holds (
rng (
gamma C)) is
supremum-dense & (
rng (
delta C)) is
infimum-dense
proof
let C be
FormalContext;
set G = (
rng (
gamma C));
thus G is
supremum-dense
proof
let a be
Element of (
ConceptLattice C);
A1: {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of (a
@ ) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) }
c= G
proof
let x be
object;
assume x
in {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of (a
@ ) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) };
then
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A2: x
=
ConceptStr (# O, A #) and
A3: ex o be
Object of C st o
in the
Extent of (a
@ ) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o});
consider o be
Object of C such that o
in the
Extent of (a
@ ) and O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) and
A4: A
= ((
ObjectDerivation C)
.
{o}) by
A3;
consider y be
Element of (
ConceptLattice C) such that
A5: ((
gamma C)
. o)
= y;
(
dom (
gamma C))
= the
carrier of C & ex O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C st y
=
ConceptStr (# O9, A9 #) & O9
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A9
= ((
ObjectDerivation C)
.
{o}) by
A5,
Def4,
FUNCT_2:def 1;
hence thesis by
A2,
A3,
A4,
A5,
FUNCT_1:def 3;
end;
(
"\/" ({
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex o be
Object of C st o
in the
Extent of (a
@ ) & O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) & A
= ((
ObjectDerivation C)
.
{o}) },(
ConceptLattice C)))
= (a
@ ) & a
= (a
@ ) by
Th9,
CONLAT_1:def 21;
hence thesis by
A1;
end;
let b be
Element of (
ConceptLattice C);
set G = (
rng (
delta C));
A6: {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of (b
@ ) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) }
c= G
proof
let x be
object;
assume x
in {
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of (b
@ ) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) };
then
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A7: x
=
ConceptStr (# O, A #) and
A8: ex a be
Attribute of C st a
in the
Intent of (b
@ ) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a}));
consider a be
Attribute of C such that a
in the
Intent of (b
@ ) and
A9: O
= ((
AttributeDerivation C)
.
{a}) and A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
A8;
consider y be
Element of (
ConceptLattice C) such that
A10: ((
delta C)
. a)
= y;
(
dom (
delta C))
= the
carrier' of C & ex O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C st y
=
ConceptStr (# O9, A9 #) & O9
= ((
AttributeDerivation C)
.
{a}) & A9
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
A10,
Def5,
FUNCT_2:def 1;
hence thesis by
A7,
A8,
A9,
A10,
FUNCT_1:def 3;
end;
(
"/\" ({
ConceptStr (# O, A #) where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : ex a be
Attribute of C st a
in the
Intent of (b
@ ) & O
= ((
AttributeDerivation C)
.
{a}) & A
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) },(
ConceptLattice C)))
= (b
@ ) & b
= (b
@ ) by
Th10,
CONLAT_1:def 21;
hence thesis by
A6;
end;
theorem ::
CONLAT_2:13
Th13: for C be
FormalContext holds for o be
Object of C holds for a be
Attribute of C holds o
is-connected-with a iff ((
gamma C)
. o)
[= ((
delta C)
. a)
proof
let C be
FormalContext;
let o be
Object of C;
let a be
Attribute of C;
set aa =
{a};
set o9 =
{o};
set oo = ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o}));
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A1: ((
gamma C)
. o)
=
ConceptStr (# O, A #) and
A2: O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) and A
= ((
ObjectDerivation C)
.
{o}) by
Def4;
hereby
assume o
is-connected-with a;
then a
in { a9 where a9 be
Attribute of C : o
is-connected-with a9 };
then a
in ((
ObjectDerivation C)
.
{o}) by
CONLAT_1: 1;
then
A3:
{a}
c= ((
ObjectDerivation C)
.
{o}) by
ZFMISC_1: 31;
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A4: ((
gamma C)
. o)
=
ConceptStr (# O, A #) and
A5: O
= ((
AttributeDerivation C)
. ((
ObjectDerivation C)
.
{o})) and A
= ((
ObjectDerivation C)
.
{o}) by
Def4;
consider O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C such that
A6: ((
delta C)
. a)
=
ConceptStr (# O9, A9 #) and
A7: O9
= ((
AttributeDerivation C)
.
{a}) and A9
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
Def5;
A8: the
Extent of (((
delta C)
. a)
@ )
= O9 by
A6,
CONLAT_1:def 21;
the
Extent of (((
gamma C)
. o)
@ )
= O by
A4,
CONLAT_1:def 21;
then the
Extent of (((
gamma C)
. o)
@ )
c= the
Extent of (((
delta C)
. a)
@ ) by
A3,
A5,
A7,
A8,
CONLAT_1: 4;
then (((
gamma C)
. o)
@ )
is-SubConcept-of (((
delta C)
. a)
@ ) by
CONLAT_1:def 16;
hence ((
gamma C)
. o)
[= ((
delta C)
. a) by
CONLAT_1: 43;
end;
consider O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C such that
A9: ((
delta C)
. a)
=
ConceptStr (# O9, A9 #) and
A10: O9
= ((
AttributeDerivation C)
.
{a}) and A9
= ((
ObjectDerivation C)
. ((
AttributeDerivation C)
.
{a})) by
Def5;
assume ((
gamma C)
. o)
[= ((
delta C)
. a);
then (((
gamma C)
. o)
@ )
is-SubConcept-of (((
delta C)
. a)
@ ) by
CONLAT_1: 43;
then
A11: the
Extent of (((
gamma C)
. o)
@ )
c= the
Extent of (((
delta C)
. a)
@ ) by
CONLAT_1:def 16;
the
Extent of (((
delta C)
. a)
@ )
= O9 by
A9,
CONLAT_1:def 21;
then O
c= O9 by
A11,
A1,
CONLAT_1:def 21;
then aa
c= ((
ObjectDerivation C)
. oo) by
A2,
A10,
CONLAT_1: 11;
then
{a}
c= ((
ObjectDerivation C)
. o9) by
CONLAT_1: 7;
then a
in ((
ObjectDerivation C)
.
{o}) by
ZFMISC_1: 31;
then a
in { a9 where a9 be
Attribute of C : o
is-connected-with a9 } by
CONLAT_1: 1;
then ex b be
Attribute of C st b
= a & o
is-connected-with b;
hence thesis;
end;
begin
Lm1: for L1,L2 be
Lattice holds for f be
Function of the
carrier of L1, the
carrier of L2 holds (for a,b be
Element of L1 holds (f
. a)
[= (f
. b) implies a
[= b) implies f is
one-to-one
proof
let L1,L2 be
Lattice;
let f be
Function of the
carrier of L1, the
carrier of L2;
assume
A1: for a,b be
Element of L1 holds (f
. a)
[= (f
. b) implies a
[= b;
let x,y be
object;
assume that
A2: x
in (
dom f) and
A3: y
in (
dom f) and
A4: (f
. x)
= (f
. y);
reconsider y as
Element of L1 by
A3;
reconsider x as
Element of L1 by
A2;
x
[= y & y
[= x by
A1,
A4;
hence thesis by
LATTICES: 8;
end;
Lm2: for L1,L2 be
complete
Lattice holds for f be
Function of the
carrier of L1, the
carrier of L2 st f is
one-to-one & (
rng f)
= the
carrier of L2 holds (for a,b be
Element of L1 holds a
[= b iff (f
. a)
[= (f
. b)) implies f is
Homomorphism of L1, L2
proof
let L1,L2 be
complete
Lattice;
let f be
Function of the
carrier of L1, the
carrier of L2;
assume
A1: f is
one-to-one & (
rng f)
= the
carrier of L2;
assume
A2: for a,b be
Element of L1 holds a
[= b iff (f
. a)
[= (f
. b);
A3: for a,b be
Element of L1 holds (f
. (a
"/\" b))
= ((f
. a)
"/\" (f
. b))
proof
let a,b be
Element of L1;
(a
"/\" b)
[= b by
LATTICES: 6;
then
A4: (f
. (a
"/\" b))
[= (f
. b) by
A2;
A5: for r be
Element of L2 st r
is_less_than
{(f
. a), (f
. b)} holds r
[= (f
. (a
"/\" b))
proof
reconsider g = (f
" ) as
Function of the
carrier of L2, the
carrier of L1 by
A1,
FUNCT_2: 25;
let r be
Element of L2;
assume
A6: r
is_less_than
{(f
. a), (f
. b)};
A7: (f
. (g
. r))
= r by
A1,
FUNCT_1: 35;
(f
. b)
in
{(f
. a), (f
. b)} by
TARSKI:def 2;
then r
[= (f
. b) by
A6;
then
A8: (g
. r)
[= b by
A2,
A7;
(f
. a)
in
{(f
. a), (f
. b)} by
TARSKI:def 2;
then r
[= (f
. a) by
A6;
then (g
. r)
[= a by
A2,
A7;
then for q be
Element of L1 st q
in
{a, b} holds (g
. r)
[= q by
A8,
TARSKI:def 2;
then
A9: (g
. r)
is_less_than
{a, b};
(a
"/\" b)
= (
"/\"
{a, b}) by
LATTICE3: 43;
then (g
. r)
[= (a
"/\" b) by
A9,
LATTICE3: 34;
hence thesis by
A2,
A7;
end;
(a
"/\" b)
[= a by
LATTICES: 6;
then (f
. (a
"/\" b))
[= (f
. a) by
A2;
then for q be
Element of L2 st q
in
{(f
. a), (f
. b)} holds (f
. (a
"/\" b))
[= q by
A4,
TARSKI:def 2;
then (f
. (a
"/\" b))
is_less_than
{(f
. a), (f
. b)};
then (f
. (a
"/\" b))
= (
"/\" (
{(f
. a), (f
. b)},L2)) by
A5,
LATTICE3: 34;
hence thesis by
LATTICE3: 43;
end;
for a,b be
Element of L1 holds (f
. (a
"\/" b))
= ((f
. a)
"\/" (f
. b))
proof
let a,b be
Element of L1;
b
[= (a
"\/" b) by
LATTICES: 5;
then
A10: (f
. b)
[= (f
. (a
"\/" b)) by
A2;
A11: for r be
Element of L2 st
{(f
. a), (f
. b)}
is_less_than r holds (f
. (a
"\/" b))
[= r
proof
reconsider g = (f
" ) as
Function of the
carrier of L2, the
carrier of L1 by
A1,
FUNCT_2: 25;
let r be
Element of L2;
assume
A12:
{(f
. a), (f
. b)}
is_less_than r;
A13: (f
. (g
. r))
= r by
A1,
FUNCT_1: 35;
(f
. b)
in
{(f
. a), (f
. b)} by
TARSKI:def 2;
then (f
. b)
[= r by
A12;
then
A14: b
[= (g
. r) by
A2,
A13;
(f
. a)
in
{(f
. a), (f
. b)} by
TARSKI:def 2;
then (f
. a)
[= r by
A12;
then a
[= (g
. r) by
A2,
A13;
then for q be
Element of L1 st q
in
{a, b} holds q
[= (g
. r) by
A14,
TARSKI:def 2;
then
A15:
{a, b}
is_less_than (g
. r);
(a
"\/" b)
= (
"\/"
{a, b}) by
LATTICE3: 43;
then (a
"\/" b)
[= (g
. r) by
A15,
LATTICE3:def 21;
hence thesis by
A2,
A13;
end;
a
[= (a
"\/" b) by
LATTICES: 5;
then (f
. a)
[= (f
. (a
"\/" b)) by
A2;
then for q be
Element of L2 st q
in
{(f
. a), (f
. b)} holds q
[= (f
. (a
"\/" b)) by
A10,
TARSKI:def 2;
then
{(f
. a), (f
. b)}
is_less_than (f
. (a
"\/" b));
then (f
. (a
"\/" b))
= (
"\/" (
{(f
. a), (f
. b)},L2)) by
A11,
LATTICE3:def 21;
hence thesis by
LATTICE3: 43;
end;
then f is
"\/"-preserving
"/\"-preserving by
A3,
LATTICE4:def 1,
LATTICE4:def 2;
hence thesis;
end;
Lm3: for C be
FormalContext holds for CS be
ConceptStr over C st ((
ObjectDerivation C)
. the
Extent of CS)
= the
Intent of CS holds CS is non
empty
proof
let C be
FormalContext;
let CS be
ConceptStr over C;
assume
A1: ((
ObjectDerivation C)
. the
Extent of CS)
= the
Intent of CS;
per cases ;
suppose the
Extent of CS is
empty;
then the
Intent of CS
= the
carrier' of C by
A1,
CONLAT_1: 17;
hence thesis by
CONLAT_1:def 8;
end;
suppose the
Extent of CS is non
empty;
hence thesis by
CONLAT_1:def 8;
end;
end;
theorem ::
CONLAT_2:14
Th14: for L be
complete
Lattice holds for C be
FormalContext holds ((
ConceptLattice C),L)
are_isomorphic iff ex g be
Function of the
carrier of C, the
carrier of L, d be
Function of the
carrier' of C, the
carrier of L st (
rng g) is
supremum-dense & (
rng d) is
infimum-dense & for o be
Object of C, a be
Attribute of C holds o
is-connected-with a iff (g
. o)
[= (d
. a)
proof
let L be
complete
Lattice;
let C be
FormalContext;
hereby
assume ((
ConceptLattice C),L)
are_isomorphic ;
then
consider f be
Homomorphism of (
ConceptLattice C), L such that
A1: f is
bijective by
LATTICE4:def 3;
take g = (f
* (
gamma C)), d = (f
* (
delta C));
thus (
rng g) is
supremum-dense
proof
let a be
Element of L;
consider b be
Element of (
ConceptLattice C) such that
A2: a
= (f
. b) by
A1,
LATTICE4: 6;
(
rng (
gamma C)) is
supremum-dense by
Th12;
then
consider D9 be
Subset of (
rng (
gamma C)) such that
A3: b
= (
"\/" (D9,(
ConceptLattice C)));
set D = { (f
. x) where x be
Element of (
ConceptLattice C) : x
in D9 };
A4: for r be
Element of L st D
is_less_than r holds a
[= r
proof
let r be
Element of L;
consider r9 be
Element of (
ConceptLattice C) such that
A5: r
= (f
. r9) by
A1,
LATTICE4: 6;
reconsider r9 as
Element of (
ConceptLattice C);
assume
A6: D
is_less_than r;
for q be
Element of (
ConceptLattice C) st q
in D9 holds q
[= r9
proof
let q be
Element of (
ConceptLattice C);
assume q
in D9;
then (f
. q)
in { (f
. x) where x be
Element of (
ConceptLattice C) : x
in D9 };
then (f
. q)
[= (f
. r9) by
A6,
A5;
hence thesis by
A1,
LATTICE4: 5;
end;
then D9
is_less_than r9;
then b
[= r9 by
A3,
LATTICE3:def 21;
hence thesis by
A1,
A2,
A5,
LATTICE4: 5;
end;
A7: D
c= (
rng g)
proof
let x be
object;
assume x
in D;
then
consider x9 be
Element of (
ConceptLattice C) such that
A8: x
= (f
. x9) and
A9: x9
in D9;
consider y be
object such that
A10: y
in (
dom (
gamma C)) & ((
gamma C)
. y)
= x9 by
A9,
FUNCT_1:def 3;
(
dom f)
= the
carrier of (
ConceptLattice C) by
FUNCT_2:def 1;
then
A11: y
in (
dom (f
* (
gamma C))) by
A10,
FUNCT_1: 11;
x
= ((f
* (
gamma C))
. y) by
A8,
A10,
FUNCT_1: 13;
hence thesis by
A11,
FUNCT_1:def 3;
end;
A12: D9
is_less_than b by
A3,
LATTICE3:def 21;
D
is_less_than a
proof
let q be
Element of L;
assume q
in D;
then
consider q9 be
Element of (
ConceptLattice C) such that
A13: q
= (f
. q9) and
A14: q9
in D9;
q9
[= b by
A12,
A14;
hence thesis by
A1,
A2,
A13,
LATTICE4: 5;
end;
then a
= (
"\/" (D,L)) by
A4,
LATTICE3:def 21;
hence thesis by
A7;
end;
thus (
rng d) is
infimum-dense
proof
let a be
Element of L;
consider b be
Element of (
ConceptLattice C) such that
A15: a
= (f
. b) by
A1,
LATTICE4: 6;
(
rng (
delta C)) is
infimum-dense by
Th12;
then
consider D9 be
Subset of (
rng (
delta C)) such that
A16: b
= (
"/\" (D9,(
ConceptLattice C)));
set D = { (f
. x) where x be
Element of (
ConceptLattice C) : x
in D9 };
A17: for r be
Element of L st r
is_less_than D holds r
[= a
proof
let r be
Element of L;
consider r9 be
Element of (
ConceptLattice C) such that
A18: r
= (f
. r9) by
A1,
LATTICE4: 6;
reconsider r9 as
Element of (
ConceptLattice C);
assume
A19: r
is_less_than D;
r9
is_less_than D9
proof
let q be
Element of (
ConceptLattice C);
assume q
in D9;
then (f
. q)
in { (f
. x) where x be
Element of (
ConceptLattice C) : x
in D9 };
then (f
. r9)
[= (f
. q) by
A19,
A18;
hence thesis by
A1,
LATTICE4: 5;
end;
then r9
[= b by
A16,
LATTICE3: 34;
hence thesis by
A1,
A15,
A18,
LATTICE4: 5;
end;
A20: D
c= (
rng d)
proof
let x be
object;
assume x
in D;
then
consider x9 be
Element of (
ConceptLattice C) such that
A21: x
= (f
. x9) and
A22: x9
in D9;
consider y be
object such that
A23: y
in (
dom (
delta C)) & ((
delta C)
. y)
= x9 by
A22,
FUNCT_1:def 3;
(
dom f)
= the
carrier of (
ConceptLattice C) by
FUNCT_2:def 1;
then
A24: y
in (
dom (f
* (
delta C))) by
A23,
FUNCT_1: 11;
x
= ((f
* (
delta C))
. y) by
A21,
A23,
FUNCT_1: 13;
hence thesis by
A24,
FUNCT_1:def 3;
end;
A25: b
is_less_than D9 by
A16,
LATTICE3: 34;
a
is_less_than D
proof
let q be
Element of L;
assume q
in D;
then
consider q9 be
Element of (
ConceptLattice C) such that
A26: q
= (f
. q9) and
A27: q9
in D9;
b
[= q9 by
A25,
A27;
hence thesis by
A1,
A15,
A26,
LATTICE4: 5;
end;
then a
= (
"/\" (D,L)) by
A17,
LATTICE3: 34;
hence thesis by
A20;
end;
let o be
Object of C, a be
Attribute of C;
A28: o
is-connected-with a iff ((
gamma C)
. o)
[= ((
delta C)
. a) by
Th13;
hereby
(
dom (
delta C))
= the
carrier' of C by
FUNCT_2:def 1;
then
A29: (f
. ((
delta C)
. a))
= ((f
* (
delta C))
. a) by
FUNCT_1: 13;
(
dom (
gamma C))
= the
carrier of C by
FUNCT_2:def 1;
then
A30: (f
. ((
gamma C)
. o))
= ((f
* (
gamma C))
. o) by
FUNCT_1: 13;
assume o
is-connected-with a;
hence (g
. o)
[= (d
. a) by
A1,
A28,
A30,
A29,
LATTICE4: 5;
end;
(
dom (
gamma C))
= the
carrier of C by
FUNCT_2:def 1;
then
A31: (f
. ((
gamma C)
. o))
= ((f
* (
gamma C))
. o) by
FUNCT_1: 13;
(
dom (
delta C))
= the
carrier' of C by
FUNCT_2:def 1;
then
A32: (f
. ((
delta C)
. a))
= ((f
* (
delta C))
. a) by
FUNCT_1: 13;
assume (g
. o)
[= (d
. a);
then ((
gamma C)
. o)
[= ((
delta C)
. a) by
A1,
A31,
A32,
LATTICE4: 5;
hence o
is-connected-with a by
Th13;
end;
given g be
Function of the
carrier of C, the
carrier of L, d be
Function of the
carrier' of C, the
carrier of L such that
A33: (
rng g) is
supremum-dense and
A34: (
rng d) is
infimum-dense and
A35: for o be
Object of C, a be
Attribute of C holds o
is-connected-with a iff (g
. o)
[= (d
. a);
set fi = {
[x,
ConceptStr (# O, A #)] where x be
Element of L, O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C : O
= { o where o be
Object of C : (g
. o)
[= x } & A
= { a where a be
Attribute of C : x
[= (d
. a) } };
set f = {
[
ConceptStr (# O, A #), x] where O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C, x be
Element of L :
ConceptStr (# O, A #) is
FormalConcept of C & x
= (
"\/" ({ (g
. o) where o be
Object of C : o
in O },L)) };
A36: (
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
A37: f
c=
[:the
carrier of (
ConceptLattice C), the
carrier of L:]
proof
let y be
object;
assume y
in f;
then
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C, x be
Element of L such that
A38: y
=
[
ConceptStr (# O, A #), x] and
A39:
ConceptStr (# O, A #) is
FormalConcept of C and x
= (
"\/" ({ (g
. o) where o be
Object of C : o
in O },L));
ConceptStr (# O, A #)
in the
carrier of (
ConceptLattice C) by
A36,
A39,
CONLAT_1: 31;
hence thesis by
A38,
ZFMISC_1:def 2;
end;
fi
c=
[:the
carrier of L, the
carrier of (
ConceptLattice C):]
proof
let y be
object;
assume y
in fi;
then
consider x be
Element of L, O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A40: y
=
[x,
ConceptStr (# O, A #)] and
A41: O
= { o where o be
Object of C : (g
. o)
[= x } and
A42: A
= { a where a be
Attribute of C : x
[= (d
. a) };
A43: ((
AttributeDerivation C)
. the
Intent of
ConceptStr (# O, A #))
= the
Extent of
ConceptStr (# O, A #)
proof
thus ((
AttributeDerivation C)
. the
Intent of
ConceptStr (# O, A #))
c= the
Extent of
ConceptStr (# O, A #)
proof
let u be
object;
A44: (
"/\" ({ (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) },L))
= x
proof
consider D be
Subset of (
rng d) such that
A45: (
"/\" (D,L))
= x by
A34;
A46: x
is_less_than D by
A45,
LATTICE3: 34;
D
c= { (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) }
proof
let u be
object;
assume
A47: u
in D;
then
consider v be
object such that
A48: v
in (
dom d) and
A49: u
= (d
. v) by
FUNCT_1:def 3;
reconsider v as
Attribute of C by
A48;
x
[= (d
. v) by
A46,
A47,
A49;
hence thesis by
A49;
end;
then
A50: (
"/\" ({ (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) },L))
[= x by
A45,
LATTICE3: 45;
x
is_less_than { (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) }
proof
let u be
Element of L;
assume u
in { (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) };
then ex v be
Attribute of C st u
= (d
. v) & x
[= (d
. v);
hence thesis;
end;
then x
[= (
"/\" ({ (d
. a9) where a9 be
Attribute of C : x
[= (d
. a9) },L)) by
LATTICE3: 39;
hence thesis by
A50,
LATTICES: 8;
end;
assume u
in ((
AttributeDerivation C)
. the
Intent of
ConceptStr (# O, A #));
then u
in { o where o be
Object of C : for a be
Attribute of C st a
in the
Intent of
ConceptStr (# O, A #) holds o
is-connected-with a } by
CONLAT_1:def 4;
then
consider u9 be
Object of C such that
A51: u9
= u and
A52: for a be
Attribute of C st a
in the
Intent of
ConceptStr (# O, A #) holds u9
is-connected-with a;
A53: for v be
Attribute of C st v
in { a where a be
Attribute of C : x
[= (d
. a) } holds (g
. u9)
[= (d
. v) by
A35,
A42,
A52;
(g
. u9)
is_less_than { (d
. a) where a be
Attribute of C : x
[= (d
. a) }
proof
let q be
Element of L;
assume q
in { (d
. a) where a be
Attribute of C : x
[= (d
. a) };
then
consider b be
Attribute of C such that
A54: q
= (d
. b) and
A55: x
[= (d
. b);
b
in { a where a be
Attribute of C : x
[= (d
. a) } by
A55;
hence thesis by
A53,
A54;
end;
then (g
. u9)
[= x by
A44,
LATTICE3: 34;
hence thesis by
A41,
A51;
end;
let u be
object;
assume u
in the
Extent of
ConceptStr (# O, A #);
then
consider u9 be
Object of C such that
A56: u9
= u and
A57: (g
. u9)
[= x by
A41;
A58: for v be
Attribute of C st v
in { a where a be
Attribute of C : x
[= (d
. a) } holds (g
. u9)
[= (d
. v)
proof
let v be
Attribute of C;
assume v
in { a where a be
Attribute of C : x
[= (d
. a) };
then ex v9 be
Attribute of C st v9
= v & x
[= (d
. v9);
hence thesis by
A57,
LATTICES: 7;
end;
for v be
Attribute of C st v
in { a where a be
Attribute of C : x
[= (d
. a) } holds u9
is-connected-with v
proof
let v be
Attribute of C;
assume v
in { a where a be
Attribute of C : x
[= (d
. a) };
then (g
. u9)
[= (d
. v) by
A58;
hence thesis by
A35;
end;
then u9
in { o where o be
Object of C : for a be
Attribute of C st a
in the
Intent of
ConceptStr (# O, A #) holds o
is-connected-with a } by
A42;
hence thesis by
A56,
CONLAT_1:def 4;
end;
((
ObjectDerivation C)
. the
Extent of
ConceptStr (# O, A #))
= the
Intent of
ConceptStr (# O, A #)
proof
thus ((
ObjectDerivation C)
. the
Extent of
ConceptStr (# O, A #))
c= the
Intent of
ConceptStr (# O, A #)
proof
let u be
object;
A59: (
"\/" ({ (g
. a9) where a9 be
Object of C : (g
. a9)
[= x },L))
= x
proof
consider D be
Subset of (
rng g) such that
A60: (
"\/" (D,L))
= x by
A33;
A61: D
is_less_than x by
A60,
LATTICE3:def 21;
D
c= { (g
. a9) where a9 be
Object of C : (g
. a9)
[= x }
proof
let u be
object;
assume
A62: u
in D;
then
consider v be
object such that
A63: v
in (
dom g) and
A64: u
= (g
. v) by
FUNCT_1:def 3;
reconsider v as
Object of C by
A63;
(g
. v)
[= x by
A61,
A62,
A64;
hence thesis by
A64;
end;
then
A65: x
[= (
"\/" ({ (g
. a9) where a9 be
Object of C : (g
. a9)
[= x },L)) by
A60,
LATTICE3: 45;
{ (g
. a9) where a9 be
Object of C : (g
. a9)
[= x }
is_less_than x
proof
let u be
Element of L;
assume u
in { (g
. a9) where a9 be
Object of C : (g
. a9)
[= x };
then ex v be
Object of C st u
= (g
. v) & (g
. v)
[= x;
hence thesis;
end;
then (
"\/" ({ (g
. a9) where a9 be
Object of C : (g
. a9)
[= x },L))
[= x by
LATTICE3:def 21;
hence thesis by
A65,
LATTICES: 8;
end;
assume u
in ((
ObjectDerivation C)
. the
Extent of
ConceptStr (# O, A #));
then u
in { o where o be
Attribute of C : for a be
Object of C st a
in the
Extent of
ConceptStr (# O, A #) holds a
is-connected-with o } by
CONLAT_1:def 3;
then
consider u9 be
Attribute of C such that
A66: u9
= u and
A67: for a be
Object of C st a
in the
Extent of
ConceptStr (# O, A #) holds a
is-connected-with u9;
A68: for v be
Object of C st v
in { a where a be
Object of C : (g
. a)
[= x } holds (g
. v)
[= (d
. u9) by
A35,
A41,
A67;
{ (g
. a) where a be
Object of C : (g
. a)
[= x }
is_less_than (d
. u9)
proof
let q be
Element of L;
assume q
in { (g
. a) where a be
Object of C : (g
. a)
[= x };
then
consider b be
Object of C such that
A69: q
= (g
. b) and
A70: (g
. b)
[= x;
b
in { a where a be
Object of C : (g
. a)
[= x } by
A70;
hence thesis by
A68,
A69;
end;
then x
[= (d
. u9) by
A59,
LATTICE3:def 21;
hence thesis by
A42,
A66;
end;
let u be
object;
assume u
in the
Intent of
ConceptStr (# O, A #);
then
consider u9 be
Attribute of C such that
A71: u9
= u and
A72: x
[= (d
. u9) by
A42;
A73: for v be
Object of C st v
in { a where a be
Object of C : (g
. a)
[= x } holds (g
. v)
[= (d
. u9)
proof
let v be
Object of C;
assume v
in { a where a be
Object of C : (g
. a)
[= x };
then ex v9 be
Object of C st v9
= v & (g
. v9)
[= x;
hence thesis by
A72,
LATTICES: 7;
end;
for v be
Object of C st v
in { a where a be
Object of C : (g
. a)
[= x } holds v
is-connected-with u9
proof
let v be
Object of C;
assume v
in { a where a be
Object of C : (g
. a)
[= x };
then (g
. v)
[= (d
. u9) by
A73;
hence thesis by
A35;
end;
then u9
in { o where o be
Attribute of C : for a be
Object of C st a
in the
Extent of
ConceptStr (# O, A #) holds a
is-connected-with o } by
A41;
hence thesis by
A71,
CONLAT_1:def 3;
end;
then
ConceptStr (# O, A #) is
FormalConcept of C by
A43,
Lm3,
CONLAT_1:def 10;
then
ConceptStr (# O, A #)
in the
carrier of (
ConceptLattice C) by
A36,
CONLAT_1: 31;
hence thesis by
A40,
ZFMISC_1:def 2;
end;
then
reconsider fi as
Relation of the
carrier of L, the
carrier of (
ConceptLattice C);
A74: for x,y1,y2 be
object st
[x, y1]
in fi &
[x, y2]
in fi holds y1
= y2
proof
let x,y1,y2 be
object;
assume that
A75:
[x, y1]
in fi and
A76:
[x, y2]
in fi;
consider z be
Element of L, O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C such that
A77:
[x, y1]
=
[z,
ConceptStr (# O, A #)] and
A78: O
= { o where o be
Object of C : (g
. o)
[= z } & A
= { a where a be
Attribute of C : z
[= (d
. a) } by
A75;
consider z9 be
Element of L, O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C such that
A79:
[x, y2]
=
[z9,
ConceptStr (# O9, A9 #)] and
A80: O9
= { o where o be
Object of C : (g
. o)
[= z9 } & A9
= { a where a be
Attribute of C : z9
[= (d
. a) } by
A76;
A81: z
= x by
A77,
XTUPLE_0: 1
.= z9 by
A79,
XTUPLE_0: 1;
thus y1
= (
[x, y1]
`2 )
.= (
[x, y2]
`2 ) by
A77,
A78,
A79,
A80,
A81
.= y2;
end;
the
carrier of L
c= (
dom fi)
proof
let y be
object;
assume y
in the
carrier of L;
then
reconsider y as
Element of L;
set A = { a where a be
Attribute of C : y
[= (d
. a) };
A
c= the
carrier' of C
proof
let u be
object;
assume u
in A;
then ex u9 be
Attribute of C st u9
= u & y
[= (d
. u9);
hence thesis;
end;
then
reconsider A as
Subset of the
carrier' of C;
set O = { o where o be
Object of C : (g
. o)
[= y };
O
c= the
carrier of C
proof
let u be
object;
assume u
in O;
then ex u9 be
Object of C st u9
= u & (g
. u9)
[= y;
hence thesis;
end;
then
reconsider O as
Subset of the
carrier of C;
[y,
ConceptStr (# O, A #)]
in fi;
hence thesis by
XTUPLE_0:def 12;
end;
then
A82: the
carrier of L
= (
dom fi);
reconsider f as
Relation of the
carrier of (
ConceptLattice C), the
carrier of L by
A37;
the
carrier of (
ConceptLattice C)
c= (
dom f)
proof
let y be
object;
assume y
in the
carrier of (
ConceptLattice C);
then
A83: y is
strict
FormalConcept of C by
A36,
CONLAT_1: 31;
then
consider O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C such that
A84: y
=
ConceptStr (# O9, A9 #);
reconsider z = (
"\/" ({ (g
. o) where o be
Object of C : o
in O9 },L)) as
Element of L;
[y, z]
in f by
A83,
A84;
hence thesis by
XTUPLE_0:def 12;
end;
then
A85: the
carrier of (
ConceptLattice C)
= (
dom f);
reconsider fi as
Function of the
carrier of L, the
carrier of (
ConceptLattice C) by
A82,
A74,
FUNCT_1:def 1,
FUNCT_2:def 1;
for x,y1,y2 be
object st
[x, y1]
in f &
[x, y2]
in f holds y1
= y2
proof
let x,y1,y2 be
object;
assume that
A86:
[x, y1]
in f and
A87:
[x, y2]
in f;
consider O be
Subset of the
carrier of C, A be
Subset of the
carrier' of C, z be
Element of L such that
A88:
[x, y1]
=
[
ConceptStr (# O, A #), z] and
ConceptStr (# O, A #) is
FormalConcept of C and
A89: z
= (
"\/" ({ (g
. o) where o be
Object of C : o
in O },L)) by
A86;
consider O9 be
Subset of the
carrier of C, A9 be
Subset of the
carrier' of C, z9 be
Element of L such that
A90:
[x, y2]
=
[
ConceptStr (# O9, A9 #), z9] and
ConceptStr (# O9, A9 #) is
FormalConcept of C and
A91: z9
= (
"\/" ({ (g
. o) where o be
Object of C : o
in O9 },L)) by
A87;
A92:
ConceptStr (# O, A #)
= (
[
ConceptStr (# O, A #), z]
`1 )
.= (
[x, y1]
`1 ) by
A88
.= x
.= (
[x, y2]
`1 )
.= (
[
ConceptStr (# O9, A9 #), z9]
`1 ) by
A90
.=
ConceptStr (# O9, A9 #);
thus y1
= (
[x, y1]
`2 )
.= (
[x, y2]
`2 ) by
A88,
A89,
A90,
A91,
A92
.= y2;
end;
then
reconsider f as
Function of the
carrier of (
ConceptLattice C), the
carrier of L by
A85,
FUNCT_1:def 1,
FUNCT_2:def 1;
A93: (
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
A94: for a be
Element of L holds (f
. (fi
. a))
= a
proof
let a be
Element of L;
reconsider a as
Element of L;
set A = { a9 where a9 be
Attribute of C : a
[= (d
. a9) };
A
c= the
carrier' of C
proof
let u be
object;
assume u
in A;
then ex u9 be
Attribute of C st u9
= u & a
[= (d
. u9);
hence thesis;
end;
then
reconsider A as
Subset of the
carrier' of C;
set O = { o where o be
Object of C : (g
. o)
[= a };
O
c= the
carrier of C
proof
let u be
object;
assume u
in O;
then ex u9 be
Object of C st u9
= u & (g
. u9)
[= a;
hence thesis;
end;
then
reconsider O as
Subset of the
carrier of C;
set b = (
"\/" ({ (g
. o) where o be
Object of C : o
in the
Extent of
ConceptStr (# O, A #) },L));
A95: (
"\/" ({ (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } },L))
= a
proof
consider D be
Subset of (
rng g) such that
A96: (
"\/" (D,L))
= a by
A33;
A97: D
is_less_than a by
A96,
LATTICE3:def 21;
D
c= { (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } }
proof
let u be
object;
assume
A98: u
in D;
then
consider v be
object such that
A99: v
in (
dom g) and
A100: u
= (g
. v) by
FUNCT_1:def 3;
reconsider v as
Object of C by
A99;
(g
. v)
[= a by
A97,
A98,
A100;
then v
in { o9 where o9 be
Object of C : (g
. o9)
[= a };
hence thesis by
A100;
end;
then
A101: a
[= (
"\/" ({ (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } },L)) by
A96,
LATTICE3: 45;
{ (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } }
is_less_than a
proof
let u be
Element of L;
assume u
in { (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } };
then
consider v be
Object of C such that
A102: u
= (g
. v) and
A103: v
in { o9 where o9 be
Object of C : (g
. o9)
[= a };
ex ov be
Object of C st ov
= v & (g
. ov)
[= a by
A103;
hence thesis by
A102;
end;
then (
"\/" ({ (g
. o) where o be
Object of C : o
in { o9 where o9 be
Object of C : (g
. o9)
[= a } },L))
[= a by
LATTICE3:def 21;
hence thesis by
A101,
LATTICES: 8;
end;
A104:
[a,
ConceptStr (# O, A #)]
in fi;
then
ConceptStr (# O, A #)
in (
rng fi) by
XTUPLE_0:def 13;
then
ConceptStr (# O, A #) is
FormalConcept of C by
A93,
CONLAT_1: 31;
then
[
ConceptStr (# O, A #), b]
in f;
then (f
.
ConceptStr (# O, A #))
= b by
FUNCT_1: 1;
hence thesis by
A104,
A95,
FUNCT_1: 1;
end;
the
carrier of L
c= (
rng f)
proof
let u be
object;
A105: (
dom f)
= the
carrier of (
ConceptLattice C) by
FUNCT_2:def 1;
assume
A106: u
in the
carrier of L;
then u
in (
dom fi) by
FUNCT_2:def 1;
then
consider v be
object such that
A107:
[u, v]
in fi by
XTUPLE_0:def 12;
reconsider u as
Element of L by
A106;
v
in (
rng fi) by
A107,
XTUPLE_0:def 13;
then
reconsider v as
Element of (
ConceptLattice C);
(f
. v)
= (f
. (fi
. u)) by
A107,
FUNCT_1: 1
.= u by
A94;
hence thesis by
A105,
FUNCT_1:def 3;
end;
then
A108: (
rng f)
= the
carrier of L;
A109: for x be
Element of (
ConceptLattice C) holds (f
. x)
= (
"/\" ({ (d
. a) where a be
Attribute of C : a
in the
Intent of (x
@ ) },L))
proof
let x be
Element of (
ConceptLattice C);
set y = (
"\/" ({ (g
. o) where o be
Object of C : o
in the
Extent of (x
@ ) },L));
A110:
[(x
@ ), y]
in f;
A111: for o be
object holds o
in { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) } implies o
in { (d
. a) where a be
Attribute of C : a
in the
Intent of (x
@ ) }
proof
let o be
object;
assume o
in { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) };
then
consider u be
Attribute of C such that
A112: o
= (d
. u) and
A113: y
[= (d
. u);
A114: for o be
Object of C st o
in the
Extent of (x
@ ) holds (g
. o)
[= (d
. u)
proof
let o be
Object of C;
assume o
in the
Extent of (x
@ );
then (g
. o)
in { (g
. o9) where o9 be
Object of C : o9
in the
Extent of (x
@ ) };
then (g
. o)
[= y by
LATTICE3: 38;
hence thesis by
A113,
LATTICES: 7;
end;
for o be
Object of C st o
in the
Extent of (x
@ ) holds o
is-connected-with u
proof
let o be
Object of C;
assume o
in the
Extent of (x
@ );
then (g
. o)
[= (d
. u) by
A114;
hence thesis by
A35;
end;
then u
in { a9 where a9 be
Attribute of C : for o9 be
Object of C st o9
in the
Extent of (x
@ ) holds o9
is-connected-with a9 };
then u
in ((
ObjectDerivation C)
. the
Extent of (x
@ )) by
CONLAT_1:def 3;
then u
in the
Intent of (x
@ ) by
CONLAT_1:def 10;
hence thesis by
A112;
end;
A115: for o9 be
Object of C st o9
in the
Extent of (x
@ ) holds for a9 be
Attribute of C st a9
in the
Intent of (x
@ ) holds (g
. o9)
[= (d
. a9)
proof
let o9 be
Object of C;
assume
A116: o9
in the
Extent of (x
@ );
let a9 be
Attribute of C;
assume a9
in the
Intent of (x
@ );
then a9
in ((
ObjectDerivation C)
. the
Extent of (x
@ )) by
CONLAT_1:def 10;
then a9
in { a where a be
Attribute of C : for o be
Object of C st o
in the
Extent of (x
@ ) holds o
is-connected-with a } by
CONLAT_1:def 3;
then ex aa be
Attribute of C st aa
= a9 & for o be
Object of C st o
in the
Extent of (x
@ ) holds o
is-connected-with aa;
then o9
is-connected-with a9 by
A116;
hence thesis by
A35;
end;
A117: for o be
object holds o
in { (d
. a) where a be
Attribute of C : a
in the
Intent of (x
@ ) } implies o
in { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) }
proof
let o be
object;
assume o
in { (d
. a) where a be
Attribute of C : a
in the
Intent of (x
@ ) };
then
consider b be
Attribute of C such that
A118: o
= (d
. b) and
A119: b
in the
Intent of (x
@ );
{ (g
. o9) where o9 be
Object of C : o9
in the
Extent of (x
@ ) }
is_less_than (d
. b)
proof
let q be
Element of L;
assume q
in { (g
. o9) where o9 be
Object of C : o9
in the
Extent of (x
@ ) };
then ex u be
Object of C st q
= (g
. u) & u
in the
Extent of (x
@ );
hence thesis by
A115,
A119;
end;
then y
[= (d
. b) by
LATTICE3:def 21;
hence thesis by
A118;
end;
A120: (
"/\" ({ (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) },L))
= y
proof
consider D be
Subset of (
rng d) such that
A121: (
"/\" (D,L))
= y by
A34;
A122: y
is_less_than D by
A121,
LATTICE3: 34;
D
c= { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) }
proof
let u be
object;
assume
A123: u
in D;
then
consider v be
object such that
A124: v
in (
dom d) and
A125: u
= (d
. v) by
FUNCT_1:def 3;
reconsider v as
Attribute of C by
A124;
y
[= (d
. v) by
A122,
A123,
A125;
hence thesis by
A125;
end;
then
A126: (
"/\" ({ (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) },L))
[= y by
A121,
LATTICE3: 45;
y
is_less_than { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) }
proof
let u be
Element of L;
assume u
in { (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) };
then ex v be
Attribute of C st u
= (d
. v) & y
[= (d
. v);
hence thesis;
end;
then y
[= (
"/\" ({ (d
. a9) where a9 be
Attribute of C : y
[= (d
. a9) },L)) by
LATTICE3: 39;
hence thesis by
A126,
LATTICES: 8;
end;
(f
. x)
= (f
. (x
@ )) by
CONLAT_1:def 21
.= y by
A110,
FUNCT_1: 1;
hence thesis by
A111,
A117,
A120,
TARSKI: 2;
end;
A127: for a be
Element of (
ConceptLattice C) holds (fi
. (f
. a))
= a
proof
let a be
Element of (
ConceptLattice C);
set x = (
"/\" ({ (d
. u) where u be
Attribute of C : u
in the
Intent of (a
@ ) },L));
set A = { a9 where a9 be
Attribute of C : x
[= (d
. a9) };
A
c= the
carrier' of C
proof
let u be
object;
assume u
in A;
then ex u9 be
Attribute of C st u9
= u & x
[= (d
. u9);
hence thesis;
end;
then
reconsider A as
Subset of the
carrier' of C;
set O = { o where o be
Object of C : (g
. o)
[= x };
O
c= the
carrier of C
proof
let u be
object;
assume u
in O;
then ex u9 be
Object of C st u9
= u & (g
. u9)
[= x;
hence thesis;
end;
then
reconsider O as
Subset of the
carrier of C;
A128: O
= { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) }
proof
thus O
c= { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) }
proof
let u be
object;
assume u
in O;
then
consider o9 be
Object of C such that
A129: u
= o9 and
A130: (g
. o9)
[= x;
for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o9)
[= (d
. a9)
proof
let a9 be
Attribute of C;
assume a9
in the
Intent of (a
@ );
then (d
. a9)
in { (d
. y) where y be
Attribute of C : y
in the
Intent of (a
@ ) };
then x
[= (d
. a9) by
LATTICE3: 38;
hence thesis by
A130,
LATTICES: 7;
end;
hence thesis by
A129;
end;
let u be
object;
assume u
in { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) };
then
consider o9 be
Object of C such that
A131: o9
= u and
A132: for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o9)
[= (d
. a9);
(g
. o9)
is_less_than { (d
. y) where y be
Attribute of C : y
in the
Intent of (a
@ ) }
proof
let q be
Element of L;
assume q
in { (d
. y) where y be
Attribute of C : y
in the
Intent of (a
@ ) };
then ex qa be
Attribute of C st q
= (d
. qa) & qa
in the
Intent of (a
@ );
hence thesis by
A132;
end;
then (g
. o9)
[= x by
LATTICE3: 34;
hence thesis by
A131;
end;
{ o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) }
= { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds o
is-connected-with a9 }
proof
thus { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) }
c= { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds o
is-connected-with a9 }
proof
let u be
object;
assume u
in { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. o)
[= (d
. a9) };
then
consider u9 be
Object of C such that
A133: u
= u9 and
A134: for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. u9)
[= (d
. a9);
for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds u9
is-connected-with a9
proof
let a9 be
Attribute of C;
assume a9
in the
Intent of (a
@ );
then (g
. u9)
[= (d
. a9) by
A134;
hence thesis by
A35;
end;
hence thesis by
A133;
end;
let u be
object;
assume u
in { o where o be
Object of C : for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds o
is-connected-with a9 };
then
consider u9 be
Object of C such that
A135: u
= u9 and
A136: for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds u9
is-connected-with a9;
for a9 be
Attribute of C st a9
in the
Intent of (a
@ ) holds (g
. u9)
[= (d
. a9) by
A35,
A136;
hence thesis by
A135;
end;
then
A137: O
= ((
AttributeDerivation C)
. the
Intent of (a
@ )) by
A128,
CONLAT_1:def 4
.= the
Extent of (a
@ ) by
CONLAT_1:def 10;
A138: (fi
. (
"/\" ({ (d
. u) where u be
Attribute of C : u
in the
Intent of (a
@ ) },L)))
= (fi
. (f
. a)) by
A109;
[x,
ConceptStr (# O, A #)]
in fi;
then
A139: (fi
. x)
=
ConceptStr (# O, A #) by
FUNCT_1: 1;
then
ConceptStr (# O, A #) is
FormalConcept of C by
A93,
CONLAT_1: 31;
then A
= ((
ObjectDerivation C)
. the
Extent of (a
@ )) by
A137,
CONLAT_1:def 10
.= the
Intent of (a
@ ) by
CONLAT_1:def 10;
hence thesis by
A138,
A139,
A137,
CONLAT_1:def 21;
end;
A140: for a,b be
Element of L holds a
[= b implies (fi
. a)
[= (fi
. b)
proof
let a,b be
Element of L;
set ca = (fi
. a), cb = (fi
. b);
assume
A141: a
[= b;
A142: { o where o be
Object of C : (g
. o)
[= a }
c= { o where o be
Object of C : (g
. o)
[= b }
proof
let x be
object;
assume x
in { o where o be
Object of C : (g
. o)
[= a };
then
consider x9 be
Object of C such that
A143: x9
= x and
A144: (g
. x9)
[= a;
(g
. x9)
[= b by
A141,
A144,
LATTICES: 7;
hence thesis by
A143;
end;
A145: (
dom fi)
= the
carrier of L by
FUNCT_2:def 1;
then
consider ya be
object such that
A146:
[a, ya]
in fi by
XTUPLE_0:def 12;
consider yb be
object such that
A147:
[b, yb]
in fi by
A145,
XTUPLE_0:def 12;
consider xb be
Element of L, Ob be
Subset of the
carrier of C, Ab be
Subset of the
carrier' of C such that
A148:
[b, yb]
=
[xb,
ConceptStr (# Ob, Ab #)] and
A149: Ob
= { o where o be
Object of C : (g
. o)
[= xb } and Ab
= { a9 where a9 be
Attribute of C : xb
[= (d
. a9) } by
A147;
A150: b
= (
[b, yb]
`1 )
.= (
[xb,
ConceptStr (# Ob, Ab #)]
`1 ) by
A148
.= xb;
then (fi
. b)
=
ConceptStr (# Ob, Ab #) by
A147,
A148,
FUNCT_1: 1;
then
A151: the
Extent of (cb
@ )
= Ob by
CONLAT_1:def 21;
consider xa be
Element of L, Oa be
Subset of the
carrier of C, Aa be
Subset of the
carrier' of C such that
A152:
[a, ya]
=
[xa,
ConceptStr (# Oa, Aa #)] and
A153: Oa
= { o where o be
Object of C : (g
. o)
[= xa } and Aa
= { a9 where a9 be
Attribute of C : xa
[= (d
. a9) } by
A146;
A154: a
= (
[a, ya]
`1 )
.= (
[xa,
ConceptStr (# Oa, Aa #)]
`1 ) by
A152
.= xa;
then (fi
. a)
=
ConceptStr (# Oa, Aa #) by
A146,
A152,
FUNCT_1: 1;
then the
Extent of (ca
@ )
= Oa by
CONLAT_1:def 21;
then (ca
@ )
is-SubConcept-of (cb
@ ) by
A142,
A153,
A149,
A154,
A150,
A151,
CONLAT_1:def 16;
hence thesis by
CONLAT_1: 43;
end;
A155: for a,b be
Element of (
ConceptLattice C) holds (f
. a)
[= (f
. b) implies a
[= b
proof
let a,b be
Element of (
ConceptLattice C);
assume
A156: (f
. a)
[= (f
. b);
(fi
. (f
. a))
= a & (fi
. (f
. b))
= b by
A127;
hence thesis by
A140,
A156;
end;
for a,b be
Element of (
ConceptLattice C) holds a
[= b implies (f
. a)
[= (f
. b)
proof
let a,b be
Element of (
ConceptLattice C);
reconsider xa = (
"\/" ({ (g
. o) where o be
Object of C : o
in the
Extent of (a
@ ) },L)), xb = (
"\/" ({ (g
. o) where o be
Object of C : o
in the
Extent of (b
@ ) },L)) as
Element of L;
[(a
@ ), xa]
in f;
then
A157: (f
. (a
@ ))
= xa by
FUNCT_1: 1;
[(b
@ ), xb]
in f;
then
A158: (f
. (b
@ ))
= xb by
FUNCT_1: 1;
assume a
[= b;
then (a
@ )
is-SubConcept-of (b
@ ) by
CONLAT_1: 43;
then
A159: the
Extent of (a
@ )
c= the
Extent of (b
@ ) by
CONLAT_1:def 16;
A160: { (g
. o) where o be
Object of C : o
in the
Extent of (a
@ ) }
c= { (g
. o) where o be
Object of C : o
in the
Extent of (b
@ ) }
proof
let x be
object;
assume x
in { (g
. o) where o be
Object of C : o
in the
Extent of (a
@ ) };
then ex o be
Object of C st x
= (g
. o) & o
in the
Extent of (a
@ );
hence thesis by
A159;
end;
(a
@ )
= a & (b
@ )
= b by
CONLAT_1:def 21;
hence thesis by
A160,
A157,
A158,
LATTICE3: 45;
end;
then
reconsider f as
Homomorphism of (
ConceptLattice C), L by
A155,
A108,
Lm1,
Lm2;
A161: f is
onto by
A108,
FUNCT_2:def 3;
f is
one-to-one by
A155,
Lm1;
hence thesis by
A161,
LATTICE4:def 3;
end;
definition
let L be
Lattice;
::
CONLAT_2:def6
func
Context (L) ->
strict non
empty non
void
ContextStr equals
ContextStr (# the
carrier of L, the
carrier of L, (
LattRel L) #);
coherence ;
end
theorem ::
CONLAT_2:15
Th15: for L be
complete
Lattice holds ((
ConceptLattice (
Context L)),L)
are_isomorphic
proof
let L be
complete
Lattice;
reconsider g = (
id the
carrier of L) as
Function of the
carrier of (
Context L), the
carrier of L;
reconsider d = (
id the
carrier of L) as
Function of the
carrier' of (
Context L), the
carrier of L;
A1: for o be
Object of (
Context L), a be
Attribute of (
Context L) holds o
is-connected-with a iff (g
. o)
[= (d
. a)
proof
let o be
Object of (
Context L), a be
Attribute of (
Context L);
reconsider o9 = o, a9 = a as
Element of L;
o
is-connected-with a iff
[o, a]
in the
Information of (
Context L) by
CONLAT_1:def 2;
hence thesis by
FILTER_1: 31;
end;
for a be
Element of L holds ex D9 be
Subset of (
rng d) st a
= (
"/\" (D9,L))
proof
let a be
Element of L;
(
"/\" (
{a},L))
= a & (
rng d)
= the
carrier of L by
LATTICE3: 42,
RELAT_1: 45;
hence thesis;
end;
then
A2: (
rng d) is
infimum-dense;
(
rng g) is
supremum-dense
proof
let a be
Element of L;
(
"\/" (
{a},L))
= a & (
rng g)
= the
carrier of L by
LATTICE3: 42,
RELAT_1: 45;
hence thesis;
end;
hence thesis by
A2,
A1,
Th14;
end;
theorem ::
CONLAT_2:16
for L be
Lattice holds L is
complete iff ex C be
FormalContext st ((
ConceptLattice C),L)
are_isomorphic
proof
let L be
Lattice;
hereby
assume L is
complete;
then ((
ConceptLattice (
Context L)),L)
are_isomorphic by
Th15;
hence ex C be
FormalContext st ((
ConceptLattice C),L)
are_isomorphic ;
end;
given C be
FormalContext such that
A1: ((
ConceptLattice C),L)
are_isomorphic ;
let X be
Subset of L;
consider f be
Homomorphism of L, (
ConceptLattice C) such that
A2: f is
bijective by
A1,
LATTICE4:def 3;
set FX = { (f
. x) where x be
Element of L : x
in X };
FX
c= the
carrier of (
ConceptLattice C)
proof
let x be
object;
assume x
in FX;
then ex y be
Element of L st x
= (f
. y) & y
in X;
hence thesis;
end;
then
reconsider FX as
Subset of (
ConceptLattice C);
set Fa = (
"/\" (FX,(
ConceptLattice C)));
consider a be
Element of L such that
A3: Fa
= (f
. a) by
A2,
LATTICE4: 6;
A4: for b be
Element of L st b
is_less_than X holds b
[= a
proof
let b be
Element of L;
assume
A5: b
is_less_than X;
(f
. b)
is_less_than FX
proof
let q be
Element of (
ConceptLattice C);
assume q
in FX;
then
consider y be
Element of L such that
A6: q
= (f
. y) and
A7: y
in X;
b
[= y by
A5,
A7;
hence thesis by
A2,
A6,
LATTICE4: 5;
end;
then (f
. b)
[= (f
. a) by
A3,
LATTICE3: 34;
hence thesis by
A2,
LATTICE4: 5;
end;
A8: Fa
is_less_than FX by
LATTICE3: 34;
a
is_less_than X
proof
let q be
Element of L;
assume q
in X;
then (f
. q)
in FX;
then Fa
[= (f
. q) by
A8;
hence thesis by
A2,
A3,
LATTICE4: 5;
end;
hence thesis by
A4;
end;
begin
registration
let L be
complete
Lattice;
cluster (L
.: ) ->
complete;
coherence
proof
let X be
Subset of (L
.: );
A1: (L
.: )
=
LattStr (# the
carrier of L, the
L_meet of L, the
L_join of L #) by
LATTICE2:def 2;
then
reconsider X9 = X as
Subset of L;
set a9 = (
"\/" (X9,L));
reconsider a = a9 as
Element of (L
.: ) by
A1;
(
LattRel (L
.: ))
= ((
LattRel L)
~ ) by
LATTICE3: 20;
then
A2: (
LattRel ((L
.: )
.: ))
= (((
LattRel L)
~ )
~ ) by
LATTICE3: 20;
A3: for b be
Element of (L
.: ) st b
is_less_than X holds b
[= a
proof
let b be
Element of (L
.: );
reconsider b9 = b as
Element of L by
A1;
assume
A4: b
is_less_than X;
X9
is_less_than b9
proof
let q be
Element of L;
reconsider q9 = q as
Element of (L
.: ) by
A1;
assume q
in X9;
then b
[= q9 by
A4;
then (b
% )
<= (q9
% ) by
LATTICE3: 7;
then
[(b
% ), (q9
% )]
in the
InternalRel of (
LattPOSet (L
.: )) by
ORDERS_2:def 5;
then
[(q9
% ), (b
% )]
in (the
InternalRel of (
LattPOSet (L
.: ))
~ ) by
RELAT_1:def 7;
then
[(q9
% ), (b
% )]
in the
InternalRel of (
LattPOSet ((L
.: )
.: )) by
LATTICE3: 20;
then (q
% )
<= (b9
% ) by
A2,
ORDERS_2:def 5;
hence thesis by
LATTICE3: 7;
end;
then a9
[= b9 by
LATTICE3:def 21;
then (a9
% )
<= (b9
% ) by
LATTICE3: 7;
then
[(a9
% ), (b9
% )]
in the
InternalRel of (
LattPOSet L) by
ORDERS_2:def 5;
then
[(b9
% ), (a9
% )]
in (the
InternalRel of (
LattPOSet L)
~ ) by
RELAT_1:def 7;
then
[(b9
% ), (a9
% )]
in the
InternalRel of (
LattPOSet (L
.: )) by
LATTICE3: 20;
then (b
% )
<= (a
% ) by
ORDERS_2:def 5;
hence thesis by
LATTICE3: 7;
end;
A5: X9
is_less_than a9 by
LATTICE3:def 21;
a
is_less_than X
proof
let q9 be
Element of (L
.: );
reconsider q = q9 as
Element of L by
A1;
assume q9
in X;
then q
[= a9 by
A5;
then (q
% )
<= (a9
% ) by
LATTICE3: 7;
then
[(q
% ), (a9
% )]
in the
InternalRel of (
LattPOSet L) by
ORDERS_2:def 5;
then
[(a9
% ), (q
% )]
in (the
InternalRel of (
LattPOSet L)
~ ) by
RELAT_1:def 7;
then
[(a9
% ), (q
% )]
in the
InternalRel of (
LattPOSet (L
.: )) by
LATTICE3: 20;
then (a
% )
<= (q9
% ) by
ORDERS_2:def 5;
hence thesis by
LATTICE3: 7;
end;
hence thesis by
A3;
end;
end
definition
let C be
FormalContext;
::
CONLAT_2:def7
func C
.: ->
strict non
empty non
void
ContextStr equals
ContextStr (# the
carrier' of C, the
carrier of C, (the
Information of C
~ ) #);
coherence ;
end
theorem ::
CONLAT_2:17
for C be
strict
FormalContext holds ((C
.: )
.: )
= C;
theorem ::
CONLAT_2:18
Th18: for C be
FormalContext holds for O be
Subset of the
carrier of C holds ((
ObjectDerivation C)
. O)
= ((
AttributeDerivation (C
.: ))
. O)
proof
let C be
FormalContext;
let O be
Subset of the
carrier of C;
reconsider O9 = O as
Subset of the
carrier' of (C
.: );
set A1 = { a where a be
Attribute of C : for o be
Object of C st o
in O holds o
is-connected-with a };
set A2 = { a where a be
Object of (C
.: ) : for o be
Attribute of (C
.: ) st o
in O9 holds a
is-connected-with o };
A1: A1
c= A2
proof
let u be
object;
assume u
in A1;
then
consider a be
Attribute of C such that
A2: a
= u and
A3: for o be
Object of C st o
in O holds o
is-connected-with a;
reconsider u9 = u as
Object of (C
.: ) by
A2;
for o9 be
Attribute of (C
.: ) st o9
in O9 holds u9
is-connected-with o9
proof
let o9 be
Attribute of (C
.: );
reconsider o = o9 as
Object of C;
assume o9
in O9;
then o
is-connected-with a by
A3;
then
[o, a]
in the
Information of C by
CONLAT_1:def 2;
then
[a, o]
in the
Information of (C
.: ) by
RELAT_1:def 7;
hence thesis by
A2,
CONLAT_1:def 2;
end;
hence thesis;
end;
A4: A2
c= A1
proof
let u be
object;
assume u
in A2;
then
consider a be
Object of (C
.: ) such that
A5: a
= u and
A6: for o be
Attribute of (C
.: ) st o
in O9 holds a
is-connected-with o;
reconsider u9 = u as
Attribute of C by
A5;
for o be
Object of C st o
in O holds o
is-connected-with u9
proof
let o9 be
Object of C;
reconsider o = o9 as
Attribute of (C
.: );
assume o9
in O;
then a
is-connected-with o by
A6;
then
[a, o]
in the
Information of (C
.: ) by
CONLAT_1:def 2;
then
[o9, u9]
in the
Information of C by
A5,
RELAT_1:def 7;
hence thesis by
CONLAT_1:def 2;
end;
hence thesis;
end;
((
ObjectDerivation C)
. O)
= { a where a be
Attribute of C : for o be
Object of C st o
in O holds o
is-connected-with a } & ((
AttributeDerivation (C
.: ))
. O9)
= { a where a be
Object of (C
.: ) : for o be
Attribute of (C
.: ) st o
in O9 holds a
is-connected-with o } by
CONLAT_1:def 3,
CONLAT_1:def 4;
hence thesis by
A1,
A4;
end;
theorem ::
CONLAT_2:19
Th19: for C be
FormalContext holds for A be
Subset of the
carrier' of C holds ((
AttributeDerivation C)
. A)
= ((
ObjectDerivation (C
.: ))
. A)
proof
let C be
FormalContext;
let O be
Subset of the
carrier' of C;
reconsider O9 = O as
Subset of the
carrier of (C
.: );
set A1 = { a where a be
Object of C : for o be
Attribute of C st o
in O holds a
is-connected-with o };
set A2 = { a where a be
Attribute of (C
.: ) : for o be
Object of (C
.: ) st o
in O9 holds o
is-connected-with a };
A1: A1
c= A2
proof
let u be
object;
assume u
in A1;
then
consider a be
Object of C such that
A2: a
= u and
A3: for o be
Attribute of C st o
in O holds a
is-connected-with o;
reconsider u9 = u as
Attribute of (C
.: ) by
A2;
for o be
Object of (C
.: ) st o
in O9 holds o
is-connected-with u9
proof
let o9 be
Object of (C
.: );
reconsider o = o9 as
Attribute of C;
assume o9
in O9;
then a
is-connected-with o by
A3;
then
[a, o]
in the
Information of C by
CONLAT_1:def 2;
then
[o9, u9]
in the
Information of (C
.: ) by
A2,
RELAT_1:def 7;
hence thesis by
CONLAT_1:def 2;
end;
hence thesis;
end;
A4: A2
c= A1
proof
let u be
object;
assume u
in A2;
then
consider a be
Attribute of (C
.: ) such that
A5: a
= u and
A6: for o be
Object of (C
.: ) st o
in O9 holds o
is-connected-with a;
reconsider u9 = u as
Object of C by
A5;
for o be
Attribute of C st o
in O holds u9
is-connected-with o
proof
let o9 be
Attribute of C;
reconsider o = o9 as
Object of (C
.: );
assume o9
in O;
then o
is-connected-with a by
A6;
then
[o, a]
in the
Information of (C
.: ) by
CONLAT_1:def 2;
then
[u9, o9]
in the
Information of C by
A5,
RELAT_1:def 7;
hence thesis by
CONLAT_1:def 2;
end;
hence thesis;
end;
((
AttributeDerivation C)
. O)
= { a where a be
Object of C : for o be
Attribute of C st o
in O holds a
is-connected-with o } & ((
ObjectDerivation (C
.: ))
. O9)
= { a where a be
Attribute of (C
.: ) : for o be
Object of (C
.: ) st o
in O9 holds o
is-connected-with a } by
CONLAT_1:def 3,
CONLAT_1:def 4;
hence thesis by
A1,
A4;
end;
definition
let C be
FormalContext;
let CP be
ConceptStr over C;
::
CONLAT_2:def8
func CP
.: ->
strict
ConceptStr over (C
.: ) means
:
Def8: the
Extent of it
= the
Intent of CP & the
Intent of it
= the
Extent of CP;
existence
proof
reconsider O = the
Intent of CP as
Subset of the
carrier of (C
.: );
reconsider A = the
Extent of CP as
Subset of the
carrier' of (C
.: );
take
ConceptStr (# O, A #);
thus thesis;
end;
uniqueness ;
end
registration
let C be
FormalContext;
let CP be
FormalConcept of C;
cluster (CP
.: ) -> non
empty
concept-like;
coherence
proof
reconsider O = the
Intent of CP as
Subset of the
carrier of (C
.: );
reconsider A = the
Extent of CP as
Subset of the
carrier' of (C
.: );
set CPD =
ConceptStr (# O, A #);
A1: ((
AttributeDerivation (C
.: ))
. the
Intent of CPD)
= ((
ObjectDerivation C)
. the
Extent of CP) by
Th18
.= the
Extent of CPD by
CONLAT_1:def 10;
A2: CPD
= (CP
.: ) by
Def8;
((
ObjectDerivation (C
.: ))
. the
Extent of CPD)
= ((
AttributeDerivation C)
. the
Intent of CP) by
Th19
.= the
Intent of CPD by
CONLAT_1:def 10;
hence thesis by
A1,
A2,
Lm3,
CONLAT_1:def 10;
end;
end
theorem ::
CONLAT_2:20
for C be
strict
FormalContext holds for CP be
strict
FormalConcept of C holds ((CP
.: )
.: )
= CP
proof
let C be
strict
FormalContext;
let CP be
strict
FormalConcept of C;
A1: the
Intent of ((CP
.: )
.: )
= the
Extent of (CP
.: ) by
Def8
.= the
Intent of CP by
Def8;
the
Extent of ((CP
.: )
.: )
= the
Intent of (CP
.: ) by
Def8
.= the
Extent of CP by
Def8;
hence thesis by
A1;
end;
definition
let C be
FormalContext;
::
CONLAT_2:def9
func
DualHomomorphism (C) ->
Homomorphism of ((
ConceptLattice C)
.: ), (
ConceptLattice (C
.: )) means
:
Def9: for CP be
strict
FormalConcept of C holds (it
. CP)
= (CP
.: );
existence
proof
set f = {
[
ConceptStr (# O, A #), (
ConceptStr (# O, A #)
.: )] where O be
Subset of the
carrier of C, A be
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;
f
c=
[:the
carrier of ((
ConceptLattice C)
.: ), the
carrier of (
ConceptLattice (C
.: )):]
proof
let y be
object;
assume y
in f;
then
consider O be
Subset of the
carrier of C, A be
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 thesis by
A4,
A6,
ZFMISC_1:def 2;
end;
then
reconsider f 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;
assume y
in the
carrier of ((
ConceptLattice C)
.: );
then
A7: y is
strict
FormalConcept of C by
A3,
CONLAT_1: 31;
then
consider O9 be
Subset of the
carrier of C, A9 be
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 as
Element of (
ConceptLattice (C
.: )) by
A1,
CONLAT_1: 31;
[y, z]
in f by
A7,
A8;
hence thesis by
XTUPLE_0:def 12;
end;
then
A9: the
carrier of ((
ConceptLattice C)
.: )
= (
dom f);
for x,y1,y2 be
object st
[x, y1]
in f &
[x, y2]
in f holds y1
= y2
proof
let x,y1,y2 be
object;
assume that
A10:
[x, y1]
in f and
A11:
[x, y2]
in f;
consider O9 be
Subset of the
carrier of C, A9 be
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 be
Subset of the
carrier of C, A be
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;
end;
then
reconsider 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 be
Element of ((
ConceptLattice C)
.: ) holds a
[= b implies (f
. a)
[= (f
. b)
proof
let a,b be
Element of ((
ConceptLattice C)
.: );
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 be
object such that
A18:
[a, fa]
in f by
XTUPLE_0:def 12;
assume a
[= 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 be
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 be
Subset of the
carrier of C, A9 be
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 be
Subset of the
carrier of C, A be
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 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 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 thesis by
A27,
A23,
CONLAT_1: 43;
end;
the
carrier of (
ConceptLattice (C
.: ))
c= (
rng f)
proof
let u be
object;
A31: (
dom f)
= the
carrier of ((
ConceptLattice C)
.: ) by
FUNCT_2:def 1;
assume u
in the
carrier of (
ConceptLattice (C
.: ));
then
reconsider 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 & the
Intent of (u
@ ) is
empty) by
CONLAT_1:def 8;
A33: ((
AttributeDerivation C)
. the
Intent of CP)
= ((
ObjectDerivation (C
.: ))
. the
Extent of (u
@ )) by
Th19
.= the
Extent of CP by
CONLAT_1:def 10;
((
ObjectDerivation C)
. the
Extent of CP)
= ((
AttributeDerivation (C
.: ))
. the
Intent of (u
@ )) by
Th18
.= the
Intent of CP by
CONLAT_1:def 10;
then CP is
FormalConcept of C by
A33,
A32,
CONLAT_1:def 8,
CONLAT_1:def 10;
then CP
in (
dom f) by
A15,
A2,
A31,
CONLAT_1: 31;
then
consider v be
object such that
A34:
[CP, v]
in f by
XTUPLE_0:def 12;
consider Ov be
Subset of the
carrier of C, Av be
Subset of the
carrier' of C such that
A35:
[CP, v]
=
[
ConceptStr (# Ov, Av #), (
ConceptStr (# Ov, Av #)
.: )] and
ConceptStr (# Ov, Av #) is
FormalConcept of C by
A34;
A36: CP
= (
[CP, 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 as
strict
FormalConcept of (C
.: ) by
A1,
CONLAT_1: 31;
v
= (
[CP, 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 thesis by
A37,
CONLAT_1:def 21;
end;
then
A38: (
rng f)
= the
carrier of (
ConceptLattice (C
.: ));
A39: f is
one-to-one
proof
let a,b be
object;
assume that
A40: a
in (
dom f) and
A41: b
in (
dom f) and
A42: (f
. a)
= (f
. b);
reconsider a, b as
Element of ((
ConceptLattice C)
.: ) by
A40,
A41;
consider fa be
object such that
A43:
[a, fa]
in f by
A40,
XTUPLE_0:def 12;
consider fb be
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 be
Subset of the
carrier of C, A be
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 be
Subset of the
carrier of C, A9 be
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 thesis by
A47,
A49,
A51;
end;
for a,b be
Element of ((
ConceptLattice C)
.: ) holds (f
. a)
[= (f
. b) implies a
[= b
proof
let a,b be
Element of ((
ConceptLattice C)
.: );
A52: (
dom f)
= the
carrier of ((
ConceptLattice C)
.: ) by
FUNCT_2:def 1;
then
consider fa be
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);
then
A54: ((f
. a)
@ )
is-SubConcept-of ((f
. b)
@ ) by
CONLAT_1: 43;
consider O be
Subset of the
carrier of C, A be
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 be
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 be
Subset of the
carrier of C, A9 be
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 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 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 thesis by
LATTICE3: 7;
end;
then
reconsider f as
Homomorphism of ((
ConceptLattice C)
.: ), (
ConceptLattice (C
.: )) by
A16,
A38,
A39,
Lm2;
for CP be
strict
FormalConcept of C holds (f
. CP)
= (CP
.: )
proof
let CP be
strict
FormalConcept of C;
CP
in (
B-carrier C) by
CONLAT_1: 31;
then CP
in (
dom f) by
A3,
FUNCT_2:def 1;
then
consider v be
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 be
Subset of the
carrier of C, Av be
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 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 thesis by
A65,
A68,
FUNCT_1: 1;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be
Homomorphism of ((
ConceptLattice C)
.: ), (
ConceptLattice (C
.: ));
assume
A69: for CP be
strict
FormalConcept of C holds (F1
. CP)
= (CP
.: );
assume
A70: for CP be
strict
FormalConcept of C holds (F2
. CP)
= (CP
.: );
A71: for u be
object st u
in the
carrier of ((
ConceptLattice C)
.: ) holds (F1
. u)
= (F2
. u)
proof
let u be
object;
(
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
then
A72: ((
ConceptLattice C)
.: )
=
LattStr (# (
B-carrier C), (
B-meet C), (
B-join C) #) by
LATTICE2:def 2;
assume u
in the
carrier of ((
ConceptLattice C)
.: );
then
reconsider u as
strict
FormalConcept of C by
A72,
CONLAT_1: 31;
(F1
. u)
= (u
.: ) by
A69
.= (F2
. u) by
A70;
hence thesis;
end;
(
dom F1)
= the
carrier of ((
ConceptLattice C)
.: ) & (
dom F2)
= the
carrier of ((
ConceptLattice C)
.: ) by
FUNCT_2:def 1;
hence thesis by
A71;
end;
end
theorem ::
CONLAT_2:21
Th21: for C be
FormalContext holds (
DualHomomorphism C) is
bijective
proof
let C be
FormalContext;
set f = (
DualHomomorphism C);
A1: (
ConceptLattice C)
=
LattStr (# (
B-carrier C), (
B-join C), (
B-meet C) #) by
CONLAT_1:def 20;
A2: ((
ConceptLattice C)
.: )
=
LattStr (# the
carrier of (
ConceptLattice C), the
L_meet of (
ConceptLattice C), the
L_join of (
ConceptLattice C) #) by
LATTICE2:def 2;
the
carrier of (
ConceptLattice (C
.: ))
c= (
rng f)
proof
let u be
object;
assume u
in the
carrier of (
ConceptLattice (C
.: ));
then
reconsider 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 #);
A3: not (the
Extent of (u
@ ) is
empty & the
Intent of (u
@ ) is
empty) by
CONLAT_1:def 8;
A4: ((
AttributeDerivation C)
. the
Intent of CP)
= ((
ObjectDerivation (C
.: ))
. the
Extent of (u
@ )) by
Th19
.= the
Extent of CP by
CONLAT_1:def 10;
A5: ((
ObjectDerivation C)
. the
Extent of CP)
= ((
AttributeDerivation (C
.: ))
. the
Intent of (u
@ )) by
Th18
.= the
Intent of CP by
CONLAT_1:def 10;
then CP is
FormalConcept of C by
A4,
A3,
CONLAT_1:def 8,
CONLAT_1:def 10;
then
A6: CP
in the
carrier of (
ConceptLattice C) by
A1,
CONLAT_1: 31;
reconsider CP as
strict
FormalConcept of C by
A5,
A4,
A3,
CONLAT_1:def 8,
CONLAT_1:def 10;
A7: the
Extent of (CP
.: )
= the
Extent of (u
@ ) by
Def8;
(f
. CP)
= (CP
.: ) & the
Intent of (CP
.: )
= the
Intent of (u
@ ) by
Def8,
Def9;
then
A8: (f
. CP)
= u by
A7,
CONLAT_1:def 21;
CP
in (
dom f) by
A2,
A6,
FUNCT_2:def 1;
hence thesis by
A8,
FUNCT_1:def 3;
end;
then (
rng f)
= the
carrier of (
ConceptLattice (C
.: ));
then
A9: f is
onto by
FUNCT_2:def 3;
f is
one-to-one
proof
let a,b be
object;
assume that
A10: a
in (
dom f) & b
in (
dom f) and
A11: (f
. a)
= (f
. b);
reconsider a, b as
Element of ((
ConceptLattice C)
.: ) by
A10;
((
ConceptLattice C)
.: )
=
LattStr (# the
carrier of (
ConceptLattice C), the
L_meet of (
ConceptLattice C), the
L_join of (
ConceptLattice C) #) by
LATTICE2:def 2;
then
reconsider a, b as
Element of (
ConceptLattice C);
A12: (f
. (a
@ ))
= (f
. a) & (f
. (b
@ ))
= (f
. b) by
CONLAT_1:def 21;
A13: (f
. (a
@ ))
= ((a
@ )
.: ) & (f
. (b
@ ))
= ((b
@ )
.: ) by
Def9;
then
A14: the
Extent of (a
@ )
= the
Intent of ((b
@ )
.: ) by
A11,
A12,
Def8
.= the
Extent of (b
@ ) by
Def8;
the
Intent of (a
@ )
= the
Extent of ((b
@ )
.: ) by
A11,
A13,
A12,
Def8
.= the
Intent of (b
@ ) by
Def8;
then a
= (b
@ ) by
A14,
CONLAT_1:def 21
.= b by
CONLAT_1:def 21;
hence thesis;
end;
hence thesis by
A9;
end;
theorem ::
CONLAT_2:22
for C be
FormalContext holds ((
ConceptLattice (C
.: )),((
ConceptLattice C)
.: ))
are_isomorphic
proof
let C be
FormalContext;
(
DualHomomorphism C) is
bijective by
Th21;
hence thesis by
LATTICE4:def 3;
end;