Copyright (c) 1999 Association of Mizar Users
environ
vocabulary CONLAT_1, QC_LANG1, LATTICES, CAT_1, FUNCT_1, TARSKI, SETFAM_1,
BOOLE, LATTICE3, SUBSET_1, RELAT_1, FUNCT_3, LATTICE6, BHSP_3, GROUP_6,
WELLORD1, MOD_4, MCART_1, FILTER_1, ORDERS_1, CONLAT_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, MCART_1, FUNCT_1,
DOMAIN_1, RELSET_1, PRE_TOPC, ORDERS_1, STRUCT_0, LATTICE2, LATTICE3,
LATTICE6, PARTFUN1, FUNCT_2, LATTICES, LATTICE4, CONLAT_1;
constructors DOMAIN_1, LATTICE2, LATTICE4, LATTICE6, CONLAT_1, MEMBERED,
PRE_TOPC;
clusters STRUCT_0, LATTICE3, PRE_TOPC, RELSET_1, LATTICE2, CONLAT_1, SUBSET_1,
SETFAM_1, LATTICES, FUNCT_2, PARTFUN1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, VECTSP_8, LATTICE6, FUNCT_1, XBOOLE_0;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, LATTICE4, LATTICES, LATTICE3,
LATTICE6, MCART_1, SETFAM_1, SUBSET_1, FUNCT_2, RELSET_1, FILTER_1,
LATTICE2, ORDERS_1, CONLAT_1, XBOOLE_0;
schemes FUNCT_2;
begin
definition
let C be FormalContext;
let CP be strict FormalConcept of C;
func @CP -> Element of ConceptLattice(C) equals :Def1:
CP;
coherence
proof
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
then CP is Element of ConceptLattice(C) by CONLAT_1:35;
hence CP is Element of ConceptLattice(C);
end;
end;
definition let C be FormalContext;
cluster ConceptLattice C -> bounded;
coherence
proof
A1: (@Concept-with-all-Attributes(C))@
= @Concept-with-all-Attributes(C) by CONLAT_1:def 24
.= Concept-with-all-Attributes(C) by Def1;
A2: for a being 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 A1,CONLAT_1:34;
hence thesis by CONLAT_1:47;
end;
for a being 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)
proof
let a be Element of ConceptLattice(C);
@Concept-with-all-Attributes(C) [= a by A2;
hence thesis by LATTICES:21;
end;
then A3: ConceptLattice C is lower-bounded by LATTICES:def 13;
A4: (@Concept-with-all-Objects(C))@
= @Concept-with-all-Objects(C) by CONLAT_1:def 24
.= Concept-with-all-Objects(C) by Def1;
A5: for a being 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 A4,CONLAT_1:34;
hence thesis by CONLAT_1:47;
end;
for a being 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)
proof
let a be Element of ConceptLattice(C);
a [= @Concept-with-all-Objects(C) by A5;
hence thesis by LATTICES:def 3;
end;
then ConceptLattice C is upper-bounded by LATTICES:def 14;
hence thesis by A3,LATTICES:def 15;
end;
end;
theorem
Th1:for C being 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-Attributes(C))@
= @Concept-with-all-Attributes(C) by CONLAT_1:def 24
.= Concept-with-all-Attributes(C) by Def1;
A2: for a being 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 A1,CONLAT_1:34;
hence thesis by CONLAT_1:47;
end;
for a being 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)
proof
let a be Element of ConceptLattice(C);
@Concept-with-all-Attributes(C) [= a by A2;
hence thesis by LATTICES:21;
end;
then A3: Bottom (ConceptLattice(C)) = @Concept-with-all-Attributes(C)
by LATTICES:def 16;
A4: (@Concept-with-all-Objects(C))@
= @Concept-with-all-Objects(C) by CONLAT_1:def 24
.= Concept-with-all-Objects(C) by Def1;
A5: for a being 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 A4,CONLAT_1:34;
hence thesis by CONLAT_1:47;
end;
for a being 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)
proof
let a be Element of ConceptLattice(C);
a [= @Concept-with-all-Objects(C) by A5;
hence thesis by LATTICES:def 3;
end;
then Top (ConceptLattice(C)) = @Concept-with-all-Objects(C) by LATTICES:def 17
;
hence thesis by A3,Def1;
end;
theorem
Th2:for C being FormalContext
for D being non empty Subset of bool(the Objects of C) holds
(ObjectDerivation(C)).(union D) =
meet({(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D})
proof
let C be FormalContext;
let D be non empty Subset of bool(the Objects of C);
reconsider D'=D as non empty Subset-Family of the Objects of C
by SETFAM_1:def 7;
set OU = (ObjectDerivation(C)).(union D);
set M = meet({(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D});
per cases;
suppose A1: {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D} <> {};
thus OU c= M
proof
let x be set; assume x in OU;
then x in {a' where a' is Attribute of C :
for o being Object of C st o in union D' holds o is-connected-with a'}
by CONLAT_1:def 6;
then consider x' being Attribute of C such that A2: x' = x &
for o being Object of C st o in union D holds o is-connected-with x';
reconsider x as Attribute of C by A2;
A3: for O being Subset of the Objects of C st O in D
for o being Object of C st o in O holds o is-connected-with x
proof
let O be Subset of the Objects 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 being Subset of the Objects of C st O in D holds
x in (ObjectDerivation(C)).O
proof
let O be Subset of the Objects of C; assume O in D;
then for o being Object of C st o in O holds o is-connected-with x
by A3;
then x in {a where a is Attribute of C :
for o being Object of C st o in O holds o is-connected-with a };
hence thesis by CONLAT_1:def 6;
end;
for Y being set holds Y in {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D} implies x in Y
proof
let Y be set; assume Y in {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D};
then consider O being Subset of the Objects of C such that
A6: Y = (ObjectDerivation(C)).O & O in D;
thus thesis by A5,A6;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
thus M c= OU
proof
let x be set; assume A7: x in M;
consider d being Element of {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D};
A8: d in {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D} by A1;
A9: x in d by A1,A7,SETFAM_1:def 1;
consider X being Subset of the Objects of C such that A10:
d = (ObjectDerivation(C)).X & X in D by A8;
reconsider x as Attribute of C by A9,A10;
A11: for O being Subset of the Objects of C st O in D holds
x in (ObjectDerivation(C)).O
proof
let O be Subset of the Objects of C; assume O in D;
then (ObjectDerivation(C)).O in
{(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in D};
hence thesis by A7,SETFAM_1:def 1;
end;
A12: for O being Subset of the Objects of C st O in D
for o being Object of C st o in O holds o is-connected-with x
proof
let O be Subset of the Objects of C; assume A13: O in D;
let o be Object of C; assume A14: o in O;
x in (ObjectDerivation(C)).O by A11,A13;
then x in {a where a is Attribute of C :
for o being Object of C st o in O holds o is-connected-with a}
by CONLAT_1:def 6;
then consider x' being Attribute of C such that A15: x' = x &
for o being Object of C st o in O holds o is-connected-with x';
thus thesis by A14,A15;
end;
for o being 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 consider Y being set such that A16: o in Y & Y in D by TARSKI:def 4
;
thus thesis by A12,A16;
end;
then x in {a' where a' is Attribute of C :
for o being Object of C st o in union D' holds o is-connected-with a'};
hence thesis by CONLAT_1:def 6;
end;
suppose A17: {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D} = {};
D = {}
proof
assume D <> {};
consider x being Element of D;
(ObjectDerivation(C)).x in {(ObjectDerivation(C)).O
where O is Subset of the Objects of C : O in D};
hence thesis by A17;
end;
hence thesis;
end;
theorem
Th3:for C being FormalContext
for D being non empty Subset of bool(the Attributes of C) holds
(AttributeDerivation(C)).(union D) =
meet({(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D})
proof
let C be FormalContext;
let D be non empty Subset of bool(the Attributes of C);
reconsider D'=D as non empty Subset-Family of the Attributes of C
by SETFAM_1:def 7;
set OU = (AttributeDerivation(C)).(union D);
set M = meet({(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D});
now per cases;
case A1: {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D} <> {};
thus OU = M
proof
thus OU c= M
proof
let x be set; assume x in OU;
then x in {o' where o' is Object of C :
for a being Attribute of C st a in
union D' holds o' is-connected-with a}
by CONLAT_1:def 7;
then consider x' being Object of C such that A2: x' = x &
for a being Attribute of C st a in
union D holds x' is-connected-with a;
reconsider x as Object of C by A2;
A3: for A being Subset of the Attributes of C st A in D
for a being Attribute of C st a in A holds x is-connected-with a
proof
let A be Subset of the Attributes 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 being Subset of the Attributes of C st A in D holds
x in (AttributeDerivation(C)).A
proof
let A be Subset of the Attributes of C; assume A in D;
then for a being Attribute of C st a in
A holds x is-connected-with a by A3;
then x in {o where o is Object of C :
for a being Attribute of C st a in
A holds o is-connected-with a};
hence thesis by CONLAT_1:def 7;
end;
for Y being set holds
Y in {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D} implies x in Y
proof
let Y be set; assume
Y in {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D};
then consider A being Subset of the Attributes of C such that
A6: Y = (AttributeDerivation(C)).A & A in D;
thus thesis by A5,A6;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
let x be set; assume A7: x in M;
consider d being Element of {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D};
A8: d in {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D} by A1;
A9: x in d by A1,A7,SETFAM_1:def 1;
consider X being Subset of the Attributes of C such that A10:
d = (AttributeDerivation(C)).X & X in D by A8;
reconsider x as Object of C by A9,A10;
A11: for A being Subset of the Attributes of C st A in D holds
x in (AttributeDerivation(C)).A
proof
let A be Subset of the Attributes of C; assume A in D;
then (AttributeDerivation(C)).A in {(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in D};
hence thesis by A7,SETFAM_1:def 1;
end;
A12: for A being Subset of the Attributes of C st A in D
for a being Attribute of C st a in A holds x is-connected-with a
proof
let A be Subset of the Attributes of C; assume A13: A in D;
let a be Attribute of C; assume A14: a in A;
x in (AttributeDerivation(C)).A by A11,A13;
then x in {o where o is Object of C :
for a being Attribute of C st a in A holds o is-connected-with a}
by CONLAT_1:def 7;
then consider x' being Object of C such that A15: x' = x &
for a being Attribute of C st a in
A holds x' is-connected-with a;
thus thesis by A14,A15;
end;
for a being 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 consider Y being set such that A16: a in Y & Y in D by TARSKI:def 4
;
thus thesis by A12,A16;
end;
then x in {o' where o' is Object of C :
for a being Attribute of C st a in
union D' holds o' is-connected-with a};
hence thesis by CONLAT_1:def 7;
end;
case A17: {(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D} = {};
D = {}
proof
assume D <> {};
consider x being Element of D;
(AttributeDerivation(C)).x in
{(AttributeDerivation(C)).A
where A is Subset of the Attributes of C : A in D};
hence thesis by A17;
end;
hence thesis;
end;
hence thesis;
end;
theorem
Th4:for C being FormalContext
for D being 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 23;
hence thesis by CONLAT_1:35;
end;
definition
let C be FormalContext;
let D be Subset of ConceptLattice(C);
func "/\"(D,C) -> FormalConcept of C equals :Def2:
"/\"(D,ConceptLattice(C));
coherence by Th4;
func "\/"(D,C) -> FormalConcept of C equals :Def3:
"\/"(D,ConceptLattice(C));
coherence by Th4;
end;
theorem
for C being FormalContext holds
"\/"({} ConceptLattice(C),C) = Concept-with-all-Attributes(C) &
"/\"({} ConceptLattice(C),C) = Concept-with-all-Objects(C)
proof
let C be FormalContext;
"\/"({} ConceptLattice(C),ConceptLattice(C)) = Bottom ConceptLattice(C)
by LATTICE3:50;
then A1: "\/"({} ConceptLattice(C),C) = Bottom ConceptLattice(C) by Def3;
for q being Element of ConceptLattice(C) st q in {}
holds @Concept-with-all-Objects(C) [= q;
then A2: @Concept-with-all-Objects(C) is_less_than {} by LATTICE3:def 16;
for b being 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 {};
A3: b@ is-SubConcept-of Concept-with-all-Objects(C) by CONLAT_1:34;
Concept-with-all-Objects(C)
= @Concept-with-all-Objects(C) by Def1
.= (@Concept-with-all-Objects(C))@ by CONLAT_1:def 24;
hence thesis by A3,CONLAT_1:47;
end;
then "/\"
({},ConceptLattice(C)) = @Concept-with-all-Objects(C) by A2,LATTICE3:34;
then "/\"({} ConceptLattice(C),C) = @Concept-with-all-Objects(C) by Def2;
hence thesis by A1,Def1,Th1;
end;
theorem
for C being 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;
"\/"(the carrier of ConceptLattice(C),ConceptLattice(C)) =
Top ConceptLattice(C) by LATTICE3:51;
then "\/"
([#]
the carrier of ConceptLattice(C),ConceptLattice(C)) = Top ConceptLattice(C)
by SUBSET_1:def 4;
then A1: "\/"([#] the carrier of ConceptLattice(C),C) = Top
ConceptLattice(C) by Def3;
A2: @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);
A3: Concept-with-all-Attributes(C) is-SubConcept-of q@ by CONLAT_1:34;
Concept-with-all-Attributes(C)
= @Concept-with-all-Attributes(C) by Def1
.= (@Concept-with-all-Attributes(C))@ by CONLAT_1:def 24;
hence thesis by A3,CONLAT_1:47;
end;
for b being Element of ConceptLattice(C)
st b is_less_than [#] the carrier of ConceptLattice(C)
holds b [= @Concept-with-all-Attributes(C)
proof
let b be Element of ConceptLattice(C);
assume A4: b is_less_than [#] the carrier of ConceptLattice(C);
@Concept-with-all-Attributes(C) in the carrier of ConceptLattice(C);
then @Concept-with-all-Attributes(C) in [#] the carrier of ConceptLattice(C)
by SUBSET_1:def 4;
hence thesis by A4,LATTICE3:def 16;
end;
then "/\"([#] the carrier of ConceptLattice(C),ConceptLattice(C)) =
@Concept-with-all-Attributes(C) by A2,LATTICE3:34;
then "/\"([#] the carrier of ConceptLattice(C),C) =
@Concept-with-all-Attributes(C) by Def2;
hence thesis by A1,Def1,Th1;
end;
theorem
for C being FormalContext
for D being 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 is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}) &
the Intent of "\/"(D,C) =
meet {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes 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 is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D});
A1: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
A2: for x being set holds x in D implies
x is strict FormalConcept of C &
ex E being Subset of the Objects of C,
I being Subset of the Attributes of C st x = ConceptStr(#E,I#)
proof
let x be set; assume x in D;
then x is strict FormalConcept of C by A1,CONLAT_1:35;
hence thesis;
end;
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
bool (the Objects of C)
proof
let x be set; assume
x in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that
A3: x = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
thus thesis by A3;
end;
then reconsider OO = {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
as Subset of bool (the Objects of C);
set A' = (ObjectDerivation(C)).
union {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C such that
A4: y = ConceptStr(#E',I'#)by A2;
the Extent of y in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} by A4;
then reconsider OO as non empty Subset of bool (the Objects of C);
A5: A' = meet({(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in OO}) by Th2;
A6: {(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}} =
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
thus {(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}} c=
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
let x be set; assume x in {(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}};
then consider O' being Subset of the Objects of C such that A7:
x = (ObjectDerivation(C)).O' & O' in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A8:
O' = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A7;
ConceptStr(#E,I#) is FormalConcept of C by A2,A8;
then x = the Intent of ConceptStr(#E,I#) by A7,A8,CONLAT_1:def 13;
hence thesis by A8;
end;
thus {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
{(ObjectDerivation(C)).O'
where O' is Subset of the Objects of C : O' in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}}
proof
let x be set; assume x in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A9:
x = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
ConceptStr(#E,I#) is FormalConcept of C by A2,A9;
then A10: x = (ObjectDerivation(C)).(the Extent of ConceptStr(#E,I#))
by A9,CONLAT_1:def 13;
the Extent of ConceptStr(#E,I#) in {the Extent of ConceptStr(#EE,II#)
where EE is Subset of the Objects of C,
II is Subset of the Attributes of C : ConceptStr(#EE,II#) in D}
by A9;
hence thesis by A10;
end;
end;
A' c= the Attributes of C
proof
let x be set; assume A11: x in A';
consider Y being Element of {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C
such that A12: y = ConceptStr(#E',I'#) by A2;
A13: the Intent of y in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} by A12;
then Y in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E1 being Subset of the Objects of C,
I1 being Subset of the Attributes of C such that A14:
Y = the Intent of ConceptStr(#E1,I1#) & ConceptStr(#E1,I1#) in D;
x in Y by A5,A6,A11,A13,SETFAM_1:def 1;
hence thesis by A14;
end;
then reconsider a = A' as Subset of the Attributes of C;
O c= the Objects of C
proof
let x be set; assume A15: x in O;
set u = union {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
u c= the Objects of C
proof
let x be set; assume x in u;
then consider Y being set such that A16: x in Y & Y in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
by TARSKI:def 4;
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A17:
Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A16;
thus thesis by A16,A17;
end;
then reconsider u as Subset of the Objects of C;
(AttributeDerivation(C)).((ObjectDerivation(C)).u) is Element of
bool(the Objects of C);
hence thesis by A15;
end;
then reconsider o = O as Subset of the Objects of C;
union {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
the Objects of C
proof
let x be set; assume
x in union {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider Y being set such that A18: x in Y &
Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the Objects
of C,I is Subset of the Attributes of C :
ConceptStr(#E,I#) in D} by TARSKI:def 4;
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that
A19: Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A18;
thus thesis by A18,A19;
end;
then reconsider CP' = ConceptStr(#o,a#) as strict FormalConcept of C
by CONLAT_1:20;
reconsider CP = CP' as Element of ConceptLattice(C)
by A1,CONLAT_1:35;
A20: the Intent of CP@ = meet {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
by A5,A6,CONLAT_1:def 24;
A21: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 24;
then the Intent of q@ in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then the Intent of CP@ c= the Intent of q@ by A20,SETFAM_1:4;
then q@ is-SubConcept-of CP@ by CONLAT_1:31;
hence thesis by CONLAT_1:47;
end;
for r being 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 being 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,LATTICE3:def 17;
then q@ is-SubConcept-of r@ by CONLAT_1:47;
hence thesis by CONLAT_1:31;
end;
the Intent of r@ c=
meet {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
let x be set; assume A24: x in the Intent of r@;
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C such that
A25: y = ConceptStr(#E',I'#)by A2;
A26: the Intent of y in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} by
A25;
for Y being set holds Y in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes 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 is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider Ey being Subset of the Objects of C,
Iy being Subset of the Attributes of C such that A27:
Y = the Intent of ConceptStr(#Ey,Iy#) & 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 A27,CONLAT_1:def 24;
end;
hence thesis by A26,SETFAM_1:def 1;
end;
then CP@ is-SubConcept-of r@ by A20,CONLAT_1:31;
hence thesis by CONLAT_1:47;
end;
then CP = "\/"(D,ConceptLattice(C)) by A21,LATTICE3:def 21;
hence thesis by A5,A6,Def3;
end;
theorem
for C being FormalContext
for D being non empty Subset of ConceptLattice(C) holds
the Extent of "/\"(D,C) =
meet {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes 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 is Subset of the Objects of C,
I is Subset of the Attributes 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 is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D});
A1: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
A2: for x being set holds x in D implies
x is strict FormalConcept of C &
ex E being Subset of the Objects of C,
I being Subset of the Attributes of C st x = ConceptStr(#E,I#)
proof
let x be set; assume x in D;
then x is strict FormalConcept of C by A1,CONLAT_1:35;
hence thesis;
end;
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
bool (the Attributes of C)
proof
let x be set; assume x in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that
A3: x = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
thus thesis by A3;
end;
then reconsider AA = {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
as Subset of bool (the Attributes of C);
set O' = (AttributeDerivation(C)).
union {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C
such that A4: y = ConceptStr(#E',I'#)by A2;
the Intent of y in {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} by A4;
then reconsider AA as non empty Subset of bool (the Attributes of C);
A5: O' = meet({(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in AA}) by Th3;
A6:{(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}} =
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
thus {(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}} c=
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
let x be set; assume x in
{(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}};
then consider A' being Subset of the Attributes of C such that A7:
x = (AttributeDerivation(C)).A' & A' in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A8:
A' = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A7;
ConceptStr(#E,I#) is FormalConcept of C by A2,A8;
then x = the Extent of ConceptStr(#E,I#) by A7,A8,CONLAT_1:def 13;
hence thesis by A8;
end;
thus {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
{(AttributeDerivation(C)).A'
where A' is Subset of the Attributes of C : A' in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}}
proof
let x be set; assume x in
{the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A9:
x = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
ConceptStr(#E,I#) is FormalConcept of C by A2,A9;
then A10: x = (AttributeDerivation(C)).(the Intent of ConceptStr(#E,I#))
by A9,CONLAT_1:def 13;
the Intent of ConceptStr(#E,I#) in
{the Intent of ConceptStr(#EE,II#)
where EE is Subset of the Objects of C,
II is Subset of the Attributes of C : ConceptStr(#EE,II#) in
D} by A9
;
hence thesis by A10;
end;
end;
O' c= the Objects of C
proof
let x be set; assume A11: x in O';
consider Y being Element of {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C
such that A12: y = ConceptStr(#E',I'#)by A2;
A13: the Extent of y in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} by A12;
then Y in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider E1 being Subset of the Objects of C,
I1 being Subset of the Attributes of C such that
A14: Y = the Extent of ConceptStr(#E1,I1#) & ConceptStr(#E1,I1#) in D;
x in Y by A5,A6,A11,A13,SETFAM_1:def 1;
hence thesis by A14;
end;
then reconsider o = O' as Subset of the Objects of C;
A c= the Attributes of C
proof
let x be set; assume A15: x in A;
set u = union {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
u c= the Attributes of C
proof
let x be set; assume x in u;
then consider Y being set such that A16: x in Y & Y in
{the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
by TARSKI:def 4;
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that A17:
Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A16;
thus thesis by A16,A17;
end;
then reconsider u as Subset of the Attributes of C;
(ObjectDerivation(C)).((AttributeDerivation(C)).u) is Element of
bool(the Attributes of C);
hence thesis by A15;
end;
then reconsider a = A as Subset of the Attributes of C;
union {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D} c=
the Attributes of C
proof
let x be set; assume x in union {the Intent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider Y being set such that A18: x in Y &
Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the Objects
of C,I is Subset of the Attributes of C :
ConceptStr(#E,I#) in D} by TARSKI:def 4;
consider E being Subset of the Objects of C,
I being Subset of the Attributes of C such that
A19: Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A18;
thus thesis by A18,A19;
end;
then reconsider CP' = ConceptStr(#o,a#) as strict FormalConcept of C
by CONLAT_1:22;
reconsider CP = CP' as Element of ConceptLattice(C)
by A1,CONLAT_1:35;
A20: the Extent of CP@ = meet {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
by A5,A6,CONLAT_1:def 24;
A21: 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 24;
then the Extent of q@ in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then the Extent of CP@ c= the Extent of q@ by A20,SETFAM_1:4;
then CP@ is-SubConcept-of q@ by CONLAT_1:def 19;
hence thesis by CONLAT_1:47;
end;
for r being 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 being 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,LATTICE3:def 16;
then r@ is-SubConcept-of q@ by CONLAT_1:47;
hence thesis by CONLAT_1:def 19;
end;
the Extent of r@ c=
meet {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
proof
let x be set; assume A24: x in the Extent of r@;
consider y being Element of D;
consider E' being Subset of the Objects of C,
I' being Subset of the Attributes of C
such that A25: y = ConceptStr(#E',I'#)by A2;
A26: the Extent of y in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D}
by A25;
for Y being set holds Y in {the Extent of ConceptStr(#E,I#)
where E is Subset of the Objects of C,
I is Subset of the Attributes 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 is Subset of the Objects of C,
I is Subset of the Attributes of C : ConceptStr(#E,I#) in D};
then consider Ey being Subset of the Objects of C,
Iy being Subset of the Attributes of C such that A27:
Y = the Extent of ConceptStr(#Ey,Iy#) & 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 A27,CONLAT_1:def 24;
end;
hence thesis by A26,SETFAM_1:def 1;
end;
then r@ is-SubConcept-of CP@ by A20,CONLAT_1:def 19;
hence thesis by CONLAT_1:47;
end;
then CP = "/\"(D,ConceptLattice(C)) by A21,LATTICE3:34;
hence thesis by A5,A6,Def2;
end;
theorem
Th9:for C being FormalContext
for CP being strict FormalConcept of C holds
"\/"({ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being 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 is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being Object of C st
o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o}};
A1: D is_less_than @CP
proof
let q be Element of ConceptLattice(C);
assume q in D;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A2:
q = ConceptStr(#O,A#) &
ex o being Object of C st
o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
consider o being Object of C such that
A3: o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o} by A2;
A4: {o} c= the Extent of CP by A3,ZFMISC_1:37;
A5: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP
by CONLAT_1:def 13;
the Intent of q@
= (ObjectDerivation(C)).{o} by A2,A3,CONLAT_1:def 24;
then the Intent of CP c= the Intent of q@ by A4,A5,CONLAT_1:3;
then A6: q@ is-SubConcept-of CP by CONLAT_1:31;
CP = @CP by Def1 .= (@CP)@ by CONLAT_1:def 24;
hence thesis by A6,CONLAT_1:47;
end;
for CP' being Element of ConceptLattice(C) st
D is_less_than CP' holds @CP [= CP'
proof
let CP' be Element of ConceptLattice(C);
assume A7: D is_less_than CP';
A8:the Extent of CP c= the Extent of (CP')@
proof
let x be set; assume A9: x in the Extent of CP;
then reconsider x as Element of the Objects of C;
set Ox = (AttributeDerivation(C)).((ObjectDerivation(C)).{x});
set Ax = (ObjectDerivation(C)).{x};
reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C
by CONLAT_1:20;
{x} c= Ox by CONLAT_1:5;
then A11: x in the Extent of Cx by ZFMISC_1:37;
A12: Cx in {ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being Object of C st
o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o}} by A9;
@Cx = Cx by Def1;
then @Cx [= CP' by A7,A12,LATTICE3:def 17;
then A13: (@Cx)@ is-SubConcept-of (CP')@ by CONLAT_1:47;
Cx = @Cx by Def1 .= (@Cx)@ by CONLAT_1:def 24;
then the Extent of Cx c= the Extent of (CP')@ by A13,CONLAT_1:def 19;
hence thesis by A11;
end;
CP = @CP by Def1 .= (@CP)@ by CONLAT_1:def 24;
then (@CP)@ is-SubConcept-of (CP')@ by A8,CONLAT_1:def 19;
hence thesis by CONLAT_1:47;
end;
then "\/"(D,ConceptLattice(C)) = @CP by A1,LATTICE3:def 21;
hence thesis by Def1;
end;
theorem
Th10:for C being FormalContext
for CP being strict FormalConcept of C holds
"/\"({ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being 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 is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being Attribute of C st
a in the Intent of CP &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a})};
A1: @CP is_less_than D
proof
let q be Element of ConceptLattice(C);
assume q in D;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A2:
q = ConceptStr(#O,A#) &
ex a being Attribute of C st
a in the Intent of CP &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a});
consider a being Attribute of C such that A3:
a in the Intent of CP &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A2;
A4: {a} c= the Intent of CP by A3,ZFMISC_1:37;
A5: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP
by CONLAT_1:def 13;
the Extent of q@
= (AttributeDerivation(C)).{a} by A2,A3,CONLAT_1:def 24;
then the Extent of CP c= the Extent of q@ by A4,A5,CONLAT_1:4;
then A6: CP is-SubConcept-of q@ by CONLAT_1:def 19;
CP = @CP by Def1 .= (@CP)@ by CONLAT_1:def 24;
hence thesis by A6,CONLAT_1:47;
end;
for CP' being Element of ConceptLattice(C) st
CP' is_less_than D holds CP' [= @CP
proof
let CP' be Element of ConceptLattice(C);
assume A7: CP' is_less_than D;
A8:the Intent of CP c= the Intent of (CP')@
proof
let x be set; assume A9: x in the Intent of CP;
then reconsider x as Element of the Attributes of C;
set Ox = (AttributeDerivation(C)).{x};
set Ax = (ObjectDerivation(C)).((AttributeDerivation(C)).{x});
reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C
by CONLAT_1:22;
{x} c= Ax by CONLAT_1:6;
then A11: x in the Intent of Cx by ZFMISC_1:37;
A12: Cx in {ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being Attribute of C st
a in the Intent of CP &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) } by A9;
@Cx = Cx by Def1;
then CP' [= @Cx by A7,A12,LATTICE3:def 16;
then A13: (CP')@ is-SubConcept-of (@Cx)@ by CONLAT_1:47;
Cx = @Cx by Def1 .= (@Cx)@ by CONLAT_1:def 24;
then the Intent of Cx c= the Intent of (CP')@ by A13,CONLAT_1:31;
hence thesis by A11;
end;
CP = @CP by Def1 .= (@CP)@ by CONLAT_1:def 24;
then (CP')@ is-SubConcept-of (@CP)@ by A8,CONLAT_1:31;
hence thesis by CONLAT_1:47;
end;
then "/\"(D,ConceptLattice(C)) = @CP by A1,LATTICE3:34;
hence thesis by Def1;
end;
definition
let C be FormalContext;
func gamma(C) -> Function of the Objects of C,
the carrier of ConceptLattice(C) means :Def4:
for o being Element of the Objects of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
it.o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
existence
proof
defpred P[set, set] means ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st $2 = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{$1}) &
A = (ObjectDerivation(C)).{$1};
A1: for e being set st e in the Objects of C
ex u being set st u in the carrier of ConceptLattice(C) & P[e,u]
proof
let e be set; assume e in the Objects of C;
then reconsider se = {e} as Subset of the Objects of C by ZFMISC_1:37;
set O = (AttributeDerivation(C)).((ObjectDerivation(C)).se);
set A = (ObjectDerivation(C)).se;
take ConceptStr(#O,A#);
A2: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
ConceptStr(#O,A#) is FormalConcept of C by CONLAT_1:20;
hence thesis by A2,CONLAT_1:35;
end;
consider f being Function of the Objects of C,
the carrier of ConceptLattice(C) such that
A3: for e being set st e in
the Objects of C holds P[e,f.e] from FuncEx1(A1);
take f;
let o be Element of the Objects of C;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be Function of the Objects of C,the carrier of ConceptLattice(C);
assume A4: for o being Element of the Objects of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
F1.o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
assume A5: for o being Element of the Objects of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
F2.o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
A6: for o being set st o in the Objects of C holds F1.o = F2.o
proof
let o be set;
assume o in the Objects of C;
then reconsider o as Element of the Objects of C;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A7: F1.o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o} by A4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A8: F2.o = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A' = (ObjectDerivation(C)).{o} by A5;
thus thesis by A7,A8;
end;
A9: dom F1 = the Objects of C by FUNCT_2:def 1;
dom F2 = the Objects of C by FUNCT_2:def 1;
hence thesis by A6,A9,FUNCT_1:9;
end;
end;
definition
let C be FormalContext;
func delta(C) -> Function of the Attributes of C,
the carrier of ConceptLattice(C) means :Def5:
for a being Element of the Attributes of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
it.a = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a});
existence
proof
defpred P[set, set] means ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st $2 = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).{$1} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{$1});
A1: for e being set st e in the Attributes of C
ex u being set st u in the carrier of ConceptLattice(C) & P[e,u]
proof
let e be set; assume e in the Attributes of C;
then reconsider se = {e} as Subset of the Attributes of C by ZFMISC_1:37;
set O = (AttributeDerivation(C)).se;
set A = (ObjectDerivation(C)).((AttributeDerivation(C)).se);
take ConceptStr(#O,A#);
A2: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
ConceptStr(#O,A#) is FormalConcept of C by CONLAT_1:22;
hence thesis by A2,CONLAT_1:35;
end;
consider f being Function of the Attributes of C,
the carrier of ConceptLattice(C) such that
A3: for e being set st e in the Attributes of C holds P[e,f.e]
from FuncEx1(A1);
take f;
let o be Element of the Attributes of C;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be
Function of the Attributes of C,the carrier of ConceptLattice(C);
assume A4: for a being Element of the Attributes of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
F1.a = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a});
assume A5: for a being Element of the Attributes of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C st
F2.a = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a});
A6: for a being set st a in the Attributes of C holds F1.a = F2.a
proof
let a be set;
assume a in the Attributes of C;
then reconsider a as Element of the Attributes of C;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A7: F1.a = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A8: F2.a = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).{a} &
A' = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A5;
thus thesis by A7,A8;
end;
A9: dom F1 = the Attributes of C by FUNCT_2:def 1;
dom F2 = the Attributes of C by FUNCT_2:def 1;
hence thesis by A6,A9,FUNCT_1:9;
end;
end;
theorem
for C being FormalContext
for o being Object of C
for a being 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 23;
hence thesis by CONLAT_1:def 18;
end;
theorem
Th12:for C being 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 is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being Object of C st
o in the Extent of a@ &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o}},
ConceptLattice(C)) = a@ by Th9;
A2: {ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being 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 set; assume x in
{ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex o being Object of C st
o in the Extent of a@ &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o}};
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A3:
x = ConceptStr(#O,A#) &
ex o being Object of C st
o in the Extent of a@ &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
consider o being Object of C such that A4:
o in the Extent of a@ &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o} by A3;
A5: dom(gamma(C)) = the Objects of C by FUNCT_2:def 1;
consider y being Element of ConceptLattice(C)
such that A6: (gamma(C)).o = y;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that A7:
y = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A' = (ObjectDerivation(C)).{o} by A6,Def4;
thus thesis by A3,A4,A5,A6,A7,FUNCT_1:def 5;
end;
a = a@ by CONLAT_1:def 24;
hence thesis by A1,A2;
end;
set G = rng(delta(C));
let b be Element of ConceptLattice(C);
A8: "/\"({ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being Attribute of C st
a in the Intent of b@ &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a})},
ConceptLattice(C)) = b@ by Th10;
A9:{ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being 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 set; assume x in
{ConceptStr(#O,A#) where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ex a being Attribute of C st
a in the Intent of b@ &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a})};
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A10:
x = ConceptStr(#O,A#) &
ex a being Attribute of C st
a in the Intent of b@ &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a});
consider a being Attribute of C such that A11:
a in the Intent of b@ &
O = (AttributeDerivation(C)).{a} &
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A10;
A12: dom(delta(C)) = the Attributes of C by FUNCT_2:def 1;
consider y being Element of ConceptLattice(C)
such that A13: (delta(C)).a = y;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that A14:
y = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).{a} &
A' = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A13,Def5;
thus thesis by A10,A11,A12,A13,A14,FUNCT_1:def 5;
end;
b = b@ by CONLAT_1:def 24;
hence thesis by A8,A9;
end;
theorem
Th13:for C being FormalContext
for o being Object of C
for a being 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;
hereby assume o is-connected-with a;
then a in {a' where a' is Attribute of C : o is-connected-with a'};
then a in (ObjectDerivation(C)).({o}) by CONLAT_1:1;
then A1: {a} c= (ObjectDerivation(C)).({o}) by ZFMISC_1:37;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A2: (gamma(C)).o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o} by Def4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A3: (delta(C)).a = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).{a} &
A' = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5;
A4: the Extent of ((gamma(C)).o)@ = O by A2,CONLAT_1:def 24;
the Extent of ((delta(C)).a)@ = O' by A3,CONLAT_1:def 24;
then the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@
by A1,A2,A3,A4,CONLAT_1:4;
then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:def 19;
hence ((gamma(C)).o) [= ((delta(C)).a) by CONLAT_1:47;
end;
assume ((gamma(C)).o) [= ((delta(C)).a);
then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:47;
then A5: the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@
by CONLAT_1:def 19;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A6: (gamma(C)).o = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o} by Def4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A7: (delta(C)).a = ConceptStr(#O',A'#) &
O' = (AttributeDerivation(C)).{a} &
A' = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5;
the Extent of ((delta(C)).a)@ = O' by A7,CONLAT_1:def 24;
then A8: O c= O' by A5,A6,CONLAT_1:def 24;
set aa = {a};
set o' = {o};
set oo = (AttributeDerivation(C)).((ObjectDerivation(C)).{o});
aa c= (ObjectDerivation(C)).oo by A6,A7,A8,CONLAT_1:11;
then {a} c= (ObjectDerivation(C)).o' by CONLAT_1:7;
then a in (ObjectDerivation(C)).({o}) by ZFMISC_1:37;
then a in {a' where a' is Attribute of C : o is-connected-with a'}
by CONLAT_1:1;
then consider b being Attribute of C such that
A9: b = a & o is-connected-with b;
thus o is-connected-with a by A9;
end;
begin :: The Characterization
Lm1:for L1,L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 holds
(for a,b being 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 being Element of L1
holds f.a [= f.b implies a [= b;
let x,y be set; assume A2:
x in dom f & y in dom f & f.x = f.y;
then reconsider x as Element of L1;
reconsider y as Element of L1 by A2;
x [= y & y [= x by A1,A2;
hence thesis by LATTICES:26;
end;
Lm2:for L1,L2 being complete Lattice
for f being 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 being 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 being Element of L1
holds a [= b iff f.a [= f.b;
A3: for a,b being Element of L1 holds
f.(a "\/" b) = f.a "\/" f.b
proof
let a,b be Element of L1;
A4: {f.a,f.b} is_less_than f.(a "\/" b)
proof
a [= a "\/" b & b [= a "\/" b by LATTICES:22;
then f.a [= f.(a "\/" b) & f.b [= f.(a "\/" b) by A2;
then for q being Element of L2 st
q in {f.a,f.b} holds q [= f.(a "\/" b) by TARSKI:def 2;
hence thesis by LATTICE3:def 17;
end;
for r being Element of L2
st {f.a,f.b} is_less_than r holds f.(a "\/" b) [= r
proof
let r be Element of L2;
assume A5: {f.a,f.b} is_less_than r;
f.a in {f.a,f.b} & f.b in {f.a,f.b} by TARSKI:def 2;
then A6: f.a [= r & f.b [= r by A5,LATTICE3:def 17;
reconsider g = f" as Function of the carrier of L2, the carrier of L1
by A1,FUNCT_2:31;
A7: f.(g.r) = r by A1,FUNCT_1:57;
then a [= g.r & b [= g.r by A2,A6;
then for q being Element of L1
st q in {a,b} holds q [= g.r by TARSKI:def 2;
then A8: {a,b} is_less_than g.r by LATTICE3:def 17;
a "\/" b = "\/"{a,b} by LATTICE3:44;
then a "\/" b [= g.r by A8,LATTICE3:def 21;
hence thesis by A2,A7;
end;
then f.(a "\/" b) = "\/"({f.a,f.b},L2) by A4,LATTICE3:def 21;
hence thesis by LATTICE3:44;
end;
for a,b being Element of L1 holds
f.(a "/\" b) = f.a "/\" f.b
proof
let a,b be Element of L1;
A9: f.(a "/\" b) is_less_than {f.a,f.b}
proof
a "/\" b [= a & a "/\" b [= b by LATTICES:23;
then f.(a "/\" b) [= f.a & f.(a "/\" b) [= f.b by A2;
then for q being Element of L2 st
q in {f.a,f.b} holds f.(a "/\" b) [= q by TARSKI:def 2;
hence thesis by LATTICE3:def 16;
end;
for r being Element of L2
st r is_less_than {f.a,f.b} holds r [= f.(a "/\" b)
proof
let r be Element of L2;
assume A10: r is_less_than {f.a,f.b};
f.a in {f.a,f.b} & f.b in {f.a,f.b} by TARSKI:def 2;
then A11: r [= f.a & r [= f.b by A10,LATTICE3:def 16;
reconsider g = f" as Function of the carrier of L2, the carrier of L1
by A1,FUNCT_2:31;
A12: f.(g.r) = r by A1,FUNCT_1:57;
then g.r [= a & g.r [= b by A2,A11;
then for q being Element of L1
st q in {a,b} holds g.r [= q by TARSKI:def 2;
then A13: g.r is_less_than {a,b} by LATTICE3:def 16;
a "/\" b = "/\"{a,b} by LATTICE3:44;
then g.r [= a "/\" b by A13,LATTICE3:34;
hence thesis by A2,A12;
end;
then f.(a "/\" b) = "/\"({f.a,f.b},L2) by A9,LATTICE3:34;
hence thesis by LATTICE3:44;
end;
hence f is Homomorphism of L1,L2 by A3,LATTICE4:def 1;
end;
Lm3:for C being FormalContext
for CS being ConceptStr over C st
(ObjectDerivation(C)).(the Extent of CS) = the Intent of CS &
(AttributeDerivation(C)).(the Intent of CS) = the Extent 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 &
(AttributeDerivation(C)).(the Intent of CS) = the Extent of CS;
per cases;
suppose the Extent of CS is empty;
then the Intent of CS = the Attributes of C by A1,CONLAT_1:18;
hence thesis by CONLAT_1:def 11;
suppose the Extent of CS is non empty;
hence thesis by CONLAT_1:def 11;
end;
theorem
Th14:for L being complete Lattice
for C being FormalContext holds
ConceptLattice(C),L are_isomorphic
iff ex g being Function of the Objects of C, the carrier of L,
d being Function of the Attributes of C, the carrier of L
st rng(g) is supremum-dense &
rng(d) is infimum-dense &
for o being Object of C,
a being 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 being Homomorphism of ConceptLattice(C),L such that
A1: f is isomorphism by LATTICE4:def 5;
A2: f is monomorphism epimorphism by A1,LATTICE4:def 4;
take g = f * gamma(C), d = f * delta(C);
thus rng(g) is supremum-dense
proof
let a be Element of L;
consider b being Element of ConceptLattice(C)
such that A3: a = f.b by A2,LATTICE4:9;
rng(gamma(C)) is supremum-dense by Th12;
then consider D' being Subset of rng(gamma(C)) such that
A4: b = "\/"(D',ConceptLattice(C)) by LATTICE6:def 13;
A5: D' is_less_than b & for r being Element of ConceptLattice(C)
st D' is_less_than r holds b [= r by A4,LATTICE3:def 21;
set D = {f.x where x is Element of ConceptLattice(C) : x in D'};
A6: D c= rng(g)
proof
let x be set; assume x in D;
then consider x' being Element of ConceptLattice(C) such that
A7: x = f.x' & x' in D';
consider y being set such that
A8: y in dom(gamma(C)) & (gamma(C)).y = x' by A7,FUNCT_1:def 5;
A9: x = (f * (gamma(C))).y by A7,A8,FUNCT_1:23;
dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
then y in dom(f * (gamma(C))) by A8,FUNCT_1:21;
hence thesis by A9,FUNCT_1:def 5;
end;
A10: D is_less_than a
proof
let q be Element of L; assume q in D;
then consider q' being Element of ConceptLattice(C) such that A11:
q = f.q' & q' in D';
q' [= b by A5,A11,LATTICE3:def 17;
hence thesis by A2,A3,A11,LATTICE4:8;
end;
for r being Element of L st D is_less_than r holds a [= r
proof
let r be Element of L;
assume A12: D is_less_than r;
consider r' being Element of ConceptLattice(C)
such that A13: r = f.r' by A2,LATTICE4:9;
reconsider r' as Element of ConceptLattice(C);
for q being Element of ConceptLattice(C)
st q in D' holds q [= r'
proof
let q be Element of ConceptLattice(C);
assume q in D';
then f.q in {f.x where x is Element of ConceptLattice(C) : x in D'};
then f.q [= f.r' by A12,A13,LATTICE3:def 17;
hence thesis by A2,LATTICE4:8;
end;
then D' is_less_than r' by LATTICE3:def 17;
then b [= r' by A4,LATTICE3:def 21;
hence thesis by A2,A3,A13,LATTICE4:8;
end;
then a = "\/"(D,L) by A10,LATTICE3:def 21;
hence thesis by A6;
end;
thus rng(d) is infimum-dense
proof
let a be Element of L;
consider b being Element of ConceptLattice(C)
such that A14: a = f.b by A2,LATTICE4:9;
rng(delta(C)) is infimum-dense by Th12;
then consider D' being Subset of rng(delta(C))
such that A15: b = "/\"(D',ConceptLattice(C)) by LATTICE6:def 14;
A16: b is_less_than D' & for r being Element of ConceptLattice(C)
st r is_less_than D' holds r [= b by A15,LATTICE3:34;
set D = {f.x where x is Element of ConceptLattice(C) : x in D'};
A17: D c= rng(d)
proof
let x be set; assume x in D;
then consider x' being Element of ConceptLattice(C) such that A18:
x = f.x' & x' in D';
consider y being set such that
A19: y in dom(delta(C)) & (delta(C)).y = x' by A18,FUNCT_1:def 5;
A20: x = (f * (delta(C))).y by A18,A19,FUNCT_1:23;
dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
then y in dom(f * (delta(C))) by A19,FUNCT_1:21;
hence thesis by A20,FUNCT_1:def 5;
end;
A21: a is_less_than D
proof
let q be Element of L; assume q in D;
then consider q' being Element of ConceptLattice(C) such that A22:
q = f.q' & q' in D';
b [= q' by A16,A22,LATTICE3:def 16;
hence thesis by A2,A14,A22,LATTICE4:8;
end;
for r being Element of L st r is_less_than D holds r [= a
proof
let r be Element of L;
assume A23: r is_less_than D;
consider r' being Element of ConceptLattice(C)
such that A24: r = f.r' by A2,LATTICE4:9;
reconsider r' as Element of ConceptLattice(C);
r' is_less_than D'
proof
let q be Element of ConceptLattice(C);
assume q in D';
then f.q in {f.x where x is Element of ConceptLattice(C) : x in D'};
then f.r' [= f.q by A23,A24,LATTICE3:def 16;
hence thesis by A2,LATTICE4:8;
end;
then r' [= b by A15,LATTICE3:34;
hence thesis by A2,A14,A24,LATTICE4:8;
end;
then a = "/\"(D,L) by A21,LATTICE3:34;
hence thesis by A17;
end;
let o be Object of C, a be Attribute of C;
A25: o is-connected-with a iff (gamma(C)).o [= (delta(C)).a by Th13;
hereby assume A26: o is-connected-with a;
dom(gamma(C)) = the Objects of C &
dom(delta(C)) = the Attributes of C by FUNCT_2:def 1;
then f.((gamma(C)).o) = (f * (gamma(C))).o &
f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:23;
hence g.o [= d.a by A2,A25,A26,LATTICE4:8;
end;
assume A27: g.o [= d.a;
dom(gamma(C)) = the Objects of C &
dom(delta(C)) = the Attributes of C by FUNCT_2:def 1;
then f.((gamma(C)).o) = (f * (gamma(C))).o &
f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:23;
then (gamma(C)).o [= (delta(C)).a by A2,A27,LATTICE4:8;
hence o is-connected-with a by Th13;
end;
given g being Function of the Objects of C, the carrier of L,
d being Function of the Attributes of C, the carrier of L such that
A28: rng(g) is supremum-dense & rng(d) is infimum-dense &
for o being Object of C,
a being Attribute of C holds
o is-connected-with a iff g.o [= d.a;
set f = {[ConceptStr(#O,A#),x] where O is Subset of the Objects of C,
A is Subset of the Attributes of C,
x is Element of L :
ConceptStr(#O,A#) is FormalConcept of C &
x = "\/"({g.o where o is Object of C : o in O},L) };
A29: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
f c= [:the carrier of ConceptLattice(C), the carrier of L:]
proof
let y be set; assume y in f;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C,
x being Element of L such that A30:
y = [ConceptStr(#O,A#),x] &
ConceptStr(#O,A#) is FormalConcept of C &
x = "\/"({g.o where o is Object of C : o in O},L);
ConceptStr(#O,A#) in the carrier of ConceptLattice(C)
by A29,A30,CONLAT_1:35;
hence thesis by A30,ZFMISC_1:def 2;
end;
then reconsider f as Relation of the carrier of ConceptLattice(C),
the carrier of L by RELSET_1:def 1;
the carrier of ConceptLattice(C) c= dom f
proof
let y be set; assume y in the carrier of ConceptLattice(C);
then A31:y is strict FormalConcept of C by A29,CONLAT_1:35;
then consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C
such that A32: y = ConceptStr(#O',A'#);
reconsider z = "\/"({g.o where o is Object of C : o in O'},L)
as Element of L;
[y,z] in f by A31,A32;
hence thesis by RELAT_1:def 4;
end;
then A33: the carrier of ConceptLattice(C) = dom f by XBOOLE_0:def 10;
for x,y1,y2 being set st [x,y1] in f & [x,y2] in f holds y1 = y2
proof
let x,y1,y2 be set; assume A34: [x,y1] in f & [x,y2] in f;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C,
z being Element of L such that
A35: [x,y1] = [ConceptStr(#O,A#),z] &
ConceptStr(#O,A#) is FormalConcept of C &
z = "\/"({g.o where o is Object of C : o in O},L);
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C,
z' being Element of L such that
A36: [x,y2] = [ConceptStr(#O',A'#),z'] &
ConceptStr(#O',A'#) is FormalConcept of C &
z' = "\/"({g.o where o is Object of C : o in O'},L) by A34;
ConceptStr(#O,A#) = [x,y1]`1 by A35,MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2]`1 by MCART_1:def 1
.= ConceptStr(#O',A'#) by A36,MCART_1:def 1;
hence y1 = [x,y2]`2 by A35,A36,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
then reconsider f as Function of the carrier of ConceptLattice(C),
the carrier of L by A33,FUNCT_1:def 1,FUNCT_2:def 1;
A37: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
A38: for a,b being Element of ConceptLattice(C)
holds a [= b implies f.a [= f.b
proof
let a,b be Element of ConceptLattice(C);
assume a [= b;
then a@ is-SubConcept-of b@ by CONLAT_1:47;
then A39: the Extent of a@ c= the Extent of b@ by CONLAT_1:def 19;
A40: {g.o where o is Object of C : o in the Extent of a@} c=
{g.o where o is Object of C : o in the Extent of b@}
proof
let x be set; assume
x in {g.o where o is Object of C : o in the Extent of a@};
then consider o being Object of C such that A41:
x = g.o & o in the Extent of a@;
thus thesis by A39,A41;
end;
reconsider xa = "\/"({g.o where o is Object of C :
o in the Extent of a@},L),
xb = "\/"({g.o where o is Object of C :
o in the Extent of b@},L) as Element of L;
[a@,xa] in f & [b@,xb] in f;
then A42: f.(a@) = xa & f.(b@) = xb by FUNCT_1:8;
a@ = a & b@ = b by CONLAT_1:def 24;
hence thesis by A40,A42,LATTICE3:46;
end;
set fi = {[x,ConceptStr(#O,A#)] where x is Element of L,
O is Subset of the Objects of C,
A is Subset of the Attributes of C :
O = {o where o is Object of C : g.o [= x} &
A = {a where a is Attribute of C : x [= d.a} };
fi c= [:the carrier of L, the carrier of ConceptLattice(C):]
proof
let y be set; assume y in fi;
then consider x being Element of L,
O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A43:
y = [x,ConceptStr(#O,A#)] &
O = {o where o is Object of C : g.o [= x} &
A = {a where a is Attribute of C : x [= d.a};
A44: (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 set; assume u in
(ObjectDerivation(C)).(the Extent of ConceptStr(#O,A#));
then u in { o where o is Attribute of C :
for a being Object of C st a in the Extent of ConceptStr(#O,A#)
holds a is-connected-with o } by CONLAT_1:def 6;
then consider u' being Attribute of C such that A45: u' = u &
for a being Object of C st a in the Extent of ConceptStr(#O,A#)
holds a is-connected-with u';
A46: for v being Object of C st v in {a where a is Object of C:
g.a [= x} holds g.v [= d.u'
proof
let v be Object of C; assume
v in {a where a is Object of C : g.a [= x};
then v is-connected-with u' by A43,A45;
hence thesis by A28;
end;
A47: {g.a where a is Object of C: g.a [= x} is_less_than d.u'
proof
let q be Element of L; assume
q in {g.a where a is Object of C: g.a [= x};
then consider b being Object of C such that A48:
q = g.b & g.b [= x;
b in {a where a is Object of C: g.a [= x} by A48;
hence thesis by A46,A48;
end;
"\/"({g.a' where a' is Object of C : g.a' [= x},L) = x
proof
consider D being Subset of rng(g) such that
A49: "\/"(D,L) = x by A28,LATTICE6:def 13;
A50: D is_less_than x by A49,LATTICE3:def 21;
D c= {g.a' where a' is Object of C : g.a' [= x}
proof
let u be set; assume A51: u in D;
then consider v being set such that A52:
v in dom g & u = g.v by FUNCT_1:def 5;
reconsider v as Object of C by A52;
g.v [= x by A50,A51,A52,LATTICE3:def 17;
hence thesis by A52;
end;
then A53: x [= "\/"({g.a' where a' is Object of C : g.a' [= x},L)
by A49,LATTICE3:46;
{g.a' where a' is Object of C : g.a' [= x} is_less_than x
proof
let u be Element of L; assume u in
{g.a' where a' is Object of C : g.a' [= x};
then consider v being Object of C such that A54:
u = g.v & g.v [= x;
thus thesis by A54;
end;
then "\/"({g.a' where a' is Object of C : g.a' [= x},L) [= x
by LATTICE3:def 21;
hence thesis by A53,LATTICES:26;
end;
then x [= d.u' by A47,LATTICE3:def 21;
hence thesis by A43,A45;
end;
let u be set;
assume u in the Intent of ConceptStr(#O,A#);
then consider u' being Attribute of C such that A55:
u' = u & x [= d.u' by A43;
A56:for v being Object of C st v in {a where a is Object of C:
g.a [= x} holds g.v [= d.u'
proof
let v be Object of C; assume
v in {a where a is Object of C : g.a [= x};
then consider v' being Object of C such that A57:
v' = v & g.v' [= x;
thus thesis by A55,A57,LATTICES:25;
end;
for v being Object of C st v in {a where a is Object of C :
g.a [= x} holds v is-connected-with u'
proof
let v be Object of C; assume
v in {a where a is Object of C : g.a [= x};
then g.v [= d.u' by A56;
hence thesis by A28;
end;
then u' in {o where o is Attribute of C : for a being Object of C
st a in the Extent of ConceptStr(#O,A#)
holds a is-connected-with o } by A43;
hence thesis by A55,CONLAT_1:def 6;
end;
(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 set; assume u in
(AttributeDerivation(C)).(the Intent of ConceptStr(#O,A#));
then u in { o where o is Object of C :
for a being Attribute of C st a in the Intent of ConceptStr(#O,A#)
holds o is-connected-with a } by CONLAT_1:def 7;
then consider u' being Object of C such that A58: u' = u &
for a being Attribute of C st a in the Intent of ConceptStr(#O,A#)
holds u' is-connected-with a;
A59: for v being Attribute of C st v in {a where a is Attribute of C:
x [= d.a} holds g.u' [= d.v
proof
let v be Attribute of C; assume
v in {a where a is Attribute of C : x [= d.a};
then u' is-connected-with v by A43,A58;
hence thesis by A28;
end;
A60: g.u' is_less_than {d.a where a is Attribute of C: x [= d.a}
proof
let q be Element of L; assume
q in {d.a where a is Attribute of C: x [= d.a};
then consider b being Attribute of C such that A61:
q = d.b & x [= d.b;
b in {a where a is Attribute of C: x [= d.a} by A61;
hence thesis by A59,A61;
end;
"/\"({d.a' where a' is Attribute of C : x [= d.a'},L) = x
proof
consider D being Subset of rng(d) such that
A62: "/\"(D,L) = x by A28,LATTICE6:def 14;
A63: x is_less_than D by A62,LATTICE3:34;
D c= {d.a' where a' is Attribute of C : x [= d.a'}
proof
let u be set; assume A64: u in D;
then consider v being set such that A65:
v in dom d & u = d.v by FUNCT_1:def 5;
reconsider v as Attribute of C by A65;
x [= d.v by A63,A64,A65,LATTICE3:def 16;
hence thesis by A65;
end;
then A66: "/\"({d.a' where a' is Attribute of C : x [= d.a'},L)
[= x by A62,LATTICE3:46;
x is_less_than {d.a' where a' is Attribute of C : x [= d.a'}
proof
let u be Element of L; assume u in
{d.a' where a' is Attribute of C : x [= d.a'};
then consider v being Attribute of C such that A67:
u = d.v & x [= d.v;
thus thesis by A67;
end;
then x [= "/\"({d.a' where a' is Attribute of C : x [= d.a'},L)
by LATTICE3:40;
hence thesis by A66,LATTICES:26;
end;
then g.u' [= x by A60,LATTICE3:34;
hence thesis by A43,A58;
end;
let u be set;
assume u in the Extent of ConceptStr(#O,A#);
then consider u' being Object of C such that A68:
u' = u & g.u' [= x by A43;
A69:for v being Attribute of C st v in
{a where a is Attribute of C:
x [= d.a} holds g.u' [= d.v
proof
let v be Attribute of C; assume
v in {a where a is Attribute of C : x [= d.a};
then consider v' being Attribute of C such that A70:
v' = v & x [= d.v';
thus thesis by A68,A70,LATTICES:25;
end;
for v being Attribute of C st v in {a where a is Attribute of C :
x [= d.a} holds u' is-connected-with v
proof
let v be Attribute of C; assume
v in {a where a is Attribute of C : x [= d.a};
then g.u' [= d.v by A69;
hence thesis by A28;
end;
then u' in {o where o is Object of C : for a being Attribute of C
st a in the Intent of ConceptStr(#O,A#)
holds o is-connected-with a } by A43;
hence thesis by A68,CONLAT_1:def 7;
end;
then ConceptStr(#O,A#) is FormalConcept of C by A44,Lm3,CONLAT_1:def 13;
then ConceptStr(#O,A#) in the carrier of ConceptLattice(C)
by A29,CONLAT_1:35;
hence thesis by A43,ZFMISC_1:def 2;
end;
then reconsider fi as Relation of the carrier of L,
the carrier of ConceptLattice(C) by RELSET_1:def 1;
the carrier of L c= dom fi
proof
let y be set; assume y in the carrier of L;
then reconsider y as Element of L;
set O = {o where o is Object of C : g.o [= y};
set A = {a where a is Attribute of C : y [= d.a};
O c= the Objects of C
proof
let u be set; assume u in O;
then consider u' being Object of C such that A71:
u' = u & g.u' [= y;
thus thesis by A71;
end;
then reconsider O as Subset of the Objects of C;
A c= the Attributes of C
proof
let u be set; assume u in A;
then consider u' being Attribute of C such that A72:
u' = u & y [= d.u';
thus thesis by A72;
end;
then reconsider A as Subset of the Attributes of C;
[y,ConceptStr(#O,A#)] in fi;
hence thesis by RELAT_1:def 4;
end;
then A73: the carrier of L = dom fi by XBOOLE_0:def 10;
for x,y1,y2 being set st [x,y1] in fi & [x,y2] in fi holds y1 = y2
proof
let x,y1,y2 be set; assume A74: [x,y1] in fi & [x,y2] in fi;
then consider z being Element of L,
O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A75: [x,y1] = [z,ConceptStr(#O,A#)] &
O = {o where o is Object of C : g.o [= z} &
A = {a where a is Attribute of C : z [= d.a};
consider z' being Element of L,
O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A76: [x,y2] = [z',ConceptStr(#O',A'#)] &
O' = {o where o is Object of C : g.o [= z'} &
A' = {a where a is Attribute of C : z' [= d.a} by A74;
z = [x,y1]`1 by A75,MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2]`1 by MCART_1:def 1
.= z' by A76,MCART_1:def 1;
hence y1 = [x,y2]`2 by A75,A76,MCART_1:def 2
.= y2 by MCART_1:def 2;
end;
then reconsider fi as Function of the carrier of L,
the carrier of ConceptLattice(C) by A73,FUNCT_1:def 1,FUNCT_2:def 1;
A77: for a,b being Element of L
holds a [= b implies fi.a [= fi.b
proof
let a,b be Element of L;
assume A78: a [= b;
A79: {o where o is Object of C : g.o [= a} c=
{o where o is Object of C : g.o [= b}
proof
let x be set; assume x in {o where o is Object of C : g.o [= a};
then consider x' being Object of C such that
A80: x' = x & g.x' [= a;
g.x' [= b by A78,A80,LATTICES:25;
hence thesis by A80;
end;
A81: dom fi = the carrier of L by FUNCT_2:def 1;
then consider ya being set such that A82: [a,ya] in fi by RELAT_1:def 4;
consider xa being Element of L,
Oa being Subset of the Objects of C,
Aa being Subset of the Attributes of C such that A83:
[a,ya] = [xa,ConceptStr(#Oa,Aa#)] &
Oa = {o where o is Object of C : g.o [= xa} &
Aa = {a' where a' is Attribute of C : xa [= d.a'} by A82;
consider yb being set such that A84: [b,yb] in fi by A81,RELAT_1:def 4;
consider xb being Element of L,
Ob being Subset of the Objects of C,
Ab being Subset of the Attributes of C such that A85:
[b,yb] = [xb,ConceptStr(#Ob,Ab#)] &
Ob = {o where o is Object of C : g.o [= xb} &
Ab = {a' where a' is Attribute of C : xb [= d.a'} by A84;
A86: a = [xa,ConceptStr(#Oa,Aa#)]`1 by A83,MCART_1:def 1
.= xa by MCART_1:def 1;
A87: b = [xb,ConceptStr(#Ob,Ab#)]`1 by A85,MCART_1:def 1
.= xb by MCART_1:def 1;
A88: fi.a = ConceptStr(#Oa,Aa#) by A82,A83,A86,FUNCT_1:8;
A89: fi.b = ConceptStr(#Ob,Ab#) by A84,A85,A87,FUNCT_1:8;
set ca = fi.a, cb = fi.b;
the Extent of ca@ = Oa &
the Extent of cb@ = Ob by A88,A89,CONLAT_1:def 24;
then ca@ is-SubConcept-of cb@ by A79,A83,A85,A86,A87,CONLAT_1:def 19;
hence thesis by CONLAT_1:47;
end;
A90: for a being Element of L holds f.(fi.a) = a
proof
let a be Element of L;
reconsider a as Element of L;
set O = {o where o is Object of C : g.o [= a};
O c= the Objects of C
proof
let u be set; assume u in O;
then consider u' being Object of C such that
A91: u' = u & g.u' [= a;
thus thesis by A91;
end;
then reconsider O as Subset of the Objects of C;
set A = {a' where a' is Attribute of C : a [= d.a'};
A c= the Attributes of C
proof
let u be set; assume u in A;
then consider u' being Attribute of C such that
A92: u' = u & a [= d.u';
thus thesis by A92;
end;
then reconsider A as Subset of the Attributes of C;
A93: [a,ConceptStr(#O,A#)] in fi;
set b = "\/"({g.o where o is Object of C :
o in the Extent of ConceptStr(#O,A#)},L);
ConceptStr(#O,A#) in rng(fi) by A93,RELAT_1:def 5;
then ConceptStr(#O,A#) is FormalConcept of C by A37,CONLAT_1:35;
then [ConceptStr(#O,A#),b] in f;
then A94: f.ConceptStr(#O,A#) = b by FUNCT_1:8;
"\/"({g.o where o is Object of C :
o in {o' where o' is Object of C : g.o' [= a}},L) = a
proof
consider D being Subset of rng(g) such that
A95: "\/"(D,L) = a by A28,LATTICE6:def 13;
A96: D is_less_than a by A95,LATTICE3:def 21;
D c= {g.o where o is Object of C :
o in {o' where o' is Object of C : g.o' [= a}}
proof
let u be set; assume A97: u in D;
then consider v being set such that A98:
v in dom g & u = g.v by FUNCT_1:def 5;
reconsider v as Object of C by A98;
g.v [= a by A96,A97,A98,LATTICE3:def 17;
then v in {o' where o' is Object of C : g.o' [= a};
hence thesis by A98;
end;
then A99: a [= "\/"({g.o where o is Object of C : o in
{o' where o' is Object of C : g.o' [= a}},L)
by A95,LATTICE3:46;
{g.o where o is Object of C : o in
{o' where o' is Object of C : g.o' [= a}}
is_less_than a
proof
let u be Element of L; assume u in
{g.o where o is Object of C : o in
{o' where o' is Object of C : g.o' [= a}};
then consider v being Object of C such that A100:
u = g.v & v in {o' where o' is Object of C : g.o' [= a};
consider ov being Object of C such that A101:
ov = v & g.ov [= a by A100;
thus thesis by A100,A101;
end;
then "\/"({g.o where o is Object of C : o in
{o' where o' is Object of C : g.o' [= a}},L) [= a
by LATTICE3:def 21;
hence thesis by A99,LATTICES:26;
end;
hence thesis by A93,A94,FUNCT_1:8;
end;
A102: for x being Element of ConceptLattice(C) holds
f.x = "/\"({d.a where a is Attribute of C : a in the Intent of x@},L)
proof
let x be Element of ConceptLattice(C);
set y = "\/"({g.o where o is Object of C : o in the Extent of x@},L);
A103: [x@, y] in f;
A104: f.x = f.x@ by CONLAT_1:def 24 .= y by A103,FUNCT_1:8;
A105:for o' being Object of C st o' in the Extent of x@
for a' being Attribute of C st a' in the Intent of x@
holds g.o' [= d.a'
proof
let o' be Object of C; assume A106: o' in the Extent of x@;
let a' be Attribute of C; assume a' in the Intent of x@;
then a' in (ObjectDerivation(C)).(the Extent of x@) by CONLAT_1:def
13;
then a' in {a where a is Attribute of C :
for o being Object of C st o in the Extent of x@ holds
o is-connected-with a } by CONLAT_1:def 6;
then consider aa being Attribute of C such that A107:
aa = a' & for o being Object of C st o in the Extent of x@ holds
o is-connected-with aa;
o' is-connected-with a' by A106,A107;
hence thesis by A28;
end;
A108: for o being set holds
o in {d.a' where a' is Attribute of C : y [= d.a'} implies
o in {d.a where a is Attribute of C : a in the Intent of x@}
proof
let o be set; assume
o in {d.a' where a' is Attribute of C : y [= d.a'};
then consider u being Attribute of C such that A109:
o = d.u & y [= d.u;
A110:for o being 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.o' where o' is Object of C : o' in the Extent of x
@};
then g.o [= y by LATTICE3:38;
hence thesis by A109,LATTICES:25;
end;
for o being 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 A110;
hence thesis by A28;
end;
then u in {a' where a' is Attribute of C :
for o' being Object of C st o' in the Extent of x@
holds o' is-connected-with a'};
then u in (ObjectDerivation(C)).(the Extent of x@)
by CONLAT_1:def 6;
then u in the Intent of x@ by CONLAT_1:def 13;
hence thesis by A109;
end;
A111: for o being set holds
o in {d.a where a is Attribute of C : a in the Intent of x@} implies
o in {d.a' where a' is Attribute of C : y [= d.a'}
proof
let o be set; assume o in
{d.a where a is Attribute of C : a in the Intent of x@};
then consider b being Attribute of C such that A112:
o = d.b & b in the Intent of x@;
{g.o' where o' is Object of C : o' in the Extent of x@}
is_less_than d.b
proof
let q be Element of L; assume q in
{g.o' where o' is Object of C : o' in the Extent of x@};
then consider u being Object of C such that A113:
q = g.u & u in the Extent of x@;
thus thesis by A105,A112,A113;
end;
then y [= d.b by LATTICE3:def 21;
hence thesis by A112;
end;
"/\"({d.a' where a' is Attribute of C : y [= d.a'},L) = y
proof
consider D being Subset of rng(d) such that
A114: "/\"(D,L) = y by A28,LATTICE6:def 14;
A115: y is_less_than D by A114,LATTICE3:34;
D c= {d.a' where a' is Attribute of C : y [= d.a'}
proof
let u be set; assume A116: u in D;
then consider v being set such that A117:
v in dom d & u = d.v by FUNCT_1:def 5;
reconsider v as Attribute of C by A117;
y [= d.v by A115,A116,A117,LATTICE3:def 16;
hence thesis by A117;
end;
then A118: "/\"({d.a' where a' is Attribute of C : y [= d.a'},L)
[= y by A114,LATTICE3:46;
y is_less_than {d.a' where a' is Attribute of C : y [= d.a'}
proof
let u be Element of L; assume u in
{d.a' where a' is Attribute of C : y [= d.a'};
then consider v being Attribute of C such that A119:
u = d.v & y [= d.v;
thus thesis by A119;
end;
then y [= "/\"({d.a' where a' is Attribute of C : y [= d.a'},L)
by LATTICE3:40;
hence thesis by A118,LATTICES:26;
end;
hence thesis by A104,A108,A111,TARSKI:2;
end;
A120: for a being Element of ConceptLattice(C)
holds fi.(f.a) = a
proof
let a be Element of ConceptLattice(C);
A121:fi.("/\"({d.u where u is Attribute of C : u in
the Intent of a@},L)) =
fi.(f.a) by A102;
set x = "/\"({d.u where u is Attribute of C : u in the Intent of a@},L);
set O = {o where o is Object of C : g.o [= x};
O c= the Objects of C
proof
let u be set; assume u in O;
then consider u' being Object of C such that
A122: u' = u & g.u' [= x;
thus thesis by A122;
end;
then reconsider O as Subset of the Objects of C;
set A = {a' where a' is Attribute of C : x [= d.a'};
A c= the Attributes of C
proof
let u be set; assume u in A;
then consider u' being Attribute of C such that
A123: u' = u & x [= d.u';
thus thesis by A123;
end;
then reconsider A as Subset of the Attributes of C;
[x,ConceptStr(#O,A#)] in fi;
then A124: fi.x = ConceptStr(#O,A#) by FUNCT_1:8;
then A125: ConceptStr(#O,A#) is FormalConcept of C by A37,CONLAT_1:35;
A126: O = {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' }
proof
thus O c= {o where o is Object of
C : for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' }
proof
let u be set; assume u in O;
then consider o' being Object of C such that
A127: u = o' & g.o' [= x;
for a' being Attribute of C st a' in the Intent of a@
holds g.o' [= d.a'
proof
let a' be Attribute of C; assume a' in the Intent of a@;
then d.a' in {d.y where y is Attribute of C : y in the Intent of a
@};
then x [= d.a' by LATTICE3:38;
hence thesis by A127,LATTICES:25;
end;
hence thesis by A127;
end;
let u be set; assume u in {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' };
then consider o' being Object of C such that
A128: o' = u & for a' being Attribute of C st a' in the Intent of a@
holds g.o' [= d.a';
g.o' is_less_than {d.y where y is Attribute of C :
y in the Intent of a@}
proof
let q be Element of L; assume q in
{d.y where y is Attribute of C : y in the Intent of a@};
then consider qa being Attribute of C such that A129:
q = d.qa & qa in the Intent of a@;
thus thesis by A128,A129;
end;
then g.o' [= x by LATTICE3:34;
hence thesis by A128;
end;
{o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' } =
{o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds o is-connected-with a' }
proof
thus {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' } c= {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds o is-connected-with a' }
proof
let u be set; assume u in {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds g.o [= d.a' };
then consider u' being Object of C such that
A130: u = u' & for a' being Attribute of C
st a' in the Intent of a@ holds g.u' [= d.a';
for a' being Attribute of C
st a' in the Intent of a@ holds u' is-connected-with a'
proof
let a' be Attribute of C; assume a' in the Intent of a@;
then g.u' [= d.a' by A130;
hence thesis by A28;
end;
hence thesis by A130;
end;
let u be set; assume u in {o where o is Object of C :
for a' being Attribute of C st a' in the Intent of a@
holds o is-connected-with a' }; then consider u' being
Object of C such that A131: u = u' & for a' being Attribute of C
st a' in the Intent of a@ holds u' is-connected-with a';
for a' being Attribute of C
st a' in the Intent of a@ holds g.u' [= d.a'
proof
let a' be Attribute of C; assume a' in the Intent of a@;
then u' is-connected-with a' by A131;
hence thesis by A28;
end;
hence thesis by A131;
end;
then A132: O = (AttributeDerivation(C)).(the Intent of a@)
by A126,CONLAT_1:def 7
.= the Extent of a@ by CONLAT_1:def 13;
then A = (ObjectDerivation(C)).(the Extent of a@) by A125,CONLAT_1:def
13
.= the Intent of a@ by CONLAT_1:def 13;
hence thesis by A121,A124,A132,CONLAT_1:def 24;
end;
A133: for a,b being Element of ConceptLattice(C)
holds f.a [= f.b implies a [= b
proof
let a,b be Element of ConceptLattice(C);
assume A134: f.a [= f.b;
fi.(f.a) = a & fi.(f.b) = b by A120;
hence thesis by A77,A134;
end;
then A135: f is one-to-one by Lm1;
the carrier of L c= rng f
proof
let u be set; assume A136: u in the carrier of L;
then u in dom fi by FUNCT_2:def 1;
then consider v being set such that A137: [u,v] in fi by RELAT_1:def 4;
rng fi c= the carrier of ConceptLattice(C) &
v in rng fi by A137,RELAT_1:def 5;
then reconsider v as Element of ConceptLattice(C);
reconsider u as Element of L by A136;
A138: f.v = f.(fi.u) by A137,FUNCT_1:8 .= u by A90;
dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
hence thesis by A138,FUNCT_1:def 5;
end;
then A139: rng f = the carrier of L by XBOOLE_0:def 10;
then reconsider f as Homomorphism of ConceptLattice(C),L
by A38,A133,A135,Lm2;
A140: f is epimorphism by A139,LATTICE4:def 3;
f is monomorphism by A135,LATTICE4:def 2;
then f is isomorphism by A140,LATTICE4:def 4;
hence ConceptLattice(C),L are_isomorphic by LATTICE4:def 5;
end;
definition
let L be Lattice;
func Context(L) -> strict non quasi-empty ContextStr equals :Def6:
ContextStr(#the carrier of L, the carrier of L, LattRel L#);
coherence by CONLAT_1:def 2;
end;
theorem
Th15:for L being complete Lattice holds
ConceptLattice(Context(L)),L are_isomorphic
proof
let L be complete Lattice;
A1: Context(L) = ContextStr(#the carrier of L, the carrier of L, LattRel L#)
by Def6;
then reconsider g = id the carrier of L
as Function of the Objects of Context(L), the carrier of L;
reconsider d = id the carrier of L
as Function of the Attributes of Context(L), the carrier of L by A1;
A2: rng(g) is supremum-dense
proof
let a be Element of L;
A3: "\/"({a},L) = a by LATTICE3:43;
rng(g) = the carrier of L by RELAT_1:71;
hence thesis by A3;
end;
for a being Element of L holds
ex D' being Subset of rng(d) st a = "/\"(D',L)
proof
let a be Element of L;
A4: "/\"({a},L) = a by LATTICE3:43;
rng(d) = the carrier of L by RELAT_1:71;
hence thesis by A4;
end;
then A5: rng(d) is infimum-dense by LATTICE6:def 14;
for o being Object of Context(L),
a being 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 o' = o, a' = a as Element of L by A1;
A6: o is-connected-with a iff [o,a] in the Information of Context(L)
by CONLAT_1:def 5;
g.o = o' & d.a = a' by FUNCT_1:34;
hence thesis by A1,A6,FILTER_1:32;
end;
hence thesis by A2,A5,Th14;
end;
theorem
for L being Lattice holds
L is complete iff
ex C being 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 being FormalContext st ConceptLattice(C),L are_isomorphic;
end;
given C being FormalContext such that
A1: ConceptLattice(C),L are_isomorphic;
consider f being Homomorphism of L,ConceptLattice(C) such that
A2: f is isomorphism by A1,LATTICE4:def 5;
let X be Subset of L;
set FX = { f.x where x is Element of L : x in X };
FX c= the carrier of ConceptLattice(C)
proof
let x be set; assume x in FX;
then consider y being Element of L such that
A3: x = f.y & y in X;
thus thesis by A3;
end;
then reconsider FX as Subset of ConceptLattice(C);
set Fa = "/\"(FX,ConceptLattice(C));
A4: Fa is_less_than FX &
for b being Element of ConceptLattice(C)
st b is_less_than FX holds b [= Fa by LATTICE3:34;
A5: f is epimorphism monomorphism by A2,LATTICE4:def 4;
then consider a being Element of L such that
A6: Fa = f.a by LATTICE4:9;
A7: 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 A4,LATTICE3:def 16;
hence thesis by A5,A6,LATTICE4:8;
end;
for b being Element of L st b is_less_than X holds b [= a
proof
let b be Element of L; assume A8: 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 being Element of L such that
A9: q = f.y & y in X;
b [= y by A8,A9,LATTICE3:def 16;
hence thesis by A5,A9,LATTICE4:8;
end;
then f.b [= f.a by A6,LATTICE3:34;
hence thesis by A5,LATTICE4:8;
end;
hence thesis by A7;
end;
begin :: Dual Concept Lattices
definition
let L be complete Lattice;
cluster L.: -> complete;
coherence
proof
A1: L.: = LattStr(#the carrier of L,the L_meet of L,
the L_join of L#) by LATTICE2:def 2;
A2: (LattPOSet L)~ = RelStr(#the carrier of (LattPOSet L),
(the InternalRel of (LattPOSet L))~#) by LATTICE3:def 5;
A3: (LattPOSet L.:)~ = RelStr(#the carrier of (LattPOSet L.:),
(the InternalRel of (LattPOSet L.:))~#) by LATTICE3:def 5;
A4: LattPOSet L = RelStr(#the carrier of L, LattRel L#) by LATTICE3:def 2;
A5: LattPOSet (L.:.:) = RelStr(#the carrier of (L.:.:), LattRel (L.:.:)#)
by LATTICE3:def 2;
LattRel (L.:) = (LattRel L)~ by LATTICE3:20;
then A6:LattRel (L.:.:) = ((LattRel L)~)~ by LATTICE3:20;
let X be Subset of L.:;
reconsider X' = X as Subset of L by A1;
set a' = "\/"(X',L);
A7: X' is_less_than a' &
for r being Element of L
st X' is_less_than r holds a' [= r by LATTICE3:def 21;
reconsider a = a' as Element of L.: by A1;
A8:a is_less_than X
proof
let q' be Element of L.:; assume A9: q' in X;
reconsider q = q' as Element of L by A1;
q [= a' by A7,A9,LATTICE3:def 17;
then q% <= (a')% by LATTICE3:7;
then [q%,(a')%] in the InternalRel of LattPOSet L by ORDERS_1:def 9;
then [(a')%,q%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7;
then A10: [(a')%,q%] in the InternalRel of LattPOSet (L.:)
by A2,LATTICE3:20;
A11: (a')% = a' by LATTICE3:def 3 .= a% by LATTICE3:def 3;
(q')% = q' by LATTICE3:def 3 .= q% by LATTICE3:def 3;
then a% <= (q')% by A10,A11,ORDERS_1:def 9;
hence thesis by LATTICE3:7;
end;
for b being Element of L.:
st b is_less_than X holds b [= a
proof
let b be Element of L.:;
assume A12: b is_less_than X;
reconsider b' = b as Element of L by A1;
X' is_less_than b'
proof
let q be Element of L; assume A13: q in X';
reconsider q' = q as Element of L.: by A1;
b [= q' by A12,A13,LATTICE3:def 16;
then b% <= (q')% by LATTICE3:7;
then [b%,(q')%] in the InternalRel of LattPOSet L.: by ORDERS_1:def 9;
then [(q')%,b%] in (the InternalRel of LattPOSet L.:)~ by RELAT_1:def 7;
then A14: [(q')%,b%] in the InternalRel of LattPOSet (L.:.:)
by A3,LATTICE3:20;
A15: (b')% = b' by LATTICE3:def 3 .= b% by LATTICE3:def 3;
(q')% = q' by LATTICE3:def 3 .= q% by LATTICE3:def 3;
then q% <= (b')% by A4,A5,A6,A14,A15,ORDERS_1:def 9;
hence thesis by LATTICE3:7;
end;
then a' [= b' by LATTICE3:def 21;
then (a')% <= (b')% by LATTICE3:7;
then [(a')%,(b')%] in the InternalRel of LattPOSet L by ORDERS_1:def 9;
then [(b')%,(a')%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7;
then A16: [(b')%,(a')%] in the InternalRel of LattPOSet (L.:)
by A2,LATTICE3:20;
A17: (a')% = a' by LATTICE3:def 3 .= a% by LATTICE3:def 3;
(b')% = b' by LATTICE3:def 3 .= b% by LATTICE3:def 3;
then b% <= a% by A16,A17,ORDERS_1:def 9;
hence thesis by LATTICE3:7;
end;
hence thesis by A8;
end;
end;
definition
let C be FormalContext;
func C.: -> strict non quasi-empty ContextStr equals :Def7:
ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #);
coherence by CONLAT_1:def 2;
end;
theorem
for C being strict FormalContext holds (C.:).: = C
proof
let C be strict FormalContext;
A1: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
set CP = C.:;
CP.: = ContextStr(#the Attributes of CP, the Objects of CP,
(the Information of CP)~ #) by Def7;
hence thesis by A1;
end;
theorem
Th18:for C being FormalContext
for O being Subset of the Objects of C holds
(ObjectDerivation(C)).O = (AttributeDerivation(C.:)).O
proof
let C be FormalContext;
let O be Subset of the Objects of C;
A1: (ObjectDerivation(C)).O =
{a where a is Attribute of C : for o being Object of C st o in O
holds o is-connected-with a } by CONLAT_1:def 6;
A2: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider O' = O as Element of bool(the Attributes of C.:);
A3: (AttributeDerivation(C.:)).O' =
{a where a is Object of C.: : for o being Attribute of C.: st o in O'
holds a is-connected-with o } by CONLAT_1:def 7;
set A1 = {a where a is Attribute of C : for o being Object of C st o in O
holds o is-connected-with a };
set A2 = {a where a is Object of C.: : for o being Attribute of C.: st o in O'
holds a is-connected-with o };
A4: A1 c= A2
proof
let u be set; assume u in A1;
then consider a being Attribute of C such that
A5: a = u & for o being Object of C st o in O
holds o is-connected-with a;
reconsider u' = u as Object of C.: by A2,A5;
for o' being Attribute of C.: st o' in O' holds u' is-connected-with o'
proof
let o' be Attribute of C.:; assume A6: o' in O';
then reconsider o = o' as Object of C;
o is-connected-with a by A5,A6;
then [o,a] in the Information of C by CONLAT_1:def 5;
then [a,o] in the Information of C.: by A2,RELAT_1:def 7;
hence thesis by A5,CONLAT_1:def 5;
end;
hence thesis;
end;
A2 c= A1
proof
let u be set; assume u in A2;
then consider a being Object of C.: such that A7:
a = u & for o being Attribute of C.: st o in O'
holds a is-connected-with o;
reconsider u' = u as Attribute of C by A2,A7;
for o being Object of C st o in O holds o is-connected-with u'
proof
let o' be Object of C; assume A8: o' in O;
then o' in O';
then reconsider o = o' as Attribute of C.:;
a is-connected-with o by A7,A8;
then [a,o] in the Information of C.: by CONLAT_1:def 5;
then [o',u'] in the Information of C by A2,A7,RELAT_1:def 7;
hence thesis by CONLAT_1:def 5;
end;
hence thesis;
end;
hence thesis by A1,A3,A4,XBOOLE_0:def 10;
end;
theorem
Th19:for C being FormalContext
for A being Subset of the Attributes of C holds
(AttributeDerivation(C)).A = (ObjectDerivation(C.:)).A
proof
let C be FormalContext;
let O be Subset of the Attributes of C;
A1: (AttributeDerivation(C)).O =
{a where a is Object of C : for o being Attribute of C st o in O
holds a is-connected-with o } by CONLAT_1:def 7;
A2: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider O' = O as Element of bool(the Objects of C.:);
A3: (ObjectDerivation(C.:)).O' =
{a where a is Attribute of C.: : for o being Object of C.: st o in O'
holds o is-connected-with a } by CONLAT_1:def 6;
set A1 = {a where a is Object of C : for o being Attribute of C st o in O
holds a is-connected-with o };
set A2 = {a where a is Attribute of C.: : for o being Object of C.: st o in O'
holds o is-connected-with a };
A4: A1 c= A2
proof
let u be set; assume u in A1;
then consider a being Object of C such that A5:
a = u & for o being Attribute of C st o in O
holds a is-connected-with o;
reconsider u' = u as Attribute of C.: by A2,A5;
for o being Object of C.: st o in O' holds o is-connected-with u'
proof
let o' be Object of C.:; assume A6: o' in O';
then reconsider o = o' as Attribute of C;
a is-connected-with o by A5,A6;
then [a,o] in the Information of C by CONLAT_1:def 5;
then [o',u'] in the Information of C.: by A2,A5,RELAT_1:def 7;
hence thesis by CONLAT_1:def 5;
end;
hence thesis;
end;
A2 c= A1
proof
let u be set; assume u in A2;
then consider a being Attribute of C.: such that A7:
a = u & for o being Object of C.: st o in O'
holds o is-connected-with a;
reconsider u' = u as Object of C by A2,A7;
for o being Attribute of C st o in O holds u' is-connected-with o
proof
let o' be Attribute of C; assume A8: o' in O;
then o' in O';
then reconsider o = o' as Object of C.:;
o is-connected-with a by A7,A8;
then [o,a] in the Information of C.: by CONLAT_1:def 5;
then [u',o'] in the Information of C by A2,A7,RELAT_1:def 7;
hence thesis by CONLAT_1:def 5;
end;
hence thesis;
end;
hence thesis by A1,A3,A4,XBOOLE_0:def 10;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
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
A1: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider A = the Extent of CP as Subset of the Attributes of C.:;
reconsider O = the Intent of CP as Subset of the Objects of C.: by A1;
take ConceptStr(# O,A#);
thus thesis;
end;
uniqueness;
end;
definition
let C be FormalContext;
let CP be FormalConcept of C;
redefine func CP.: -> strict FormalConcept of C.:;
coherence
proof
A1: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider A = the Extent of CP as Subset of the Attributes of C.:;
reconsider O = the Intent of CP as Subset of the Objects of C.: by A1;
set CPD = ConceptStr(# O,A#);
A2: (ObjectDerivation(C.:)).(the Extent of CPD) =
(AttributeDerivation(C)).(the Intent of CP) by Th19 .= the Intent of CPD
by CONLAT_1:def 13;
A3: (AttributeDerivation(C.:)).(the Intent of CPD) =
(ObjectDerivation(C)).(the Extent of CP) by Th18 .= the Extent of CPD by
CONLAT_1:def 13;
CPD = CP.: by Def8;
hence thesis by A2,A3,Lm3,CONLAT_1:def 13;
end;
end;
theorem
for C being FormalContext
for CP being strict FormalConcept of C holds (CP.:).: = CP
proof
let C be FormalContext;
let CP be strict FormalConcept of C;
A1: the Extent of (CP.:).: = the Intent of CP.: by Def8
.= the Extent of CP by Def8;
the Intent of (CP.:).: = the Extent of CP.: by Def8
.= the Intent of CP by Def8;
then ConceptStr(#the Extent of (CP.:).:,the Intent of (CP.:).:#) =
ConceptStr(# the Extent of CP,the Intent of CP#) by A1;
hence thesis;
end;
Lm4:for C being FormalContext
for O being Subset of the Objects of C
for A being Subset of the Attributes of C
st ConceptStr(#O,A#) is FormalConcept of C
holds (ConceptStr(#O,A#)).: is FormalConcept of C.:
proof
let C be FormalContext;
let O be Subset of the Objects of C;
let A be Subset of the Attributes of C;
assume ConceptStr(#O,A#) is FormalConcept of C;
then reconsider CP = ConceptStr(#O,A#) as strict FormalConcept of C;
CP.: is strict FormalConcept of C.:;
hence thesis;
end;
definition
let C be FormalContext;
func DualHomomorphism(C) ->
Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:) means :Def9:
for CP being strict FormalConcept of C holds it.CP = CP.:;
existence
proof
set f = {[ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]
where O is Subset of the Objects of C,
A is Subset of the Attributes of C :
ConceptStr(#O,A#) is FormalConcept of C };
A1: (ConceptLattice(C)).:
= LattStr(#the carrier of ConceptLattice(C),
the L_meet of ConceptLattice(C),
the L_join of ConceptLattice(C)#) by LATTICE2:def 2;
A2: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
A3: ConceptLattice(C.:) = LattStr(#B-carrier(C.:),B-join(C.:),B-meet(C.:)#)
by CONLAT_1:def 23;
A4: (ConceptLattice(C)).:
= LattStr(#B-carrier(C),B-meet(C),B-join(C)#) by A2,LATTICE2:def 2;
f c= [: the carrier of (ConceptLattice(C)).:,
the carrier of ConceptLattice(C.:) :]
proof
let y be set; assume y in f;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A5:
y = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] &
ConceptStr(#O,A#) is FormalConcept of C;
A6: ConceptStr(#O,A#) in the carrier of (ConceptLattice(C)).:
by A4,A5,CONLAT_1:35;
(ConceptStr(#O,A#)).: is strict FormalConcept of C.: by A5,Lm4;
then (ConceptStr(#O,A#)).: in the carrier of ConceptLattice(C.:)
by A3,CONLAT_1:35;
hence thesis by A5,A6,ZFMISC_1:def 2;
end;
then reconsider f as Relation of the carrier of (ConceptLattice(C)).:,
the carrier of ConceptLattice(C.:) by RELSET_1:def 1;
the carrier of (ConceptLattice(C)).: c= dom f
proof
let y be set; assume y in the carrier of (ConceptLattice(C)).:;
then A7:y is strict FormalConcept of C by A4,CONLAT_1:35;
then consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A8: y = ConceptStr(#O',A'#);
set z = (ConceptStr(#O',A'#)).:;
(ConceptStr(#O',A'#)).: is strict FormalConcept of C.: by A7,A8,Lm4;
then reconsider z as Element of ConceptLattice(C.:)
by A3,CONLAT_1:35;
[y,z] in f by A7,A8;
hence thesis by RELAT_1:def 4;
end;
then A9: the carrier of (ConceptLattice(C)).: = dom f by XBOOLE_0:def 10;
for x,y1,y2 being set st [x,y1] in f & [x,y2] in f holds y1 = y2
proof
let x,y1,y2 be set; assume A10: [x,y1] in f & [x,y2] in f;
then consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that
A11: [x,y1] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] &
ConceptStr(#O,A#) is FormalConcept of C;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that
A12: [x,y2] = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:] &
ConceptStr(#O',A'#) is FormalConcept of C by A10;
ConceptStr(#O,A#) = [x,y1]`1 by A11,MCART_1:def 1
.= x by MCART_1:def 1
.= [x,y2]`1 by MCART_1:def 1
.= ConceptStr(#O',A'#) by A12,MCART_1:def 1;
hence y1 = [x,y2]`2 by A11,A12,MCART_1:def 2
.= y2 by MCART_1:def 2;
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;
A13: (LattPOSet (ConceptLattice(C)))~ =
RelStr(#the carrier of (LattPOSet (ConceptLattice(C))),
(the InternalRel of (LattPOSet (ConceptLattice(C))))~#)
by LATTICE3:def 5;
A14: LattPOSet ConceptLattice(C) =
RelStr(#the carrier of ConceptLattice(C),LattRel ConceptLattice(C)#)
by LATTICE3:def 2;
A15: for a,b being Element of (ConceptLattice(C)).:
holds a [= b implies f.a [= f.b
proof
let a,b be Element of (ConceptLattice(C)).:;
assume A16: a [= b;
reconsider a' = a, b' = b as Element of ConceptLattice(C)
by A1;
A17: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
then consider fa being set such that A18: [a,fa] in f by RELAT_1:def 4;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A19:
[a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] &
ConceptStr(#O,A#) is FormalConcept of C by A18;
A20: a = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 by A19,MCART_1:def 1
.= (ConceptStr(#O,A#)) by MCART_1:def 1;
A21: f.a = fa by A18,FUNCT_1:8;
consider fb being set such that A22: [b,fb] in f by A17,RELAT_1:def 4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that A23:
[b,fb] = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:] &
ConceptStr(#O',A'#) is FormalConcept of C by A22;
A24: b = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:]`1 by A23,MCART_1:
def 1
.= (ConceptStr(#O',A'#)) by MCART_1:def 1;
A25: f.b = fb by A22,FUNCT_1:8;
a% <= b% by A16,LATTICE3:7;
then [a%,b%] in the InternalRel of (LattPOSet((ConceptLattice(C)).:))
by ORDERS_1:def 9;
then [a%,b%] in (the InternalRel of (LattPOSet (ConceptLattice(C))))~
by A13,LATTICE3:20;
then A26: [b%,a%] in the InternalRel of (LattPOSet (ConceptLattice(C)))
by RELAT_1:def 7;
reconsider aa = a%, bb = b% as Element of
LattPOSet ConceptLattice(C) by A1,A14,LATTICE3:def 3;
A27: bb <= aa by A26,ORDERS_1:def 9;
A28: (%aa)% = %aa by LATTICE3:def 3 .= aa by LATTICE3:def 4;
(%bb)% = %bb by LATTICE3:def 3 .= bb by LATTICE3:def 4;
then %bb [= %aa by A27,A28,LATTICE3:7;
then A29: (%bb)@ is-SubConcept-of (%aa)@ by CONLAT_1:47;
A30: %(bb)@ = %bb by CONLAT_1:def 24 .= bb by LATTICE3:def 4
.= b by LATTICE3:def 3 .= (b')@ by CONLAT_1:def 24;
A31: %(aa)@ = %aa by CONLAT_1:def 24 .= aa by LATTICE3:def 4
.= a by LATTICE3:def 3 .= (a')@ by CONLAT_1:def 24;
fa in rng f by A18,RELAT_1:def 5;
then reconsider fa as Element of ConceptLattice(C.:);
fb in rng f by A22,RELAT_1:def 5;
then reconsider fb as Element of ConceptLattice(C.:);
fa = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`2
by A19,MCART_1:def 2
.= (ConceptStr(#O,A#)).: by MCART_1:def 2;
then A32: the Intent of fa@
= the Intent of (ConceptStr(#O,A#)).: by CONLAT_1:def 24
.= the Extent of ConceptStr(#O,A#) by Def8
.= the Extent of (a')@ by A20,CONLAT_1:def 24;
fb = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:]`2
by A23,MCART_1:def 2
.= (ConceptStr(#O',A'#)).: by MCART_1:def 2;
then the Intent of fb@
= the Intent of (ConceptStr(#O',A'#)).: by CONLAT_1:def 24
.= the Extent of ConceptStr(#O',A'#) by Def8
.= the Extent of (b')@ by A24,CONLAT_1:def 24;
then the Intent of (fb)@ c= the Intent of (fa)@ by A29,A30,A31,A32,
CONLAT_1:def 19;
then (fa)@ is-SubConcept-of (fb)@ by CONLAT_1:31;
hence thesis by A21,A25,CONLAT_1:47;
end;
the carrier of ConceptLattice(C.:) c= rng f
proof
let u be set; assume u in the carrier of ConceptLattice(C.:);
then reconsider u as Element of ConceptLattice(C.:);
A33: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider O' = the Extent of u@ as Subset of the Attributes of C;
reconsider A' = the Intent of u@ as Subset of the Objects of C by A33;
set CP = ConceptStr(#A',O'#);
A34: (ObjectDerivation(C)).(the Extent of CP) =
(AttributeDerivation(C.:)).(the Intent of u@) by Th18 .=
the Intent of CP by CONLAT_1:def 13;
A35: (AttributeDerivation(C)).(the Intent of CP) =
(ObjectDerivation(C.:)).(the Extent of u@) by Th19 .=
the Extent of CP by CONLAT_1:def 13;
not(the Extent of u@ is empty & the Intent of u@ is empty)
by CONLAT_1:def 11;
then A36: CP is FormalConcept of C by A34,A35,CONLAT_1:def 11,def 13;
dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
then CP in dom f by A1,A2,A36,CONLAT_1:35;
then consider v being set such that A37: [CP,v] in f by RELAT_1:def 4;
consider Ov being Subset of the Objects of C,
Av being Subset of the Attributes of C such that A38:
[CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] &
ConceptStr(#Ov,Av#) is FormalConcept of C by A37;
A39: v in rng f by A37,RELAT_1:def 5;
then reconsider v as strict FormalConcept of C.: by A3,CONLAT_1:35;
A40: v = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:
]`2 by A38,MCART_1:def 2
.= (ConceptStr(#Ov,Av#)).: by MCART_1:def 2;
A41: CP = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:
]`1 by A38,MCART_1:def 1
.= ConceptStr(#Ov,Av#) by MCART_1:def 1; then A42:
the Extent of v = the Extent of u@ by A40,Def8;
the Intent of v = the Intent of u@ by A40,A41,Def8;
hence thesis by A39,A42,CONLAT_1:def 24;
end;
then A43: rng f = the carrier of ConceptLattice(C.:) by XBOOLE_0:def 10;
A44: for a,b being Element of (ConceptLattice(C)).:
holds f.a [= f.b implies a [= b
proof
let a,b be Element of (ConceptLattice(C)).:;
assume A45: f.a [= f.b;
reconsider a' = a, b' = b as Element of ConceptLattice(C)
by A1;
A46: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
then consider fa being set such that A47: [a,fa] in f by RELAT_1:def 4;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A48:
[a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] &
ConceptStr(#O,A#) is FormalConcept of C by A47;
A49: a = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 by A48,MCART_1:def 1
.= (ConceptStr(#O,A#)) by MCART_1:def 1;
consider fb being set such that A50: [b,fb] in f by A46,RELAT_1:def 4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that A51:
[b,fb] = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:] &
ConceptStr(#O',A'#) is FormalConcept of C by A50;
A52: b = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:]`1 by A51,MCART_1:
def 1
.= (ConceptStr(#O',A'#)) by MCART_1:def 1;
A53: (f.a)@ is-SubConcept-of (f.b)@ by A45,CONLAT_1:47;
fa in rng f by A47,RELAT_1:def 5;
then reconsider fa as Element of ConceptLattice(C.:);
fb in rng f by A50,RELAT_1:def 5;
then reconsider fb as Element of ConceptLattice(C.:);
A54: fa = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`2
by A48,MCART_1:def 2
.= (ConceptStr(#O,A#)).: by MCART_1:def 2;
A55: the Intent of (f.a)@
= the Intent of fa@ by A47,FUNCT_1:8
.= the Intent of (ConceptStr(#O,A#)).: by A54,CONLAT_1:def 24
.= the Extent of ConceptStr(#O,A#) by Def8
.= the Extent of (a')@ by A49,CONLAT_1:def 24;
A56: fb = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:]`2
by A51,MCART_1:def 2
.= (ConceptStr(#O',A'#)).: by MCART_1:def 2;
the Intent of (f.b)@
= the Intent of fb@ by A50,FUNCT_1:8
.= the Intent of (ConceptStr(#O',A'#)).: by A56,CONLAT_1:def 24
.= the Extent of ConceptStr(#O',A'#) by Def8
.= the Extent of (b')@ by A52,CONLAT_1:def 24;
then the Extent of (b')@ c= the Extent of (a')@ by A53,A55,CONLAT_1:31;
then (b')@ is-SubConcept-of (a')@ by CONLAT_1:def 19;
then b' [= a' by CONLAT_1:47;
then (b')% <= (a')% by LATTICE3:7;
then A57: [(b')%,(a')%] in the InternalRel of (LattPOSet(ConceptLattice(C))
)
by ORDERS_1:def 9;
A58: (a')% = a' by LATTICE3:def 3 .= a% by LATTICE3:def 3;
(b')% = b' by LATTICE3:def 3 .= b% by LATTICE3:def 3;
then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)))~ by A13
,A57,A58,RELAT_1:def 7;
then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)).:)
by LATTICE3:20;
then a% <= b% by ORDERS_1:def 9;
hence thesis by LATTICE3:7;
end;
f is one-to-one
proof
let a,b be set;
assume A59: a in dom f & b in dom f & f.a = f.b;
then reconsider a,b as Element of (ConceptLattice(C)).:;
consider fa being set such that A60: [a,fa] in f by A59,RELAT_1:def 4;
consider O being Subset of the Objects of C,
A being Subset of the Attributes of C such that A61:
[a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] &
ConceptStr(#O,A#) is FormalConcept of C by A60;
A62: a = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 by A61,MCART_1:def 1
.= (ConceptStr(#O,A#)) by MCART_1:def 1;
consider fb being set such that A63: [b,fb] in f by A59,RELAT_1:def 4;
consider O' being Subset of the Objects of C,
A' being Subset of the Attributes of C such that A64:
[b,fb] = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:] &
ConceptStr(#O',A'#) is FormalConcept of C by A63;
A65: b = [ConceptStr(#O',A'#),(ConceptStr(#O',A'#)).:
]`1 by A64,MCART_1:def 1
.= (ConceptStr(#O',A'#)) by MCART_1:def 1;
A66: f.b = fb by A63,FUNCT_1:8;
A67: (ConceptStr(#O',A'#)).: = [b,fb]`2 by A64,MCART_1:def 2
.= fb by MCART_1:def 2
.= fa by A59,A60,A66,FUNCT_1:8
.= [a,fa]`2 by MCART_1:def 2
.= (ConceptStr(#O,A#)).: by A61,MCART_1:def 2;
then A68: the Extent of ConceptStr(#O',A'#) =
the Intent of (ConceptStr(#O,A#)).: by Def8 .=
the Extent of ConceptStr(#O,A#) by Def8;
the Intent of ConceptStr(#O',A'#) =
the Extent of (ConceptStr(#O,A#)).: by A67,Def8 .=
the Intent of ConceptStr(#O,A#) by Def8;
hence thesis by A62,A65,A68;
end;
then reconsider f as Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:)
by A15,A43,A44,Lm2;
for CP being strict FormalConcept of C holds f.CP = CP.:
proof
let CP be strict FormalConcept of C;
CP in B-carrier(C) by CONLAT_1:35;
then CP in dom f by A4,FUNCT_2:def 1;
then consider v being set such that A69: [CP,v] in f by RELAT_1:def 4;
consider Ov being Subset of the Objects of C,
Av being Subset of the Attributes of C such that A70:
[CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] &
ConceptStr(#Ov,Av#) is FormalConcept of C by A69;
v in rng f by A69,RELAT_1:def 5;
then reconsider v as strict FormalConcept of C.: by A3,CONLAT_1:35;
A71: v = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:
]`2 by A70,MCART_1:def 2
.= (ConceptStr(#Ov,Av#)).: by MCART_1:def 2;
CP = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)
).:]`1 by A70,MCART_1:def 1
.= ConceptStr(#Ov,Av#) by MCART_1:def 1;
hence thesis by A69,A71,FUNCT_1:8;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:);
assume A72: for CP being strict FormalConcept of C holds F1.CP = CP.:;
assume A73: for CP being strict FormalConcept of C holds F2.CP = CP.:;
A74: for u being set st u in the carrier of (ConceptLattice(C)).:
holds F1.u = F2.u
proof
let u be set;
assume A75: u in the carrier of (ConceptLattice(C)).:;
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
then (ConceptLattice(C)).: = LattStr(#B-carrier(C),B-meet(C),B-join(C)#)
by LATTICE2:def 2;
then reconsider u as strict FormalConcept of C by A75,CONLAT_1:35;
F1.u = u.: by A72 .= F2.u by A73;
hence thesis;
end;
A76: dom F1 = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
dom F2 = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
hence thesis by A74,A76,FUNCT_1:9;
end;
end;
theorem
Th21:for C being FormalContext holds DualHomomorphism(C) is isomorphism
proof
let C be FormalContext;
set f = DualHomomorphism(C);
f is one-to-one
proof
let a,b be set; assume
A1:a in dom f & b in dom f & f.a = f.b;
then reconsider a,b as Element of (ConceptLattice(C)).:;
(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);
A2: f.(a@) = (a@).: & f.(b@) = (b@).: by Def9;
A3: f.(a@) = f.a & f.(b@) = f.b by CONLAT_1:def 24;
then A4: the Intent of a@ = the Extent of (b@).: by A1,A2,Def8
.= the Intent of b@ by Def8;
the Extent of a@ = the Intent of (b@).: by A1,A2,A3,Def8
.= the Extent of b@ by Def8;
then a = b@ by A4,CONLAT_1:def 24 .= b by CONLAT_1:def 24;
hence thesis;
end;
then A5: f is monomorphism by LATTICE4:def 2;
A6: (ConceptLattice(C)).:
= LattStr(#the carrier of ConceptLattice(C),
the L_meet of ConceptLattice(C),
the L_join of ConceptLattice(C)#) by LATTICE2:def 2;
A7: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#)
by CONLAT_1:def 23;
the carrier of ConceptLattice(C.:) c= rng f
proof
let u be set; assume u in the carrier of ConceptLattice(C.:);
then reconsider u as Element of ConceptLattice(C.:);
A8: C.: = ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #) by Def7;
then reconsider O' = the Extent of u@ as Subset of the Attributes of C;
reconsider A' = the Intent of u@ as Subset of the Objects of C by A8;
set CP = ConceptStr(#A',O'#);
A9: (ObjectDerivation(C)).(the Extent of CP) =
(AttributeDerivation(C.:)).(the Intent of u@) by Th18 .=
the Intent of CP by CONLAT_1:def 13;
A10: (AttributeDerivation(C)).(the Intent of CP) =
(ObjectDerivation(C.:)).(the Extent of u@) by Th19 .=
the Extent of CP by CONLAT_1:def 13;
A11: not(the Extent of u@ is empty & the Intent of u@ is empty)
by CONLAT_1:def 11;
then CP is FormalConcept of C by A9,A10,CONLAT_1:def 11,def 13;
then A12: CP in the carrier of (ConceptLattice(C)) by A7,CONLAT_1:35;
reconsider CP as strict FormalConcept of C by A9,A10,A11,CONLAT_1:def 11,def
13;
A13: CP in dom f by A6,A12,FUNCT_2:def 1;
A14: f.CP = CP.: by Def9;
A15: the Intent of CP.: = the Intent of u@ by Def8;
the Extent of CP.: = the Extent of u@ by Def8;
then f.CP = u by A14,A15,CONLAT_1:def 24;
hence thesis by A13,FUNCT_1:def 5;
end;
then rng f = the carrier of ConceptLattice(C.:) by XBOOLE_0:def 10;
then f is epimorphism by LATTICE4:def 3;
hence thesis by A5,LATTICE4:def 4;
end;
theorem
for C being FormalContext holds
ConceptLattice(C.:),(ConceptLattice(C)).: are_isomorphic
proof
let C be FormalContext;
DualHomomorphism(C) is isomorphism by Th21;
hence thesis by LATTICE4:def 5;
end;