Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### Introduction to Concept Lattices

by
Christoph Schwarzweller

MML identifier: CONLAT_1
[ Mizar article, MML identifier index ]

```environ

vocabulary CAT_1, RELAT_1, FUNCT_1, MCART_1, PRE_TOPC, YELLOW_1, LATTICE3,
ORDERS_1, FILTER_1, WAYBEL_1, WAYBEL_0, LATTICES, BOOLE, ZF_LANG,
BINOP_1, QC_LANG1, BHSP_3, SETFAM_1, TARSKI, CONLAT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, RELAT_1, FUNCT_1,
STRUCT_0, BINOP_1, LATTICES, RELSET_1, FUNCT_2, ORDERS_1, PRE_TOPC,
YELLOW_1, WAYBEL_1, LATTICE3, SETFAM_1, WAYBEL_0;
constructors DOMAIN_1, LATTICE3, WAYBEL_1, ORDERS_3;
clusters STRUCT_0, LATTICE3, YELLOW_1, RELSET_1, SUBSET_1, LATTICES, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

definition
struct 2-sorted (# Objects, Attributes -> set #);
end;

definition
let C be 2-sorted;
attr C is empty means
:: CONLAT_1:def 1
the Objects of C is empty & the Attributes of C is empty;
attr C is quasi-empty means
:: CONLAT_1:def 2
the Objects of C is empty or the Attributes of C is empty;
end;

definition
cluster strict non empty 2-sorted;
cluster strict non quasi-empty 2-sorted;
end;

definition
cluster strict empty quasi-empty 2-sorted;
end;

definition
struct (2-sorted) ContextStr
(# Objects, Attributes -> set,
Information -> Relation of the Objects,the Attributes #);
end;

definition
cluster strict non empty ContextStr;
cluster strict non quasi-empty ContextStr;
end;

definition
mode FormalContext is non quasi-empty ContextStr;
end;

definition
let C be 2-sorted;
mode Object of C is Element of the Objects of C;
mode Attribute of C is Element of the Attributes of C;
canceled 2;
end;

definition
let C be non quasi-empty 2-sorted;
cluster the Attributes of C -> non empty;
cluster the Objects of C -> non empty;
end;

definition
let C be non quasi-empty 2-sorted;
cluster non empty Subset of the Objects of C;
cluster non empty Subset of the Attributes 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 5
[o,a] in the Information of C;
antonym o is-not-connected-with a;
end;

::: Derivation Operators
::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

begin

definition
let C be FormalContext;
func ObjectDerivation(C) ->
Function of bool(the Objects of C),bool(the Attributes of C) means
:: CONLAT_1:def 6
for O being Element of bool(the Objects 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 Attributes of C),bool(the Objects of C) means
:: CONLAT_1:def 7
for A being Element of bool(the Attributes 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 Objects 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 Attributes 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 Objects of C holds
O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O);

theorem :: CONLAT_1:6
for C being FormalContext
for A being Subset of the Attributes of C holds
A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A);

theorem :: CONLAT_1:7
for C being FormalContext
for O being Subset of the Objects 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 Attributes 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 Objects of C
for A being Subset of the Attributes 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 Objects of C
for A being Subset of the Attributes 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 Objects of C
for A being Subset of the Attributes of C holds
O c= (AttributeDerivation(C)).A iff A c= (ObjectDerivation(C)).O;

definition
let C be FormalContext;
func phi(C) -> map of BoolePoset(the Objects of C),
BoolePoset(the Attributes of C) equals
:: CONLAT_1:def 8
ObjectDerivation(C);
end;

definition
let C be FormalContext;
func psi(C) -> map of BoolePoset(the Attributes of C),
BoolePoset(the Objects of C) equals
:: CONLAT_1:def 9
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 10
ex f being map of P,R, g being map 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;

canceled;

theorem :: CONLAT_1:13
for P,R being non empty Poset
for Con being Connection of P,R
for f being map of P,R, g being map 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:14
for P,R being non empty Poset
for Con being Connection of P,R st Con is co-Galois
for f being map of P,R, g being map of R,P st Con = [f,g] holds
f = f * (g * f) & g = g * (f * g);

theorem :: CONLAT_1:15
for C being FormalContext holds [phi(C),psi(C)] is co-Galois;

theorem :: CONLAT_1:16
for C being FormalContext
for O1,O2 being Subset of the Objects of C holds
(ObjectDerivation(C)).(O1 \/ O2) =
((ObjectDerivation(C)).O1) /\ ((ObjectDerivation(C)).O2);

theorem :: CONLAT_1:17
for C being FormalContext
for A1,A2 being Subset of the Attributes of C holds
(AttributeDerivation(C)).(A1 \/ A2) =
((AttributeDerivation(C)).A1) /\ ((AttributeDerivation(C)).A2);

theorem :: CONLAT_1:18
for C being FormalContext holds
(ObjectDerivation(C)).{} = the Attributes of C;

theorem :: CONLAT_1:19
for C being FormalContext holds
(AttributeDerivation(C)).{} = the Objects of C;

begin :: Formal Concepts

definition
let C be 2-sorted;
struct ConceptStr over C
(# Extent -> Subset of the Objects of C,
Intent -> Subset of the Attributes of C #);
end;

definition
let C be 2-sorted;
let CP be ConceptStr over C;
attr CP is empty means
:: CONLAT_1:def 11
the Extent of CP is empty & the Intent of CP is empty;
attr CP is quasi-empty means
:: CONLAT_1:def 12
the Extent of CP is empty or the Intent of CP is empty;
end;

definition
let C be non quasi-empty 2-sorted;
cluster strict non empty ConceptStr over C;
cluster strict quasi-empty ConceptStr over C;
end;

definition
let C be empty 2-sorted;
cluster -> empty ConceptStr over C;
end;

definition
let C be quasi-empty 2-sorted;
cluster -> quasi-empty ConceptStr over C;
end;

definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is concept-like means
:: CONLAT_1:def 13
(ObjectDerivation(C)).(the Extent of CP) = the Intent of CP &
(AttributeDerivation(C)).(the Intent of CP) = the Extent of CP;
end;

definition
let C be FormalContext;
cluster concept-like non empty ConceptStr over C;
end;

definition
let C be FormalContext;
mode FormalConcept of C is concept-like non empty ConceptStr over C;
end;

definition
let C be FormalContext;
cluster strict FormalConcept of C;
end;

theorem :: CONLAT_1:20
for C being FormalContext
for O being Subset of the Objects of C holds
ConceptStr(#(AttributeDerivation(C)).((ObjectDerivation(C)).O),
(ObjectDerivation(C)).O#)
is FormalConcept of C &
for O' being Subset of the Objects of C,
A' being Subset of the Attributes of C
st ConceptStr(#O',A'#) is FormalConcept of C & O c= O'
holds (AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O';

theorem :: CONLAT_1:21
for C being FormalContext
for O being Subset of the Objects of C holds
(ex A being Subset of the Attributes of C
st ConceptStr(#O,A#) is FormalConcept of C) iff
(AttributeDerivation(C)).((ObjectDerivation(C)).O) = O;

theorem :: CONLAT_1:22
for C being FormalContext
for A being Subset of the Attributes of C holds
ConceptStr(#(AttributeDerivation(C)).A,
(ObjectDerivation(C)).((AttributeDerivation(C)).A)#)
is FormalConcept of C &
for O' being Subset of the Objects of C,
A' being Subset of the Attributes of C
st ConceptStr(#O',A'#) is FormalConcept of C & A c= A'
holds (ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A';

theorem :: CONLAT_1:23
for C being FormalContext
for A being Subset of the Attributes of C holds
(ex O being Subset of the Objects 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 14
the Extent of CP = the Objects of C;
end;

definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is co-universal means
:: CONLAT_1:def 15
the Intent of CP = the Attributes of C;
end;

definition
let C be FormalContext;
cluster strict universal FormalConcept of C;
cluster strict co-universal FormalConcept of C;
end;

definition
let C be FormalContext;
func Concept-with-all-Objects(C)
-> strict universal FormalConcept of C means
:: CONLAT_1:def 16
ex O being Subset of the Objects of C,
A being Subset of the Attributes 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 17
ex O being Subset of the Objects of C,
A being Subset of the Attributes of C
st (it = ConceptStr(#O,A#) &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).({})) &
A = (ObjectDerivation(C)).({}));
end;

theorem :: CONLAT_1:24
for C being FormalContext holds
the Extent of Concept-with-all-Objects(C) = the Objects of C &
the Intent of Concept-with-all-Attributes(C) = the Attributes of C;

theorem :: CONLAT_1:25
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:26
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:27
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:28
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 18
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 19
the Extent of CP1 c= the Extent of CP2;
synonym CP2 is-SuperConcept-of CP1;
end;

canceled 2;

theorem :: CONLAT_1:31
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;

canceled;

theorem :: CONLAT_1:33
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:34
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 20
{ ConceptStr(#E,I#) where E is Subset of the Objects of C,
I is Subset of the Attributes 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;

definition
let C be FormalContext;
cluster B-carrier(C) -> non empty;
end;

theorem :: CONLAT_1:35
for C being FormalContext
for CP being set 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 21
for CP1,CP2 being strict FormalConcept of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes 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 22
for CP1,CP2 being strict FormalConcept of C holds
ex O being Subset of the Objects of C,
A being Subset of the Attributes 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:36
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:37
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:38
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:39
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:40
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:41
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:42
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:43
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:44
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:45
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 23
LattStr(#B-carrier(C),B-join(C),B-meet(C)#);
end;

theorem :: CONLAT_1:46
for C being FormalContext holds ConceptLattice(C) is Lattice;

definition
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 24
CP;
end;

theorem :: CONLAT_1:47
for C being FormalContext
for CP1,CP2 being Element of ConceptLattice(C) holds
CP1 [= CP2 iff CP1@ is-SubConcept-of CP2@;

theorem :: CONLAT_1:48
for C being FormalContext holds ConceptLattice(C) is complete Lattice;

definition
let C be FormalContext;
cluster ConceptLattice(C) -> complete;
end;
```