:: A Characterization of Concept Lattices; Dual Concept Lattices :: by Christoph Schwarzweller :: :: Received August 17, 1999 :: Copyright (c) 1999-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 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, LATTICE4; 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;