begin
:: deftheorem CONLAT_1:def 1 :
canceled;
:: deftheorem Def2 defines quasi-empty CONLAT_1:def 2 :
:: deftheorem CONLAT_1:def 3 :
canceled;
:: deftheorem CONLAT_1:def 4 :
canceled;
:: deftheorem Def5 defines is-connected-with CONLAT_1:def 5 :
begin
:: deftheorem Def6 defines ObjectDerivation CONLAT_1:def 6 :
:: deftheorem Def7 defines AttributeDerivation CONLAT_1:def 7 :
theorem
theorem
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem
:: deftheorem defines phi CONLAT_1:def 8 :
:: deftheorem defines psi CONLAT_1:def 9 :
:: deftheorem Def10 defines co-Galois CONLAT_1:def 10 :
theorem
canceled;
theorem Th13:
theorem
theorem
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
begin
:: deftheorem Def11 defines empty CONLAT_1:def 11 :
:: deftheorem Def12 defines quasi-empty CONLAT_1:def 12 :
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
:: deftheorem Def13 defines concept-like CONLAT_1:def 13 :
theorem Th20:
theorem
theorem Th22:
theorem
:: deftheorem Def14 defines universal CONLAT_1:def 14 :
:: deftheorem Def15 defines co-universal CONLAT_1:def 15 :
:: deftheorem Def16 defines Concept-with-all-Objects CONLAT_1:def 16 :
:: deftheorem Def17 defines Concept-with-all-Attributes CONLAT_1:def 17 :
theorem Th24:
theorem
theorem Th26:
theorem
theorem
:: deftheorem Def18 defines Set-of-FormalConcepts CONLAT_1:def 18 :
:: deftheorem Def19 defines is-SubConcept-of CONLAT_1:def 19 :
theorem
canceled;
theorem
canceled;
theorem Th31:
theorem
canceled;
theorem
theorem
begin
:: deftheorem defines B-carrier CONLAT_1:def 20 :
theorem Th35:
definition
let C be
FormalContext;
func B-meet C -> BinOp of
(B-carrier C) means :
Def21:
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 b1 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
( b1 . 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)) )
uniqueness
for b1, b2 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
( b1 . 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
( b2 . 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
b1 = b2
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:
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 b1 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
( b1 . 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 )
uniqueness
for b1, b2 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
( b1 . 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
( b2 . 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
b1 = b2
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)
Lm3:
for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-join C) . CP1,CP2 in rng (B-join C)
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 )
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem
theorem Th43:
theorem
theorem
:: deftheorem defines ConceptLattice CONLAT_1:def 23 :
theorem Th46:
:: deftheorem defines @ CONLAT_1:def 24 :
theorem Th47:
theorem Th48: