:: Introduction to Concept Lattices
:: by Christoph Schwarzweller
::
:: Received October 2, 1998
:: Copyright (c) 1998-2011 Association of Mizar Users

begin

definition

let C be 2-sorted ;
canceled;
attr C is quasi-empty means :Def2: :: CONLAT_1:def 2
( the carrier of C is empty or the carrier' of C is empty );

end;

:: deftheorem CONLAT_1:def 1 :
canceled;

:: deftheorem Def2 defines quasi-empty CONLAT_1:def 2 :
for C being 2-sorted holds
( C is quasi-empty iff ( the carrier of C is empty or the carrier' of C is empty ) );

registration

cluster non empty strict non void 2-sorted ;
existence
ex b₁ being 2-sorted st
( b₁ is strict & not b₁ is empty & not b₁ is void )

proof end;

cluster strict non quasi-empty 2-sorted ;
existence
ex b₁ being 2-sorted st
( b₁ is strict & not b₁ is quasi-empty )

proof end;

end;

registration

cluster empty strict void quasi-empty 2-sorted ;
existence
ex b₁ being 2-sorted st
( b₁ is strict & b₁ is empty & b₁ is void & b₁ is quasi-empty )

proof end;

end;

definition

attr c₁ is strict ;
struct ContextStr -> 2-sorted ;
aggr ContextStr(# carrier, carrier', Information #) -> ContextStr ;
sel Information c₁ -> Relation of the carrier of c₁, the carrier' of c₁;

end;

registration

cluster non empty strict ContextStr ;
existence
ex b₁ being ContextStr st
( b₁ is strict & not b₁ is empty )

proof end;

cluster non quasi-empty strict ContextStr ;
existence
ex b₁ being ContextStr st
( b₁ is strict & not b₁ is quasi-empty )

proof end;

end;

definition

mode FormalContext is non quasi-empty 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 quasi-empty 2-sorted ;
cluster the carrier' of C -> non empty ;
coherence
not the carrier' of C is empty by Def2;
cluster the carrier of C -> non empty ;
coherence
not the carrier of C is empty by Def2;

end;

registration

let C be non quasi-empty 2-sorted ;
cluster non empty Element of bool the carrier of C;
existence
not for b₁ being Subset of the carrier of C holds b₁ is empty

proof end;

cluster non empty Element of bool the carrier' of C;
existence
not for b₁ being Subset of the carrier' of C holds b₁ is empty

proof end;

end;

definition

let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
canceled;
canceled;
pred o is-connected-with a means :Def5: :: CONLAT_1:def 5
[o,a] in the Information of C;

end;

:: deftheorem CONLAT_1:def 3 :
canceled;

:: deftheorem CONLAT_1:def 4 :
canceled;

:: deftheorem Def5 defines is-connected-with CONLAT_1:def 5 :
for C being FormalContext
for o being Object of C
for a being Attribute of C holds
( o is-connected-with a iff [o,a] in the Information of C );

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;

begin

definition

let C be FormalContext;
func ObjectDerivation C -> Function of (bool the carrier of C),(bool the carrier' of C) means :Def6: :: CONLAT_1:def 6
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 } ;
existence
ex b₁ being Function of (bool the carrier of C),(bool the carrier' of C) st
for O being Subset of the carrier of C holds b₁ . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }

proof end;

uniqueness
for b₁, b₂ being Function of (bool the carrier of C),(bool the carrier' of C) st ( for O being Subset of the carrier of C holds b₁ . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ) & ( for O being Subset of the carrier of C holds b₂ . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines ObjectDerivation CONLAT_1:def 6 :
for C being FormalContext
for b₂ being Function of (bool the carrier of C),(bool the carrier' of C) holds
( b₂ = ObjectDerivation C iff for O being Subset of the carrier of C holds b₂ . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } );

definition

let C be FormalContext;
func AttributeDerivation C -> Function of (bool the carrier' of C),(bool the carrier of C) means :Def7: :: CONLAT_1:def 7
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 } ;
existence
ex b₁ being Function of (bool the carrier' of C),(bool the carrier of C) st
for A being Subset of the carrier' of C holds b₁ . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }

proof end;

uniqueness
for b₁, b₂ being Function of (bool the carrier' of C),(bool the carrier of C) st ( for A being Subset of the carrier' of C holds b₁ . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ) & ( for A being Subset of the carrier' of C holds b₂ . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines AttributeDerivation CONLAT_1:def 7 :
for C being FormalContext
for b₂ being Function of (bool the carrier' of C),(bool the carrier of C) holds
( b₂ = AttributeDerivation C iff for A being Subset of the carrier' of C holds b₂ . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } );

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 }

proof end;

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 }

proof end;

theorem Th3: :: CONLAT_1:3

for C being FormalContext
for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1

proof end;

theorem Th4: :: CONLAT_1:4

for C being FormalContext
for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1

proof end;

theorem Th5: :: CONLAT_1:5

for C being FormalContext
for O being Subset of the carrier of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)

proof end;

theorem Th6: :: CONLAT_1:6

for C being FormalContext
for A being Subset of the carrier' of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)

proof end;

theorem Th7: :: 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))

proof end;

theorem Th8: :: 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))

proof end;

theorem Th9: :: 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 )

proof end;

theorem Th10: :: 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 )

