Volume 10, 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

### The abstract of the Mizar article:

### Introduction to Concept Lattices

**by****Christoph Schwarzweller**- Received October 2, 1998
- 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;

Back to top