:: CONLAT_1 semantic presentation

definition

attr c₁ is strict;
struct 2-sorted -> ;
aggr 2-sorted(# Objects, Attributes #) -> 2-sorted ;
sel Objects c₁ -> set ;
sel Attributes c₁ -> set ;

end;

definition

let C be 2-sorted ;
attr C is empty means :Def1: :: CONLAT_1:def 1
( the Objects of C is empty & the Attributes of C is empty );
attr C is quasi-empty means :Def2: :: CONLAT_1:def 2
( the Objects of C is empty or the Attributes of C is empty );

end;

:: deftheorem Def1 defines empty CONLAT_1:def 1 :

:: deftheorem Def2 defines quasi-empty CONLAT_1:def 2 :

registration

cluster strict non empty 2-sorted ;
existence

proof end;

cluster strict non quasi-empty 2-sorted ;
existence

proof end;

end;

registration

cluster strict empty quasi-empty 2-sorted ;
existence

proof end;

end;

definition

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

end;

registration

cluster non empty strict ContextStr ;
existence

proof end;

cluster non quasi-empty strict ContextStr ;
existence

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 the Objects of C;
mode Attribute of C is Element of the Attributes of C;

end;

registration

let C be non quasi-empty 2-sorted ;
cluster the Attributes of C -> non empty ;
coherence by Def2;
cluster the Objects of C -> non empty ;
coherence by Def2;

end;

registration

let C be non quasi-empty 2-sorted ;
cluster non empty Element of bool the Objects of C;
existence

proof end;

cluster non empty Element of bool the Attributes of C;
existence

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 :

:: deftheorem CONLAT_1:def 4 :

:: deftheorem Def5 defines is-connected-with CONLAT_1:def 5 :

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;

definition

let C be FormalContext;
func ObjectDerivation C -> Function of bool the Objects of C, bool the Attributes of C means :Def6: :: CONLAT_1:def 6
for O being Subset of 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 } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines ObjectDerivation CONLAT_1:def 6 :

definition

let C be FormalContext;
func AttributeDerivation C -> Function of bool the Attributes of C, bool the Objects of C means :Def7: :: CONLAT_1:def 7
for A being Subset of 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 } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines AttributeDerivation CONLAT_1:def 7 :

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

proof end;

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

proof end;

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 )

proof end;

definition

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

proof end;

end;

:: deftheorem defines phi CONLAT_1:def 8 :

definition

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

proof end;

end;

:: deftheorem defines psi CONLAT_1:def 9 :

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 :

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 Objects 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 Attributes 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 Attributes of C

proof end;

theorem Th19: :: CONLAT_1:19

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

proof end;

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 Objects of C;
sel Intent c₂ -> Subset of the Attributes 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 :

:: deftheorem Def12 defines quasi-empty CONLAT_1:def 12 :

registration

let C be non quasi-empty 2-sorted ;
cluster strict non empty ConceptStr of C;
existence

proof end;

cluster strict quasi-empty ConceptStr of C;
existence

proof end;

end;

registration

let C be empty 2-sorted ;
cluster -> empty ConceptStr of C;
coherence

proof end;

end;

registration

let C be quasi-empty 2-sorted ;
cluster -> quasi-empty ConceptStr of C;
coherence

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 & (AttributeDerivation C) . the Intent of CS = the Extent 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 :

registration

let C be FormalContext;
cluster non empty concept-like ConceptStr of C;
existence

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 ConceptStr of C;
existence

proof end;

end;

theorem Th20: :: 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
for 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' ) )

proof end;

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 )

proof end;

theorem Th22: :: 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
for 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' ) )

proof end;

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 )

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 Objects of C;

end;

:: deftheorem Def14 defines universal CONLAT_1:def 14 :

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 Attributes of C;

end;

:: deftheorem Def15 defines co-universal CONLAT_1:def 15 :

registration

let C be FormalContext;
cluster strict universal ConceptStr of C;
existence

proof end;

cluster strict co-universal ConceptStr of C;
existence

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 Objects of C ex A being Subset of the Attributes of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def16 defines Concept-with-all-Objects CONLAT_1:def 16 :

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 Objects of C ex A being Subset of the Attributes of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def17 defines Concept-with-all-Attributes CONLAT_1:def 17 :

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

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

proof end;

end;

:: deftheorem Def18 defines Set-of-FormalConcepts CONLAT_1:def 18 :

definition

let C be FormalContext;
let FCS be Set-of-FormalConcepts of C;
:: original: Element
redefine mode Element of FCS -> FormalConcept of C;
coherence 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 :

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;

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 : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;
coherence

proof end;

end;

:: deftheorem defines B-carrier CONLAT_1:def 20 :

definition

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

proof end;

end;

registration

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

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 Objects of C ex 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)) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def21 defines B-meet CONLAT_1:def 21 :

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 Objects of C ex 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 );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def22 defines B-join CONLAT_1:def 22 :

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;

Lm4: for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds
( (B-meet C) . CP1,CP2 is strict FormalConcept of C & (B-join C) . CP1,CP2 is strict FormalConcept of 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 ;

end;

:: deftheorem defines ConceptLattice CONLAT_1:def 23 :

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

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 by Th35;

end;

:: deftheorem defines @ CONLAT_1:def 24 :

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 Lattice-like complete ;
coherence by Th48;

end;