:: Introduction to Concept Lattices
:: by Christoph Schwarzweller
::
:: Received October 2, 1998
:: Copyright (c) 1998-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, XBOOLE_0, RELAT_1, CAT_1, SUBSET_1, TARSKI, FUNCT_1,
ZFMISC_1, MCART_1, YELLOW_1, LATTICE3, ORDERS_2, FILTER_1, WAYBEL_1,
WAYBEL_0, XXREAL_0, PBOOLE, EQREL_1, CLASSES2, BINOP_1, LATTICES,
QC_LANG1, REWRITE1, SETFAM_1, CONLAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES,
ORDERS_2, YELLOW_1, WAYBEL_1, LATTICE3, SETFAM_1, WAYBEL_0;
constructors BINOP_1, DOMAIN_1, LATTICE3, WAYBEL_1, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES,
LATTICE3, YELLOW_1, XTUPLE_0;
requirements SUBSET, BOOLE;
begin
registration
cluster strict non empty non void for 2-sorted;
end;
definition
::$CD
struct (2-sorted) ContextStr (# carrier, carrier' -> set, Information ->
Relation of the carrier,the carrier' #);
end;
registration
cluster strict non empty non void for ContextStr;
end;
definition
mode FormalContext is non empty non void ContextStr;
end;
definition
let C be 2-sorted;
mode Object of C is Element of C;
mode Attribute of C is Element of the carrier' of C;
end;
registration
let C be non empty non void 2-sorted;
cluster the carrier' of C -> non empty;
cluster the carrier of C -> non empty;
end;
registration
let C be non empty non void 2-sorted;
cluster non empty for Subset of the carrier of C;
cluster non empty for Subset of the carrier' of C;
end;
definition
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
pred o is-connected-with a means
:: CONLAT_1:def 2
[o,a] in the Information of C;
end;
notation
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
antonym o is-not-connected-with a for o is-connected-with a;
end;
:: Derivation Operators
begin
definition
let C be FormalContext;
func ObjectDerivation(C) -> Function of bool the carrier of C,bool the
carrier' of C means
:: CONLAT_1:def 3
for O being Subset of the carrier of C holds it.O =
{ a where a is Attribute of C : for o being Object of C st o in O holds o
is-connected-with a };
end;
definition
let C be FormalContext;
func AttributeDerivation(C) -> Function of bool the carrier' of C,bool the
carrier of C means
:: CONLAT_1:def 4
for A being Subset of the carrier' of C holds it.A =
{ o where o is Object of C : for a being Attribute of C st a in A holds o
is-connected-with a };
end;
theorem :: CONLAT_1:1
for C being FormalContext for o being Object of C holds (
ObjectDerivation(C)).({o}) = {a where a is Attribute of C : o is-connected-with
a};
theorem :: CONLAT_1:2
for C being FormalContext for a being Attribute of C holds (
AttributeDerivation(C)).({a}) = {o where o is Object of C : o is-connected-with
a};
theorem :: CONLAT_1:3
for C being FormalContext for O1,O2 being Subset of the carrier
of C holds O1 c= O2 implies (ObjectDerivation(C)).O2 c= (ObjectDerivation(C)).
O1;
theorem :: CONLAT_1:4
for C being FormalContext for A1,A2 being Subset of the carrier'
of C holds A1 c= A2 implies (AttributeDerivation(C)).A2 c= (AttributeDerivation
(C)).A1;
theorem :: CONLAT_1:5
for C being FormalContext for O being Subset of the carrier of C
holds O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O);
theorem :: CONLAT_1:6
for C being FormalContext for A being Subset of the carrier' of C
holds A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A);
theorem :: CONLAT_1:7
for C being FormalContext for O being Subset of the carrier of C
holds (ObjectDerivation(C)).O = (ObjectDerivation(C)).((AttributeDerivation(C))
.((ObjectDerivation(C)).O));
theorem :: CONLAT_1:8
for C being FormalContext for A being Subset of the carrier' of C
holds (AttributeDerivation(C)).A = (AttributeDerivation(C)).((ObjectDerivation(
C)).((AttributeDerivation(C)).A));
theorem :: CONLAT_1:9
for C being FormalContext for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A
iff [:O,A:] c= the Information of C;
theorem :: CONLAT_1:10
for C being FormalContext for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds A c= (ObjectDerivation(C)).O iff
[:O,A:] c= the Information of C;
theorem :: CONLAT_1:11
for C being FormalContext for O being Subset of the carrier of C for A
being Subset of the carrier' of C holds O c= (AttributeDerivation(C)).A iff A
c= (ObjectDerivation(C)).O;
definition
let C be FormalContext;
func phi(C) -> Function of BoolePoset the carrier of C, BoolePoset the
carrier' of C equals
:: CONLAT_1:def 5
ObjectDerivation(C);
end;
definition
let C be FormalContext;
func psi(C) -> Function of BoolePoset the carrier' of C, BoolePoset the
carrier of C equals
:: CONLAT_1:def 6
AttributeDerivation(C);
end;
definition
let P,R be non empty RelStr;
let Con be Connection of P,R;
attr Con is co-Galois means
:: CONLAT_1:def 7
ex f being Function of P,R, g being
Function of R,P st (Con = [f,g] & f is antitone & g is antitone & for p1,p2
being Element of P, r1,r2 being Element of R holds p1 <= g.(f.p1) & r1 <= f.(g.
r1));
end;
theorem :: CONLAT_1:12
for P,R being non empty Poset for Con being Connection of P,R
for f being Function of P,R, g being Function of R,P st Con = [f,g] holds Con
is co-Galois iff for p being Element of P, r being Element of R holds p <= g.r
iff r <= f.p;
theorem :: CONLAT_1:13
for P,R being non empty Poset for Con being Connection of P,R st Con
is co-Galois for f being Function of P,R, g being Function of R,P st Con = [f,g
] holds f = f * (g * f) & g = g * (f * g);
theorem :: CONLAT_1:14
for C being FormalContext holds [phi(C),psi(C)] is co-Galois;
theorem :: CONLAT_1:15
for C being FormalContext for O1,O2 being Subset of the carrier
of C holds (ObjectDerivation(C)).(O1 \/ O2) = ((ObjectDerivation(C)).O1) /\ ((
ObjectDerivation(C)).O2);
theorem :: CONLAT_1:16
for C being FormalContext for A1,A2 being Subset of the carrier'
of C holds (AttributeDerivation(C)).(A1 \/ A2) = ((AttributeDerivation(C)).A1)
/\ ((AttributeDerivation(C)).A2);
theorem :: CONLAT_1:17
for C being FormalContext holds (ObjectDerivation(C)).{} = the carrier' of C;
theorem :: CONLAT_1:18
for C being FormalContext holds (AttributeDerivation(C)).{} =
the carrier of C;
begin :: Formal Concepts
definition
let C be 2-sorted;
struct ConceptStr over C (# Extent -> Subset of the carrier of C, Intent ->
Subset of the carrier' of C #);
end;
definition
let C be 2-sorted;
let CP be ConceptStr over C;
attr CP is empty means
:: CONLAT_1:def 8
the Extent of CP is empty & the Intent of CP is empty;
attr CP is quasi-empty means
:: CONLAT_1:def 9
the Extent of CP is empty or the Intent of CP is empty;
end;
registration
let C be non empty non void 2-sorted;
cluster strict non empty for ConceptStr over C;
cluster strict quasi-empty for ConceptStr over C;
end;
registration
let C be empty void 2-sorted;
cluster -> empty for ConceptStr over C;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is concept-like means
:: CONLAT_1:def 10
(ObjectDerivation(C)).(the Extent of
CP) = the Intent of CP & (AttributeDerivation(C)).(the Intent of CP) = the
Extent of CP;
end;
registration
let C be FormalContext;
cluster concept-like non empty for ConceptStr over C;
end;
definition
let C be FormalContext;
mode FormalConcept of C is concept-like non empty ConceptStr over C;
end;
registration
let C be FormalContext;
cluster strict for FormalConcept of C;
end;
theorem :: CONLAT_1:19
for C being FormalContext for O being Subset of the carrier of C
holds ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O), (
ObjectDerivation(C)).O#) is FormalConcept of C & for O9 being Subset of the
carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is
FormalConcept of C & O c= O9 holds (AttributeDerivation(C)).((ObjectDerivation(
C)).O) c= O9;
theorem :: CONLAT_1:20
for C being FormalContext for O being Subset of the carrier of C holds
(ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is FormalConcept
of C) iff (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O;
theorem :: CONLAT_1:21
for C being FormalContext for A being Subset of the carrier' of
C holds ConceptStr(#(AttributeDerivation(C)).A, (ObjectDerivation(C)).((
AttributeDerivation(C)).A)#) is FormalConcept of C & for O9 being Subset of the
carrier of C, A9 being Subset of the carrier' of C st ConceptStr(#O9,A9#) is
FormalConcept of C & A c= A9 holds (ObjectDerivation(C)).((AttributeDerivation(
C)).A) c= A9;
theorem :: CONLAT_1:22
for C being FormalContext for A being Subset of the carrier' of C
holds (ex O being Subset of the carrier of C st ConceptStr(#O,A#) is
FormalConcept of C) iff (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is universal means
:: CONLAT_1:def 11
the Extent of CP = the carrier of C;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is co-universal means
:: CONLAT_1:def 12
the Intent of CP = the carrier' of C;
end;
registration
let C be FormalContext;
cluster strict universal for FormalConcept of C;
cluster strict co-universal for FormalConcept of C;
end;
definition
let C be FormalContext;
func Concept-with-all-Objects(C) -> strict universal FormalConcept of C
means
:: CONLAT_1:def 13
ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).({}) & A
= (ObjectDerivation(C)).((AttributeDerivation(C)).({}));
end;
definition
let C be FormalContext;
func Concept-with-all-Attributes(C) -> strict co-universal FormalConcept of
C means
:: CONLAT_1:def 14
ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((
ObjectDerivation(C)).({})) & A = (ObjectDerivation(C)).({});
end;
theorem :: CONLAT_1:23
for C being FormalContext holds the Extent of
Concept-with-all-Objects(C) = the carrier of C & the Intent of
Concept-with-all-Attributes(C) = the carrier' of C;
theorem :: CONLAT_1:24
for C being FormalContext for CP being FormalConcept of C holds (the
Extent of CP = {} implies CP is co-universal) & (the Intent of CP = {} implies
CP is universal);
theorem :: CONLAT_1:25
for C being FormalContext for CP being strict FormalConcept of C
holds (the Extent of CP = {} implies CP = Concept-with-all-Attributes(C)) & (
the Intent of CP = {} implies CP = Concept-with-all-Objects(C));
theorem :: CONLAT_1:26
for C being FormalContext for CP being quasi-empty ConceptStr over C
st CP is FormalConcept of C holds CP is universal or CP is co-universal;
theorem :: CONLAT_1:27
for C being FormalContext for CP being quasi-empty ConceptStr over C
st CP is strict FormalConcept of C holds CP = Concept-with-all-Objects(C) or CP
= Concept-with-all-Attributes(C);
definition
let C be FormalContext;
mode Set-of-FormalConcepts of C -> non empty set means
:: CONLAT_1:def 15
for X being set st X in it holds X is FormalConcept of C;
end;
definition
let C be FormalContext;
let FCS be Set-of-FormalConcepts of C;
redefine mode Element of FCS -> FormalConcept of C;
end;
definition
let C be FormalContext;
let CP1,CP2 be FormalConcept of C;
pred CP1 is-SubConcept-of CP2 means
:: CONLAT_1:def 16
the Extent of CP1 c= the Extent of CP2;
end;
notation
let C be FormalContext;
let CP1,CP2 be FormalConcept of C;
synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2;
end;
theorem :: CONLAT_1:28
for C being FormalContext for CP1,CP2 being FormalConcept of C
holds CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1;
theorem :: CONLAT_1:29
for C being FormalContext for CP1,CP2 being FormalConcept of C holds
CP1 is-SuperConcept-of CP2 iff the Intent of CP1 c= the Intent of CP2;
theorem :: CONLAT_1:30
for C being FormalContext for CP being FormalConcept of C holds CP
is-SubConcept-of Concept-with-all-Objects(C) & Concept-with-all-Attributes(C)
is-SubConcept-of CP;
begin :: Concept Lattices
definition
let C be FormalContext;
func B-carrier(C) -> non empty set equals
:: CONLAT_1:def 17
{ ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) is non empty & (ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E
};
end;
definition
let C be FormalContext;
redefine func B-carrier(C) -> Set-of-FormalConcepts of C;
end;
registration
let C be FormalContext;
cluster B-carrier(C) -> non empty;
end;
theorem :: CONLAT_1:31
for C being FormalContext for CP being object holds CP in B-carrier
(C) iff CP is strict FormalConcept of C;
definition
let C be FormalContext;
func B-meet(C) -> BinOp of B-carrier(C) means
:: CONLAT_1:def 18
for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, A being
Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = (the
Extent of CP1) /\ (the Extent of CP2) & A = (ObjectDerivation(C)).((
AttributeDerivation(C)). ((the Intent of CP1) \/ (the Intent of CP2)));
end;
definition
let C be FormalContext;
func B-join(C) -> BinOp of B-carrier(C) means
:: CONLAT_1:def 19
for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, A being
Subset of the carrier' of C st it.(CP1,CP2) = ConceptStr(#O,A#) & O = (
AttributeDerivation(C)).((ObjectDerivation(C)). ((the Extent of CP1) \/ (the
Extent of CP2))) & A = (the Intent of CP1) /\ (the Intent of CP2);
end;
theorem :: CONLAT_1:32
for C being FormalContext for CP1,CP2 being strict FormalConcept
of C holds (B-meet(C)).(CP1,CP2) = (B-meet(C)).(CP2,CP1);
theorem :: CONLAT_1:33
for C being FormalContext for CP1,CP2 being strict FormalConcept
of C holds (B-join(C)).(CP1,CP2) = (B-join(C)).(CP2,CP1);
theorem :: CONLAT_1:34
for C being FormalContext for CP1,CP2,CP3 being strict
FormalConcept of C holds (B-meet(C)).(CP1,(B-meet(C)).(CP2,CP3)) = (B-meet(C)).
((B-meet(C)).(CP1,CP2),CP3);
theorem :: CONLAT_1:35
for C being FormalContext for CP1,CP2,CP3 being strict
FormalConcept of C holds (B-join(C)).(CP1,(B-join(C)).(CP2,CP3)) = (B-join(C)).
((B-join(C)).(CP1,CP2),CP3);
theorem :: CONLAT_1:36
for C being FormalContext for CP1,CP2 being strict FormalConcept
of C holds (B-join(C)).((B-meet(C)).(CP1,CP2),CP2) = CP2;
theorem :: CONLAT_1:37
for C being FormalContext for CP1,CP2 being strict FormalConcept
of C holds (B-meet(C)).(CP1,(B-join(C)).(CP1,CP2)) = CP1;
theorem :: CONLAT_1:38
for C being FormalContext for CP being strict FormalConcept of C holds
(B-meet(C)).(CP,Concept-with-all-Objects(C)) = CP;
theorem :: CONLAT_1:39
for C being FormalContext for CP being strict FormalConcept of C
holds (B-join(C)).(CP,Concept-with-all-Objects(C)) = Concept-with-all-Objects(C
);
theorem :: CONLAT_1:40
for C being FormalContext for CP being strict FormalConcept of C holds
(B-join(C)).(CP,Concept-with-all-Attributes(C)) = CP;
theorem :: CONLAT_1:41
for C being FormalContext for CP being strict FormalConcept of C holds
(B-meet(C)).(CP,Concept-with-all-Attributes(C)) = Concept-with-all-Attributes(C
);
definition
let C be FormalContext;
func ConceptLattice(C) -> strict non empty LattStr equals
:: CONLAT_1:def 20
LattStr(#B-carrier
(C),B-join(C),B-meet(C)#);
end;
theorem :: CONLAT_1:42
for C being FormalContext holds ConceptLattice(C) is Lattice;
registration
let C be FormalContext;
cluster ConceptLattice(C) -> strict non empty Lattice-like;
end;
definition
let C be FormalContext;
let S be non empty Subset of ConceptLattice(C);
redefine mode Element of S -> FormalConcept of C;
end;
definition
let C be FormalContext;
let CP be Element of ConceptLattice(C);
func CP@ -> strict FormalConcept of C equals
:: CONLAT_1:def 21
CP;
end;
theorem :: CONLAT_1:43
for C being FormalContext for CP1,CP2 being Element of
ConceptLattice(C) holds CP1 [= CP2 iff CP1@ is-SubConcept-of CP2@;
theorem :: CONLAT_1:44
for C being FormalContext holds ConceptLattice(C) is complete Lattice;
registration
let C be FormalContext;
cluster ConceptLattice(C) -> complete;
end;