:: CONLAT_2 semantic presentation

definition

let c₁ be FormalContext;
let c₂ be strict FormalConcept of c₁;
func @ c₂ -> Element of (ConceptLattice a₁) equals :: CONLAT_2:def 1
a₂;
coherence

proof end;

end;

:: deftheorem Def1 defines @ CONLAT_2:def 1 :

registration

let c₁ be FormalContext;
cluster ConceptLattice a₁ -> bounded ;
coherence

proof end;

end;

theorem Th1: :: CONLAT_2:1

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

proof end;

theorem Th2: :: CONLAT_2:2

for b₁ being FormalContext
for b₂ being non empty Subset-Family of the Objects of b₁ holds (ObjectDerivation b₁) . (union b₂) = meet { ((ObjectDerivation b₁) . b₃) where B is Subset of the Objects of b₁ : b₃ in b₂ }

proof end;

theorem Th3: :: CONLAT_2:3

for b₁ being FormalContext
for b₂ being non empty Subset-Family of the Attributes of b₁ holds (AttributeDerivation b₁) . (union b₂) = meet { ((AttributeDerivation b₁) . b₃) where B is Subset of the Attributes of b₁ : b₃ in b₂ }

proof end;

theorem Th4: :: CONLAT_2:4

for b₁ being FormalContext
for b₂ being Subset of (ConceptLattice b₁) holds
( "/\" b₂,(ConceptLattice b₁) is FormalConcept of b₁ & "\/" b₂,(ConceptLattice b₁) is FormalConcept of b₁ )

proof end;

definition

let c₁ be FormalContext;
let c₂ be Subset of (ConceptLattice c₁);
func "/\" c₂,c₁ -> FormalConcept of a₁ equals :: CONLAT_2:def 2
"/\" a₂,(ConceptLattice a₁);
coherence by Th4;
func "\/" c₂,c₁ -> FormalConcept of a₁ equals :: CONLAT_2:def 3
"\/" a₂,(ConceptLattice a₁);
coherence by Th4;

end;

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

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

theorem Th5: :: CONLAT_2:5

for b₁ being FormalContext holds
( "\/" ({} (ConceptLattice b₁)),b₁ = Concept-with-all-Attributes b₁ & "/\" ({} (ConceptLattice b₁)),b₁ = Concept-with-all-Objects b₁ )

proof end;

theorem Th6: :: CONLAT_2:6

for b₁ being FormalContext holds
( "\/" ([#] the carrier of (ConceptLattice b₁)),b₁ = Concept-with-all-Objects b₁ & "/\" ([#] the carrier of (ConceptLattice b₁)),b₁ = Concept-with-all-Attributes b₁ )

proof end;

theorem Th7: :: CONLAT_2:7

for b₁ being FormalContext
for b₂ being non empty Subset of (ConceptLattice b₁) holds
( the Extent of ("\/" b₂,b₁) = (AttributeDerivation b₁) . ((ObjectDerivation b₁) . (union { the Extent of ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ConceptStr(# b₃,b₄ #) in b₂ } )) & the Intent of ("\/" b₂,b₁) = meet { the Intent of ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ConceptStr(# b₃,b₄ #) in b₂ } )

proof end;

theorem Th8: :: CONLAT_2:8

for b₁ being FormalContext
for b₂ being non empty Subset of (ConceptLattice b₁) holds
( the Extent of ("/\" b₂,b₁) = meet { the Extent of ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ConceptStr(# b₃,b₄ #) in b₂ } & the Intent of ("/\" b₂,b₁) = (ObjectDerivation b₁) . ((AttributeDerivation b₁) . (union { the Intent of ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ConceptStr(# b₃,b₄ #) in b₂ } )) )

proof end;

theorem Th9: :: CONLAT_2:9

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds "\/" { ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ex b₁ being Object of b₁ st
( b₅ in the Extent of b₂ & b₃ = (AttributeDerivation b₁) . ((ObjectDerivation b₁) . {b₅}) & b₄ = (ObjectDerivation b₁) . {b₅} ) } ,(ConceptLattice b₁) = b₂

proof end;

theorem Th10: :: CONLAT_2:10

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds "/\" { ConceptStr(# b₃,b₄ #) where B is Subset of the Objects of b₁, B is Subset of the Attributes of b₁ : ex b₁ being Attribute of b₁ st
( b₅ in the Intent of b₂ & b₃ = (AttributeDerivation b₁) . {b₅} & b₄ = (ObjectDerivation b₁) . ((AttributeDerivation b₁) . {b₅}) ) } ,(ConceptLattice b₁) = b₂

proof end;

definition

let c₁ be FormalContext;
func gamma c₁ -> Function of the Objects of a₁,the carrier of (ConceptLattice a₁) means :Def4: :: CONLAT_2:def 4
for b₁ being Element of the Objects of a₁ ex b₂ being Subset of the Objects of a₁ex b₃ being Subset of the Attributes of a₁ st
( a₂ . b₁ = ConceptStr(# b₂,b₃ #) & b₂ = (AttributeDerivation a₁) . ((ObjectDerivation a₁) . {b₁}) & b₃ = (ObjectDerivation a₁) . {b₁} );
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 a₁,the carrier of (ConceptLattice a₁) means :Def5: :: CONLAT_2:def 5
for b₁ being Element of the Attributes of a₁ ex b₂ being Subset of the Objects of a₁ex b₃ being Subset of the Attributes of a₁ st
( a₂ . b₁ = ConceptStr(# b₂,b₃ #) & b₂ = (AttributeDerivation a₁) . {b₁} & b₃ = (ObjectDerivation a₁) . ((AttributeDerivation a₁) . {b₁}) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines delta CONLAT_2:def 5 :

theorem Th11: :: CONLAT_2:11

for b₁ being FormalContext
for b₂ being Object of b₁
for b₃ being Attribute of b₁ holds
( (gamma b₁) . b₂ is FormalConcept of b₁ & (delta b₁) . b₃ is FormalConcept of b₁ )

proof end;

theorem Th12: :: CONLAT_2:12

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

proof end;

theorem Th13: :: CONLAT_2:13

for b₁ being FormalContext
for b₂ being Object of b₁
for b₃ being Attribute of b₁ holds
( b₂ is-connected-with b₃ iff (gamma b₁) . b₂ [= (delta b₁) . b₃ )

proof end;

Lemma11: for b₁, b₂ being Lattice
for b₃ being Function of the carrier of b₁,the carrier of b₂ st ( for b₄, b₅ being Element of b₁ st b₃ . b₄ [= b₃ . b₅ holds
b₄ [= b₅ ) holds
b₃ is one-to-one

proof end;

Lemma12: for b₁, b₂ being complete Lattice
for b₃ being Function of the carrier of b₁,the carrier of b₂ st b₃ is one-to-one & rng b₃ = the carrier of b₂ & ( for b₄, b₅ being Element of b₁ holds
( b₄ [= b₅ iff b₃ . b₄ [= b₃ . b₅ ) ) holds
b₃ is Homomorphism of b₁,b₂

proof end;

Lemma13: for b₁ being FormalContext
for b₂ being ConceptStr of b₁ st (ObjectDerivation b₁) . the Extent of b₂ = the Intent of b₂ & (AttributeDerivation b₁) . the Intent of b₂ = the Extent of b₂ holds
not b₂ is empty

proof end;

theorem Th14: :: CONLAT_2:14

for b₁ being complete Lattice
for b₂ being FormalContext holds
( ConceptLattice b₂,b₁ are_isomorphic iff ex b₃ being Function of the Objects of b₂,the carrier of b₁ex b₄ being Function of the Attributes of b₂,the carrier of b₁ st
( rng b₃ is supremum-dense & rng b₄ is infimum-dense & ( for b₅ being Object of b₂
for b₆ being Attribute of b₂ holds
( b₅ is-connected-with b₆ iff b₃ . b₅ [= b₄ . b₆ ) ) ) )

proof end;

definition

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

end;

:: deftheorem Def6 defines Context CONLAT_2:def 6 :

theorem Th15: :: CONLAT_2:15

for b₁ being complete Lattice holds ConceptLattice (Context b₁),b₁ are_isomorphic

proof end;

theorem Th16: :: CONLAT_2:16

for b₁ being Lattice holds
( b₁ is complete iff ex b₂ being FormalContext st ConceptLattice b₂,b₁ are_isomorphic )

proof end;

registration

let c₁ be complete Lattice;
cluster a₁ .: -> 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 a₁,the Objects of a₁,(the Information of a₁ ~ ) #);
coherence by CONLAT_1:def 2;

end;

:: deftheorem Def7 defines .: CONLAT_2:def 7 :

theorem Th17: :: CONLAT_2:17

for b₁ being strict FormalContext holds (b₁ .: ) .: = b₁ ;

theorem Th18: :: CONLAT_2:18

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁ holds (ObjectDerivation b₁) . b₂ = (AttributeDerivation (b₁ .: )) . b₂

proof end;

theorem Th19: :: CONLAT_2:19

for b₁ being FormalContext
for b₂ being Subset of the Attributes of b₁ holds (AttributeDerivation b₁) . b₂ = (ObjectDerivation (b₁ .: )) . b₂

proof end;

definition

let c₁ be FormalContext;
let c₂ be ConceptStr of c₁;
func c₂ .: -> strict ConceptStr of a₁ .: means :Def8: :: CONLAT_2:def 8
( the Extent of a₃ = the Intent of a₂ & the Intent of a₃ = the Extent of a₂ );
existence

proof end;

uniqueness ;

end;

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

definition

let c₁ be FormalContext;
let c₂ be FormalConcept of c₁;
redefine func .: as c₂ .: -> strict FormalConcept of a₁ .: ;
coherence

proof end;

end;

theorem Th20: :: CONLAT_2:20

for b₁ being strict FormalContext
for b₂ being strict FormalConcept of b₁ holds (b₂ .: ) .: = b₂

proof end;

Lemma19: for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁
for b₃ being Subset of the Attributes of b₁ st ConceptStr(# b₂,b₃ #) is FormalConcept of b₁ holds
ConceptStr(# b₂,b₃ #) .: is FormalConcept of b₁ .:

proof end;

definition

let c₁ be FormalContext;
func DualHomomorphism c₁ -> Homomorphism of (ConceptLattice a₁) .: , ConceptLattice (a₁ .: ) means :Def9: :: CONLAT_2:def 9
for b₁ being strict FormalConcept of a₁ holds a₂ . b₁ = b₁ .: ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :

theorem Th21: :: CONLAT_2:21

for b₁ being FormalContext holds DualHomomorphism b₁ is isomorphism

proof end;

theorem Th22: :: CONLAT_2:22

for b₁ being FormalContext holds ConceptLattice (b₁ .: ),(ConceptLattice b₁) .: are_isomorphic

proof end;