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;