:: CONLAT_2 semantic presentation

definition

let C be FormalContext;
let CP be strict FormalConcept of C;
func @ CP -> Element of (ConceptLattice C) equals :: CONLAT_2:def 1
CP;
coherence

proof end;

end;

:: deftheorem defines @ CONLAT_2:def 1 :

registration

let C be FormalContext;
cluster ConceptLattice C -> bounded ;
coherence

proof end;

end;

theorem Th1: :: CONLAT_2:1

for C being FormalContext holds
( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )

proof end;

theorem Th2: :: CONLAT_2:2

for C being FormalContext
for D being non empty Subset-Family of 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 }

proof end;

theorem Th3: :: CONLAT_2:3

for C being FormalContext
for D being non empty Subset-Family of 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 }

proof end;

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

proof end;

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);
coherence by Th4;
func "\/" D,C -> FormalConcept of C equals :: CONLAT_2:def 3
"\/" D,(ConceptLattice C);
coherence by Th4;

end;

:: deftheorem defines "/\" CONLAT_2:def 2 :

:: deftheorem defines "\/" CONLAT_2:def 3 :

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 )

proof end;

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 )

proof end;

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

proof end;

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

proof end;

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

proof end;

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

proof end;

definition

let C be FormalContext;
func gamma C -> Function of the Objects of C,the carrier of (ConceptLattice C) means :Def4: :: CONLAT_2:def 4
for o being Element of the Objects of C ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( it . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines gamma CONLAT_2:def 4 :

definition

let C be FormalContext;
func delta C -> Function of the Attributes of C,the carrier of (ConceptLattice C) means :Def5: :: CONLAT_2:def 5
for a being Element of the Attributes of C ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( it . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines delta CONLAT_2:def 5 :

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 )

proof end;

theorem Th12: :: CONLAT_2:12

for C being FormalContext holds
( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )

proof end;

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

proof end;

Lm1: for L1, L2 being Lattice
for f being Function of the carrier of L1,the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one

proof end;

Lm2: for L1, L2 being complete Lattice
for f being Function of the carrier of L1,the carrier of L2 st f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2

proof end;

Lm3: 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;

theorem Th14: :: 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 ex 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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )

proof end;

definition

let L be Lattice;
func Context L -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 6
ContextStr(# the carrier of L,the carrier of L,(LattRel L) #);
coherence by CONLAT_1:def 2;

end;

:: deftheorem defines Context CONLAT_2:def 6 :

theorem Th15: :: CONLAT_2:15

for L being complete Lattice holds ConceptLattice (Context L),L are_isomorphic

proof end;

theorem :: CONLAT_2:16

for L being Lattice holds
( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )

proof end;

registration

let L be complete Lattice;
cluster L .: -> complete ;
coherence

proof end;

end;

definition

let C be FormalContext;
func C .: -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 7
ContextStr(# the Attributes of C,the Objects of C,(the Information of C ~ ) #);
coherence by CONLAT_1:def 2;

end;

:: deftheorem defines .: CONLAT_2:def 7 :

theorem :: CONLAT_2:17

for C being strict FormalContext holds (C .: ) .: = C ;

theorem Th18: :: CONLAT_2:18

for C being FormalContext
for O being Subset of the Objects of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .: )) . O

proof end;

theorem Th19: :: CONLAT_2:19

for C being FormalContext
for A being Subset of the Attributes of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .: )) . A

proof end;

definition

let C be FormalContext;
let CP be ConceptStr of C;
func CP .: -> strict ConceptStr of C .: means :Def8: :: CONLAT_2:def 8
( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines .: CONLAT_2:def 8 :

definition

let C be FormalContext;
let CP be FormalConcept of C;
:: original: .:
redefine func CP .: -> strict FormalConcept of C .: ;
coherence

proof end;

end;

theorem :: CONLAT_2:20

for C being strict FormalContext
for CP being strict FormalConcept of C holds (CP .: ) .: = CP

proof end;

Lm4: for C being FormalContext
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 holds
ConceptStr(# O,A #) .: is FormalConcept of C .:

proof end;

definition

let C be FormalContext;
func DualHomomorphism C -> Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .: ) means :Def9: :: CONLAT_2:def 9
for CP being strict FormalConcept of C holds it . CP = CP .: ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :

theorem Th21: :: CONLAT_2:21

for C being FormalContext holds DualHomomorphism C is isomorphism

proof end;

theorem :: CONLAT_2:22

for C being FormalContext holds ConceptLattice (C .: ),(ConceptLattice C) .: are_isomorphic

proof end;