:: CONLAT_1 semantic presentation

definition

attr a₁ 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 a₁ is empty means :Def1: :: CONLAT_1:def 1
( the Objects of a₁ is empty & the Attributes of a₁ is empty );
attr a₁ is quasi-empty means :Def2: :: CONLAT_1:def 2
( the Objects of a₁ is empty or the Attributes of a₁ 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 a₁ is strict;
struct ContextStr -> 2-sorted ;
aggr ContextStr(# Objects, Attributes, Information #) -> ContextStr ;
sel Information c₁ -> Relation of the Objects of a₁,the Attributes of a₁;

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

end;

registration

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

end;

registration

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

proof end;

cluster non empty Element of bool the Attributes of a₁;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def3 CONLAT_1:def 3 :

:: deftheorem Def4 CONLAT_1:def 4 :

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

notation

let c₁ be FormalContext;
let c₂ be Object of c₁;
let c₃ be Attribute of c₁;
antonym c₂ is-not-connected-with c₃ for c₂ is-connected-with c₃;

end;

definition

let c₁ be FormalContext;
func ObjectDerivation c₁ -> Function of bool the Objects of a₁, bool the Attributes of a₁ means :Def6: :: CONLAT_1:def 6
for b₁ being Subset of the Objects of a₁ holds a₂ . b₁ = { b₂ where B is Attribute of a₁ : for b₁ being Object of a₁ st b₃ in b₁ holds
b₃ is-connected-with b₂ } ;
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 a₁, bool the Objects of a₁ means :Def7: :: CONLAT_1:def 7
for b₁ being Subset of the Attributes of a₁ holds a₂ . b₁ = { b₂ where B is Object of a₁ : for b₁ being Attribute of a₁ st b₃ in b₁ holds
b₂ is-connected-with b₃ } ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines AttributeDerivation CONLAT_1:def 7 :

theorem Th1: :: CONLAT_1:1

for b₁ being FormalContext
for b₂ being Object of b₁ holds (ObjectDerivation b₁) . {b₂} = { b₃ where B is Attribute of b₁ : b₂ is-connected-with b₃ }

proof end;

theorem Th2: :: CONLAT_1:2

for b₁ being FormalContext
for b₂ being Attribute of b₁ holds (AttributeDerivation b₁) . {b₂} = { b₃ where B is Object of b₁ : b₃ is-connected-with b₂ }

proof end;

theorem Th3: :: CONLAT_1:3

for b₁ being FormalContext
for b₂, b₃ being Subset of the Objects of b₁ st b₂ c= b₃ holds
(ObjectDerivation b₁) . b₃ c= (ObjectDerivation b₁) . b₂

proof end;

theorem Th4: :: CONLAT_1:4

for b₁ being FormalContext
for b₂, b₃ being Subset of the Attributes of b₁ st b₂ c= b₃ holds
(AttributeDerivation b₁) . b₃ c= (AttributeDerivation b₁) . b₂

proof end;

theorem Th5: :: CONLAT_1:5

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

proof end;

theorem Th6: :: CONLAT_1:6

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

proof end;

theorem Th7: :: CONLAT_1:7

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

proof end;

theorem Th8: :: CONLAT_1:8

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

proof end;

theorem Th9: :: CONLAT_1:9

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁
for b₃ being Subset of the Attributes of b₁ holds
( b₂ c= (AttributeDerivation b₁) . b₃ iff [:b₂,b₃:] c= the Information of b₁ )

proof end;

theorem Th10: :: CONLAT_1:10

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁
for b₃ being Subset of the Attributes of b₁ holds
( b₃ c= (ObjectDerivation b₁) . b₂ iff [:b₂,b₃:] c= the Information of b₁ )

proof end;

theorem Th11: :: CONLAT_1:11

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁
for b₃ being Subset of the Attributes of b₁ holds
( b₂ c= (AttributeDerivation b₁) . b₃ iff b₃ c= (ObjectDerivation b₁) . b₂ )

proof end;

definition

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

proof end;

end;

:: deftheorem Def8 defines phi CONLAT_1:def 8 :

definition

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

proof end;

end;

:: deftheorem Def9 defines psi CONLAT_1:def 9 :

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Connection of c₁,c₂;
attr a₃ is co-Galois means :Def10: :: CONLAT_1:def 10
ex b₁ being Function of a₁,a₂ex b₂ being Function of a₂,a₁ st
( a₃ = [b₁,b₂] & b₁ is antitone & b₂ is antitone & ( for b₃, b₄ being Element of a₁
for b₅, b₆ being Element of a₂ holds
( b₃ <= b₂ . (b₁ . b₃) & b₅ <= b₁ . (b₂ . b₅) ) ) );

end;

:: deftheorem Def10 defines co-Galois CONLAT_1:def 10 :

theorem Th12: :: CONLAT_1:12

canceled;

theorem Th13: :: CONLAT_1:13

for b₁, b₂ being non empty Poset
for b₃ being Connection of b₁,b₂
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₁ st b₃ = [b₄,b₅] holds
( b₃ is co-Galois iff for b₆ being Element of b₁
for b₇ being Element of b₂ holds
( b₆ <= b₅ . b₇ iff b₇ <= b₄ . b₆ ) )

proof end;

theorem Th14: :: CONLAT_1:14

for b₁, b₂ being non empty Poset
for b₃ being Connection of b₁,b₂ st b₃ is co-Galois holds
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₁ st b₃ = [b₄,b₅] holds
( b₄ = b₄ * (b₅ * b₄) & b₅ = b₅ * (b₄ * b₅) )

proof end;

theorem Th15: :: CONLAT_1:15

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

proof end;

theorem Th16: :: CONLAT_1:16

for b₁ being FormalContext
for b₂, b₃ being Subset of the Objects of b₁ holds (ObjectDerivation b₁) . (b₂ \/ b₃) = ((ObjectDerivation b₁) . b₂) /\ ((ObjectDerivation b₁) . b₃)

proof end;

theorem Th17: :: CONLAT_1:17

for b₁ being FormalContext
for b₂, b₃ being Subset of the Attributes of b₁ holds (AttributeDerivation b₁) . (b₂ \/ b₃) = ((AttributeDerivation b₁) . b₂) /\ ((AttributeDerivation b₁) . b₃)

proof end;

theorem Th18: :: CONLAT_1:18

for b₁ being FormalContext holds (ObjectDerivation b₁) . {} = the Attributes of b₁

proof end;

theorem Th19: :: CONLAT_1:19

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

proof end;

definition

let c₁ be 2-sorted ;
attr a₂ is strict;
struct ConceptStr of c₁ -> ;
aggr ConceptStr(# Extent, Intent #) -> ConceptStr of a₁;
sel Extent c₂ -> Subset of the Objects of a₁;
sel Intent c₂ -> Subset of the Attributes of a₁;

end;

definition

let c₁ be 2-sorted ;
let c₂ be ConceptStr of c₁;
attr a₂ is empty means :Def11: :: CONLAT_1:def 11
( the Extent of a₂ is empty & the Intent of a₂ is empty );
attr a₂ is quasi-empty means :Def12: :: CONLAT_1:def 12
( the Extent of a₂ is empty or the Intent of a₂ 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 a₁;
existence

proof end;

cluster strict quasi-empty ConceptStr of a₁;
existence

proof end;

end;

registration

let c₁ be empty 2-sorted ;
cluster -> empty ConceptStr of a₁;
coherence

proof end;

end;

registration

let c₁ be quasi-empty 2-sorted ;
cluster -> quasi-empty ConceptStr of a₁;
coherence

proof end;

end;

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

definition

let c₁ be FormalContext;
let c₂ be ConceptStr of c₁;
attr a₂ is concept-like means :Def13: :: CONLAT_1:def 13
( (ObjectDerivation a₁) . the Extent of a₂ = the Intent of a₂ & (AttributeDerivation a₁) . the Intent of a₂ = the Extent of a₂ );

end;

:: deftheorem Def13 defines concept-like CONLAT_1:def 13 :

registration

let c₁ be FormalContext;
cluster non empty concept-like ConceptStr of a₁;
existence

proof end;

end;

definition

let c₁ be FormalContext;
mode FormalConcept of a₁ is non empty concept-like ConceptStr of a₁;

end;

registration

let c₁ be FormalContext;
cluster strict ConceptStr of a₁;
existence

proof end;

end;

theorem Th20: :: CONLAT_1:20

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁ holds
( ConceptStr(# ((AttributeDerivation b₁) . ((ObjectDerivation b₁) . b₂)),((ObjectDerivation b₁) . b₂) #) is FormalConcept of b₁ & ( 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₁ & b₂ c= b₃ holds
(AttributeDerivation b₁) . ((ObjectDerivation b₁) . b₂) c= b₃ ) )

proof end;

theorem Th21: :: CONLAT_1:21

for b₁ being FormalContext
for b₂ being Subset of the Objects of b₁ holds
( ex b₃ being Subset of the Attributes of b₁ st ConceptStr(# b₂,b₃ #) is FormalConcept of b₁ iff (AttributeDerivation b₁) . ((ObjectDerivation b₁) . b₂) = b₂ )

proof end;

theorem Th22: :: CONLAT_1:22

for b₁ being FormalContext
for b₂ being Subset of the Attributes of b₁ holds
( ConceptStr(# ((AttributeDerivation b₁) . b₂),((ObjectDerivation b₁) . ((AttributeDerivation b₁) . b₂)) #) is FormalConcept of b₁ & ( 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₁ & b₂ c= b₄ holds
(ObjectDerivation b₁) . ((AttributeDerivation b₁) . b₂) c= b₄ ) )

proof end;

theorem Th23: :: CONLAT_1:23

for b₁ being FormalContext
for b₂ being Subset of the Attributes of b₁ holds
( ex b₃ being Subset of the Objects of b₁ st ConceptStr(# b₃,b₂ #) is FormalConcept of b₁ iff (ObjectDerivation b₁) . ((AttributeDerivation b₁) . b₂) = b₂ )

proof end;

definition

let c₁ be FormalContext;
let c₂ be ConceptStr of c₁;
attr a₂ is universal means :Def14: :: CONLAT_1:def 14
the Extent of a₂ = the Objects of a₁;

end;

:: deftheorem Def14 defines universal CONLAT_1:def 14 :

definition

let c₁ be FormalContext;
let c₂ be ConceptStr of c₁;
attr a₂ is co-universal means :Def15: :: CONLAT_1:def 15
the Intent of a₂ = the Attributes of a₁;

end;

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

registration

let c₁ be FormalContext;
cluster strict universal ConceptStr of a₁;
existence

proof end;

cluster strict co-universal ConceptStr of a₁;
existence

proof end;

end;

definition

let c₁ be FormalContext;
func Concept-with-all-Objects c₁ -> strict universal FormalConcept of a₁ means :Def16: :: CONLAT_1:def 16
ex b₁ being Subset of the Objects of a₁ex b₂ being Subset of the Attributes of a₁ st
( a₂ = ConceptStr(# b₁,b₂ #) & b₁ = (AttributeDerivation a₁) . {} & b₂ = (ObjectDerivation a₁) . ((AttributeDerivation a₁) . {} ) );
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 a₁ means :Def17: :: CONLAT_1:def 17
ex b₁ being Subset of the Objects of a₁ex b₂ being Subset of the Attributes of a₁ st
( a₂ = ConceptStr(# b₁,b₂ #) & b₁ = (AttributeDerivation a₁) . ((ObjectDerivation a₁) . {} ) & b₂ = (ObjectDerivation a₁) . {} );
existence

proof end;

uniqueness ;

end;

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

theorem Th24: :: CONLAT_1:24

for b₁ being FormalContext holds
( the Extent of (Concept-with-all-Objects b₁) = the Objects of b₁ & the Intent of (Concept-with-all-Attributes b₁) = the Attributes of b₁ )

proof end;

theorem Th25: :: CONLAT_1:25

for b₁ being FormalContext
for b₂ being FormalConcept of b₁ holds
( ( the Extent of b₂ = {} implies b₂ is co-universal ) & ( the Intent of b₂ = {} implies b₂ is universal ) )

proof end;

theorem Th26: :: CONLAT_1:26

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds
( ( the Extent of b₂ = {} implies b₂ = Concept-with-all-Attributes b₁ ) & ( the Intent of b₂ = {} implies b₂ = Concept-with-all-Objects b₁ ) )

proof end;

theorem Th27: :: CONLAT_1:27

for b₁ being FormalContext
for b₂ being quasi-empty ConceptStr of b₁ holds
( not b₂ is FormalConcept of b₁ or b₂ is universal or b₂ is co-universal )

proof end;

theorem Th28: :: CONLAT_1:28

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

proof end;

definition

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

proof end;

end;

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

definition

let c₁ be FormalContext;
let c₂ be Set-of-FormalConcepts of c₁;
redefine mode Element as Element of c₂ -> FormalConcept of a₁;
coherence by Def18;

end;

definition

let c₁ be FormalContext;
let c₂, c₃ be FormalConcept of c₁;
pred c₂ is-SubConcept-of c₃ means :Def19: :: CONLAT_1:def 19
the Extent of a₂ c= the Extent of a₃;

end;

:: deftheorem Def19 defines is-SubConcept-of CONLAT_1:def 19 :

notation

let c₁ be FormalContext;
let c₂, c₃ be FormalConcept of c₁;
synonym c₃ is-SuperConcept-of c₂ for c₂ is-SubConcept-of c₃;

end;

theorem Th29: :: CONLAT_1:29

canceled;

theorem Th30: :: CONLAT_1:30

canceled;

theorem Th31: :: CONLAT_1:31

for b₁ being FormalContext
for b₂, b₃ being FormalConcept of b₁ holds
( b₂ is-SubConcept-of b₃ iff the Intent of b₃ c= the Intent of b₂ )

proof end;

theorem Th32: :: CONLAT_1:32

canceled;

theorem Th33: :: CONLAT_1:33

for b₁ being FormalContext
for b₂, b₃ being FormalConcept of b₁ holds
( b₂ is-SuperConcept-of b₃ iff the Intent of b₂ c= the Intent of b₃ ) by Th31;

theorem Th34: :: CONLAT_1:34

for b₁ being FormalContext
for b₂ being FormalConcept of b₁ holds
( b₂ is-SubConcept-of Concept-with-all-Objects b₁ & Concept-with-all-Attributes b₁ is-SubConcept-of b₂ )

proof end;

definition

let c₁ be FormalContext;
func B-carrier c₁ -> non empty set equals :: CONLAT_1:def 20
{ ConceptStr(# b₁,b₂ #) where B is Subset of the Objects of a₁, B is Subset of the Attributes of a₁ : ( not ConceptStr(# b₁,b₂ #) is empty & (ObjectDerivation a₁) . b₁ = b₂ & (AttributeDerivation a₁) . b₂ = b₁ ) } ;
coherence

proof end;

end;

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

definition

let c₁ be FormalContext;
redefine func B-carrier as B-carrier c₁ -> Set-of-FormalConcepts of a₁;
coherence

proof end;

end;

registration

let c₁ be FormalContext;
cluster B-carrier a₁ -> non empty ;
coherence ;

end;

theorem Th35: :: CONLAT_1:35

for b₁ being FormalContext
for b₂ being set holds
( b₂ in B-carrier b₁ iff b₂ is strict FormalConcept of b₁ )

proof end;

definition

let c₁ be FormalContext;
func B-meet c₁ -> BinOp of B-carrier a₁ means :Def21: :: CONLAT_1:def 21
for b₁, b₂ being strict FormalConcept of a₁ ex b₃ being Subset of the Objects of a₁ex b₄ being Subset of the Attributes of a₁ st
( a₂ . b₁,b₂ = ConceptStr(# b₃,b₄ #) & b₃ = the Extent of b₁ /\ the Extent of b₂ & b₄ = (ObjectDerivation a₁) . ((AttributeDerivation a₁) . (the Intent of b₁ \/ the Intent of b₂)) );
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 a₁ means :Def22: :: CONLAT_1:def 22
for b₁, b₂ being strict FormalConcept of a₁ ex b₃ being Subset of the Objects of a₁ex b₄ being Subset of the Attributes of a₁ st
( a₂ . b₁,b₂ = ConceptStr(# b₃,b₄ #) & b₃ = (AttributeDerivation a₁) . ((ObjectDerivation a₁) . (the Extent of b₁ \/ the Extent of b₂)) & b₄ = the Intent of b₁ /\ the Intent of b₂ );
existence

proof end;

uniqueness

proof end;

end;

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

Lemma38: for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,b₃ in rng (B-meet b₁)

proof end;

Lemma39: for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-join b₁) . b₂,b₃ in rng (B-join b₁)

proof end;

Lemma40: for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds
( (B-meet b₁) . b₂,b₃ is strict FormalConcept of b₁ & (B-join b₁) . b₂,b₃ is strict FormalConcept of b₁ )

proof end;

theorem Th36: :: CONLAT_1:36

for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,b₃ = (B-meet b₁) . b₃,b₂

proof end;

theorem Th37: :: CONLAT_1:37

for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-join b₁) . b₂,b₃ = (B-join b₁) . b₃,b₂

proof end;

theorem Th38: :: CONLAT_1:38

for b₁ being FormalContext
for b₂, b₃, b₄ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,((B-meet b₁) . b₃,b₄) = (B-meet b₁) . ((B-meet b₁) . b₂,b₃),b₄

proof end;

theorem Th39: :: CONLAT_1:39

for b₁ being FormalContext
for b₂, b₃, b₄ being strict FormalConcept of b₁ holds (B-join b₁) . b₂,((B-join b₁) . b₃,b₄) = (B-join b₁) . ((B-join b₁) . b₂,b₃),b₄

proof end;

theorem Th40: :: CONLAT_1:40

for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-join b₁) . ((B-meet b₁) . b₂,b₃),b₃ = b₃

proof end;

theorem Th41: :: CONLAT_1:41

for b₁ being FormalContext
for b₂, b₃ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,((B-join b₁) . b₂,b₃) = b₂

proof end;

theorem Th42: :: CONLAT_1:42

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,(Concept-with-all-Objects b₁) = b₂

proof end;

theorem Th43: :: CONLAT_1:43

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds (B-join b₁) . b₂,(Concept-with-all-Objects b₁) = Concept-with-all-Objects b₁

proof end;

theorem Th44: :: CONLAT_1:44

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds (B-join b₁) . b₂,(Concept-with-all-Attributes b₁) = b₂

proof end;

theorem Th45: :: CONLAT_1:45

for b₁ being FormalContext
for b₂ being strict FormalConcept of b₁ holds (B-meet b₁) . b₂,(Concept-with-all-Attributes b₁) = Concept-with-all-Attributes b₁

proof end;

definition

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

end;

:: deftheorem Def23 defines ConceptLattice CONLAT_1:def 23 :

theorem Th46: :: CONLAT_1:46

for b₁ being FormalContext holds ConceptLattice b₁ is Lattice

proof end;

registration

let c₁ be FormalContext;
cluster ConceptLattice a₁ -> non empty strict Lattice-like ;
coherence by Th46;

end;

definition

let c₁ be FormalContext;
let c₂ be non empty Subset of (ConceptLattice c₁);
redefine mode Element as Element of c₂ -> FormalConcept of a₁;
coherence

proof end;

end;

definition

let c₁ be FormalContext;
let c₂ be Element of (ConceptLattice c₁);
func c₂ @ -> strict FormalConcept of a₁ equals :: CONLAT_1:def 24
a₂;
coherence by Th35;

end;

:: deftheorem Def24 defines @ CONLAT_1:def 24 :

theorem Th47: :: CONLAT_1:47

for b₁ being FormalContext
for b₂, b₃ being Element of (ConceptLattice b₁) holds
( b₂ [= b₃ iff b₂ @ is-SubConcept-of b₃ @ )

proof end;

theorem Th48: :: CONLAT_1:48

for b₁ being FormalContext holds ConceptLattice b₁ is complete Lattice

proof end;

registration

let c₁ be FormalContext;
cluster ConceptLattice a₁ -> non empty strict Lattice-like complete ;
coherence by Th48;

end;