proof end;

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 )

proof end;

definition

let C be FormalContext;
func phi C -> Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) equals :: CONLAT_1:def 8
ObjectDerivation C;
coherence
ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C)

proof end;

end;

:: deftheorem defines phi CONLAT_1:def 8 :
for C being FormalContext holds phi C = ObjectDerivation C;

definition

let C be FormalContext;
func psi C -> Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) equals :: CONLAT_1:def 9
AttributeDerivation C;
coherence
AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C)

proof end;

end;

:: deftheorem defines psi CONLAT_1:def 9 :
for C being FormalContext holds psi C = AttributeDerivation C;

definition

let P, R be non empty RelStr ;
let Con be Connection of P,R;
attr Con is co-Galois means :Def10: :: CONLAT_1:def 10
ex f being Function of P,R ex g being Function of R,P st
( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) );

end;

:: deftheorem Def10 defines co-Galois CONLAT_1:def 10 :
for P, R being non empty RelStr
for Con being Connection of P,R holds
( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st
( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) );

theorem :: CONLAT_1:12

canceled;

theorem Th13: :: CONLAT_1:13

for P, R being non empty Poset
for Con being Connection of P,R
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )

proof end;

theorem :: CONLAT_1:14

for P, R being non empty Poset
for Con being Connection of P,R st Con is co-Galois holds
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )

proof end;

theorem :: CONLAT_1:15

for C being FormalContext holds [(phi C),(psi C)] is co-Galois

proof end;

theorem Th16: :: CONLAT_1:16

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)

proof end;

theorem Th17: :: CONLAT_1:17

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)

proof end;

theorem Th18: :: CONLAT_1:18

for C being FormalContext holds (ObjectDerivation C) . {} = the carrier' of C

proof end;

theorem Th19: :: CONLAT_1:19

for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C

proof end;

begin

definition

let C be 2-sorted ;
attr c₂ is strict ;
struct ConceptStr of C -> ;
aggr ConceptStr(# Extent, Intent #) -> ConceptStr of C;
sel Extent c₂ -> Subset of the carrier of C;
sel Intent c₂ -> Subset of the carrier' of C;

end;

definition

let C be 2-sorted ;
let CP be ConceptStr of C;
attr CP is empty means :Def11: :: CONLAT_1:def 11
( the Extent of CP is empty & the Intent of CP is empty );
attr CP is quasi-empty means :Def12: :: CONLAT_1:def 12
( the Extent of CP is empty or the Intent of CP is empty );

end;

:: deftheorem Def11 defines empty CONLAT_1:def 11 :
for C being 2-sorted
for CP being ConceptStr of C holds
( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) );

:: deftheorem Def12 defines quasi-empty CONLAT_1:def 12 :
for C being 2-sorted
for CP being ConceptStr of C holds
( CP is quasi-empty iff ( the Extent of CP is empty or the Intent of CP is empty ) );

registration

let C be non quasi-empty 2-sorted ;
cluster strict non empty ConceptStr of C;
existence
ex b₁ being ConceptStr of C st
( b₁ is strict & not b₁ is empty )

proof end;

cluster strict quasi-empty ConceptStr of C;
existence
ex b₁ being ConceptStr of C st
( b₁ is strict & b₁ is quasi-empty )

proof end;

end;

registration

let C be empty void 2-sorted ;
cluster -> empty ConceptStr of C;
coherence
for b₁ being ConceptStr of C holds b₁ is empty

proof end;

end;

registration

let C be quasi-empty 2-sorted ;
cluster -> quasi-empty ConceptStr of C;
coherence
for b₁ being ConceptStr of C holds b₁ is quasi-empty

