The abstract of the Mizar article:

A Characterization of Concept Lattices. Dual Concept Lattices

by

Christoph Schwarzweller

Received August 17, 1999

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;