:: A Characterization of Concept Lattices; Dual Concept Lattices
:: by Christoph Schwarzweller
::
:: Received August 17, 1999
:: Copyright (c) 1999-2017 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 CONLAT_1, STRUCT_0, QC_LANG1, SUBSET_1, LATTICES, XXREAL_2,
PBOOLE, EQREL_1, XBOOLE_0, SETFAM_1, FUNCT_1, TARSKI, CAT_1, LATTICE3,
ZFMISC_1, RELAT_1, FUNCT_3, LATTICE6, REWRITE1, GROUP_6, WELLORD1,
FUNCT_2, MCART_1, FILTER_1, XXREAL_0, ORDERS_2, CONLAT_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, XTUPLE_0, MCART_1,
FUNCT_1, DOMAIN_1, RELSET_1, ORDERS_2, STRUCT_0, LATTICE2, LATTICE3,
LATTICE6, PARTFUN1, FUNCT_2, LATTICES, LATTICE4, CONLAT_1;
constructors DOMAIN_1, LATTICE2, LATTICE4, CONLAT_1, LATTICE6, RELSET_1,
XTUPLE_0;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2,
LATTICE3, CONLAT_1, RELSET_1, XTUPLE_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;
registration
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-Family of
the carrier of C holds (ObjectDerivation(C)).(union D) = meet({(
ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D});
theorem :: CONLAT_2:3
for C being FormalContext for D being non empty Subset-Family of(
the carrier' of C) holds (AttributeDerivation(C)).(union D) = meet({(
AttributeDerivation(C)).A where A is Subset of the carrier' 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 carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}
) & the Intent of "\/"(D,C) = meet {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' 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 carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D} & the Intent of "/\"(D,C) = (
ObjectDerivation(C)).((AttributeDerivation(C)). union {the Intent of ConceptStr
(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' 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 carrier of C, A is
Subset of the carrier' 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 carrier of C, A is
Subset of the carrier' 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 carrier of C, the carrier of ConceptLattice
(C) means
:: CONLAT_2:def 4
for o being Element of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' 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 carrier' of C, the carrier of
ConceptLattice(C) means
:: CONLAT_2:def 5
for a being Element of the carrier' of C holds
ex O being Subset of the carrier of C, A being Subset of the carrier' 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 carrier of C,
the carrier of L, d being Function of the carrier' 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 empty non void 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
registration
let L be complete Lattice;
cluster L.: -> complete;
end;
definition
let C be FormalContext;
func C.: -> strict non empty non void ContextStr equals
:: CONLAT_2:def 7
ContextStr(#the
carrier' of C, the carrier 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 carrier of C
holds (ObjectDerivation(C)).O = (AttributeDerivation(C.:)).O;
theorem :: CONLAT_2:19
for C being FormalContext for A being Subset of the carrier' 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;
registration
let C be FormalContext;
let CP be FormalConcept of C;
cluster CP.: -> non empty concept-like;
end;
theorem :: CONLAT_2:20
for C being strict 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 bijective;
theorem :: CONLAT_2:22
for C being FormalContext holds ConceptLattice(C.:),(ConceptLattice(C)
).: are_isomorphic;