proof end;

end;

Lm1: for C being FormalContext
for CS being ConceptStr of C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty

proof end;

definition

let C be FormalContext;
let CP be ConceptStr of C;
attr CP is concept-like means :Def13: :: 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;

:: deftheorem Def13 defines concept-like CONLAT_1:def 13 :
for C being FormalContext
for CP being ConceptStr of C holds
( CP is concept-like iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) );

registration

let C be FormalContext;
cluster non empty concept-like ConceptStr of C;
existence
ex b₁ being ConceptStr of C st
( b₁ is concept-like & not b₁ is empty )

proof end;

end;

definition

let C be FormalContext;
mode FormalConcept of C is non empty concept-like ConceptStr of C;

end;

registration

let C be FormalContext;
cluster strict non empty concept-like ConceptStr of C;
existence
ex b₁ being FormalConcept of C st b₁ is strict

proof end;

end;

theorem Th20: :: CONLAT_1:20

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
for 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 ) )

proof end;

theorem :: CONLAT_1:21

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 )

proof end;

theorem Th22: :: CONLAT_1:22

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
for 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 ) )

proof end;

theorem :: CONLAT_1:23

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 )

proof end;

definition

let C be FormalContext;
let CP be ConceptStr of C;
attr CP is universal means :Def14: :: CONLAT_1:def 14
the Extent of CP = the carrier of C;

end;

:: deftheorem Def14 defines universal CONLAT_1:def 14 :
for C being FormalContext
for CP being ConceptStr of C holds
( CP is universal iff the Extent of CP = the carrier of C );

definition

let C be FormalContext;
let CP be ConceptStr of C;
attr CP is co-universal means :Def15: :: CONLAT_1:def 15
the Intent of CP = the carrier' of C;

end;

:: deftheorem Def15 defines co-universal CONLAT_1:def 15 :
for C being FormalContext
for CP being ConceptStr of C holds
( CP is co-universal iff the Intent of CP = the carrier' of C );

registration

let C be FormalContext;
cluster strict non empty concept-like universal ConceptStr of C;
existence
ex b₁ being FormalConcept of C st
( b₁ is strict & b₁ is universal )

proof end;

cluster strict non empty concept-like co-universal ConceptStr of C;
existence
ex b₁ being FormalConcept of C st
( b₁ is strict & b₁ is co-universal )

proof end;

end;

definition

let C be FormalContext;
func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def16: :: CONLAT_1:def 16
ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) );
existence
ex b₁ being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) )

proof end;

uniqueness
for b₁, b₂ being strict universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) holds
b₁ = b₂ ;

end;

:: deftheorem Def16 defines Concept-with-all-Objects CONLAT_1:def 16 :
for C being FormalContext
for b₂ being strict universal FormalConcept of C holds
( b₂ = Concept-with-all-Objects C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) );

definition

let C be FormalContext;
func Concept-with-all-Attributes C -> strict co-universal FormalConcept of C means :Def17: :: CONLAT_1:def 17
ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} );
existence
ex b₁ being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} )

proof end;

uniqueness
for b₁, b₂ being strict co-universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) & ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) holds
b₁ = b₂ ;

end;

:: deftheorem Def17 defines Concept-with-all-Attributes CONLAT_1:def 17 :
for C being FormalContext
for b₂ being strict co-universal FormalConcept of C holds
( b₂ = Concept-with-all-Attributes C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) );

theorem Th24: :: CONLAT_1:24

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 )

proof end;

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 ) )

proof end;

theorem Th26: :: 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 ) )

proof end;

theorem :: CONLAT_1:27

for C being FormalContext
for CP being quasi-empty ConceptStr of C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )

proof end;

theorem :: CONLAT_1:28

for C being FormalContext
for CP being quasi-empty ConceptStr of C holds
( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )

proof end;

definition

let C be FormalContext;
mode Set-of-FormalConcepts of C -> non empty set means :Def18: :: CONLAT_1:def 18
for X being set st X in it holds
X is FormalConcept of C;
existence
ex b₁ being non empty set st
for X being set st X in b₁ holds
X is FormalConcept of C

proof end;

end;

:: deftheorem Def18 defines Set-of-FormalConcepts CONLAT_1:def 18 :
for C being FormalContext
for b₂ being non empty set holds
( b₂ is Set-of-FormalConcepts of C iff for X being set st X in b₂ holds
X is FormalConcept of C );

definition

