:: A Characterization of Concept Lattices; Dual Concept Lattices
:: by Christoph Schwarzweller
::
:: Received August 17, 1999
:: Copyright (c) 1999 Association of Mizar Users
:: deftheorem defines @ CONLAT_2:def 1 :
theorem Th1: :: CONLAT_2:1
theorem Th2: :: CONLAT_2:2
theorem Th3: :: CONLAT_2:3
theorem Th4: :: CONLAT_2:4
:: deftheorem defines "/\" CONLAT_2:def 2 :
:: deftheorem defines "\/" CONLAT_2:def 3 :
theorem :: CONLAT_2:5
theorem :: CONLAT_2:6
theorem :: CONLAT_2:7
theorem :: CONLAT_2:8
theorem Th9: :: CONLAT_2:9
theorem Th10: :: CONLAT_2:10
:: deftheorem Def4 defines gamma CONLAT_2:def 4 :
:: deftheorem Def5 defines delta CONLAT_2:def 5 :
theorem :: CONLAT_2:11
theorem Th12: :: CONLAT_2:12
theorem Th13: :: CONLAT_2:13
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
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
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
theorem Th14: :: CONLAT_2:14
:: deftheorem defines Context CONLAT_2:def 6 :
theorem Th15: :: CONLAT_2:15
theorem :: CONLAT_2:16
:: deftheorem defines .: CONLAT_2:def 7 :
theorem :: CONLAT_2:17
theorem Th18: :: CONLAT_2:18
theorem Th19: :: CONLAT_2:19
:: deftheorem Def8 defines .: CONLAT_2:def 8 :
theorem :: CONLAT_2:20
Lm4:
for C being FormalContext
for O being Subset of the carrier of C
for A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C holds
ConceptStr(# O,A #) .: is FormalConcept of C .:
:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :
theorem Th21: :: CONLAT_2:21
theorem :: CONLAT_2:22