:: Introduction to Concept Lattices :: by Christoph Schwarzweller :: :: Received October 2, 1998 :: Copyright (c) 1998-2021 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;