begin
:: deftheorem defines @ CONLAT_2:def 1 :
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
:: deftheorem defines "/\" CONLAT_2:def 2 :
:: deftheorem defines "\/" CONLAT_2:def 3 :
theorem
theorem
theorem
theorem
theorem Th9:
theorem Th10:
:: deftheorem Def4 defines gamma CONLAT_2:def 4 :
:: deftheorem Def5 defines delta CONLAT_2:def 5 :
theorem
theorem Th12:
theorem Th13:
begin
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 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
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 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
Lm3:
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
theorem Th14:
:: deftheorem defines Context CONLAT_2:def 6 :
theorem Th15:
theorem
begin
:: deftheorem defines .: CONLAT_2:def 7 :
theorem
theorem Th18:
theorem Th19:
:: deftheorem Def8 defines .: CONLAT_2:def 8 :
theorem
Lm4:
for C being FormalContext
for O being Subset of
for A being Subset of st ConceptStr(# O,A #) is FormalConcept of holds
ConceptStr(# O,A #) .: is FormalConcept of
:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :
theorem Th21:
theorem