Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### A Characterization of Concept Lattices. Dual Concept Lattices

by
Christoph Schwarzweller

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

```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;

begin

definition
let C be FormalContext;
let CP be strict FormalConcept of C;
func @CP -> Element of ConceptLattice(C) equals
:: CONLAT_2:def 1
CP;
end;

definition let C be FormalContext;
cluster ConceptLattice C -> bounded;
end;

theorem :: CONLAT_2:1
for C being FormalContext holds
Bottom (ConceptLattice(C)) = Concept-with-all-Attributes(C) &
Top (ConceptLattice(C)) = Concept-with-all-Objects(C);

theorem :: CONLAT_2:2
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});

theorem :: CONLAT_2:3
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});

theorem :: CONLAT_2:4
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;

definition
let C be FormalContext;
let D be Subset of ConceptLattice(C);
func "/\"(D,C) -> FormalConcept of C equals
:: CONLAT_2:def 2
"/\"(D,ConceptLattice(C));
func "\/"(D,C) -> FormalConcept of C equals
:: CONLAT_2:def 3
"\/"(D,ConceptLattice(C));
end;

theorem :: CONLAT_2:5
for C being FormalContext holds
"\/"({} ConceptLattice(C),C) = Concept-with-all-Attributes(C) &
"/\"({} ConceptLattice(C),C) = Concept-with-all-Objects(C);

theorem :: CONLAT_2:6
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);

theorem :: CONLAT_2:7
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};

theorem :: CONLAT_2:8
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});

theorem :: CONLAT_2:9
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;

theorem :: CONLAT_2:10
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;

definition
let C be FormalContext;
func gamma(C) -> Function of the Objects of C,
the carrier of ConceptLattice(C) means
:: CONLAT_2:def 4
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};
end;

definition
let C be FormalContext;
func delta(C) -> Function of the Attributes of C,
the carrier of ConceptLattice(C) means
:: CONLAT_2:def 5
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});
end;

theorem :: CONLAT_2:11
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;

theorem :: CONLAT_2:12
for C being FormalContext holds
rng(gamma(C)) is supremum-dense & rng(delta(C)) is infimum-dense;

theorem :: CONLAT_2:13
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;

begin

theorem :: CONLAT_2:14
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;

definition
let L be Lattice;
func Context(L) -> strict non quasi-empty ContextStr equals
:: CONLAT_2:def 6
ContextStr(#the carrier of L, the carrier of L, LattRel L#);
end;

theorem :: CONLAT_2:15
for L being complete Lattice holds
ConceptLattice(Context(L)),L are_isomorphic;

theorem :: CONLAT_2:16
for L being Lattice holds
L is complete iff
ex C being FormalContext st ConceptLattice(C),L are_isomorphic;

begin :: Dual Concept Lattices

definition
let L be complete Lattice;
cluster L.: -> complete;
end;

definition
let C be FormalContext;
func C.: -> strict non quasi-empty ContextStr equals
:: CONLAT_2:def 7
ContextStr(#the Attributes of C, the Objects of C,
(the Information of C)~ #);
end;

theorem :: CONLAT_2:17
for C being strict FormalContext holds (C.:).: = C;

theorem :: CONLAT_2:18
for C being FormalContext
for O being Subset of the Objects of C holds
(ObjectDerivation(C)).O = (AttributeDerivation(C.:)).O;

theorem :: CONLAT_2:19
for C being FormalContext
for A being Subset of the Attributes of C holds
(AttributeDerivation(C)).A = (ObjectDerivation(C.:)).A;

definition
let C be FormalContext;
let CP be ConceptStr over C;
func CP.: -> strict ConceptStr over C.: means
:: CONLAT_2:def 8
the Extent of it = the Intent of CP &
the Intent of it = the Extent of CP;
end;

definition
let C be FormalContext;
let CP be FormalConcept of C;
redefine func CP.: -> strict FormalConcept of C.:;
end;

theorem :: CONLAT_2:20
for C being FormalContext
for CP being strict FormalConcept of C holds (CP.:).: = CP;

definition
let C be FormalContext;
func DualHomomorphism(C) ->
Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:) means
:: CONLAT_2:def 9
for CP being strict FormalConcept of C holds it.CP = CP.:;
end;

theorem :: CONLAT_2:21
for C being FormalContext holds DualHomomorphism(C) is isomorphism;

theorem :: CONLAT_2:22
for C being FormalContext holds
ConceptLattice(C.:),(ConceptLattice(C)).: are_isomorphic;

```