let C be FormalContext;
let FCS be Set-of-FormalConcepts of C;
:: original: Element
redefine mode Element of FCS -> FormalConcept of C;
coherence
for b₁ being Element of FCS holds b₁ is FormalConcept of C by Def18;

end;

definition

let C be FormalContext;
let CP1, CP2 be FormalConcept of C;
pred CP1 is-SubConcept-of CP2 means :Def19: :: CONLAT_1:def 19
the Extent of CP1 c= the Extent of CP2;

end;

:: deftheorem Def19 defines is-SubConcept-of CONLAT_1:def 19 :
for C being FormalContext
for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 );

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:29

canceled;

theorem :: CONLAT_1:30

canceled;

theorem Th31: :: 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 )

proof end;

theorem :: CONLAT_1:32

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 ) by Th31;

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 )

proof end;

begin

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 carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;
coherence
{ ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set

proof end;

end;

:: deftheorem defines B-carrier CONLAT_1:def 20 :
for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;

definition

let C be FormalContext;
:: original: B-carrier
redefine func B-carrier C -> Set-of-FormalConcepts of C;
coherence
B-carrier C is Set-of-FormalConcepts of C

proof end;

end;

registration

let C be FormalContext;
cluster B-carrier C -> non empty ;
coherence
not B-carrier C is empty ;

end;

theorem Th35: :: CONLAT_1:35

for C being FormalContext
for CP being set holds
( CP in B-carrier C iff CP is strict FormalConcept of C )

proof end;

definition

let C be FormalContext;
func B-meet C -> BinOp of (B-carrier C) means :Def21: :: CONLAT_1:def 21
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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)) );
existence
ex b₁ being BinOp of (B-carrier C) st
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ . (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)) )

proof end;

uniqueness
for b₁, b₂ being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ . (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)) ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . (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)) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def21 defines B-meet CONLAT_1:def 21 :
for C being FormalContext
for b₂ being BinOp of (B-carrier C) holds
( b₂ = B-meet C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . (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)) ) );

definition

let C be FormalContext;
func B-join C -> BinOp of (B-carrier C) means :Def22: :: CONLAT_1:def 22
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex 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 );
existence
ex b₁ being BinOp of (B-carrier C) st
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ . (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 )

proof end;

uniqueness
for b₁, b₂ being BinOp of (B-carrier C) st ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₁ . (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 ) ) & ( for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . (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 ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def22 defines B-join CONLAT_1:def 22 :
for C being FormalContext
for b₂ being BinOp of (B-carrier C) holds
( b₂ = B-join C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b₂ . (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 ) );

Lm2: for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) in rng (B-meet C)

proof end;

Lm3: for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)

proof end;

theorem Th36: :: 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)

proof end;

theorem Th37: :: 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)

proof end;

theorem Th38: :: 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)

proof end;

theorem Th39: :: 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)

proof end;

theorem Th40: :: 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

proof end;

theorem Th41: :: 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

proof end;

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

proof end;

theorem Th43: :: 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

proof end;

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

proof end;

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

proof end;

definition

let C be FormalContext;
func ConceptLattice C -> non empty strict LattStr equals :: CONLAT_1:def 23
LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
coherence
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr ;

end;

:: deftheorem defines ConceptLattice CONLAT_1:def 23 :
for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

theorem Th46: :: CONLAT_1:46

for C being FormalContext holds ConceptLattice C is Lattice

proof end;

registration

let C be FormalContext;
cluster ConceptLattice C -> non empty strict Lattice-like ;
coherence
( ConceptLattice C is strict & not ConceptLattice C is empty & ConceptLattice C is Lattice-like ) by Th46;

end;

definition

let C be FormalContext;
let S be non empty Subset of (ConceptLattice C);
:: original: Element
redefine mode Element of S -> FormalConcept of C;
coherence
for b₁ being Element of S holds b₁ is FormalConcept of C

proof end;

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;
coherence
CP is strict FormalConcept of C by Th35;

end;

:: deftheorem defines @ CONLAT_1:def 24 :
for C being FormalContext
for CP being Element of (ConceptLattice C) holds CP @ = CP;

theorem Th47: :: CONLAT_1:47

for C being FormalContext
for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )

proof end;

theorem Th48: :: CONLAT_1:48

for C being FormalContext holds ConceptLattice C is complete Lattice

proof end;

registration

let C be FormalContext;
cluster ConceptLattice C -> non empty strict complete ;
coherence
ConceptLattice C is complete by Th48;

end;