:: by Christoph Schwarzweller

::

:: Received August 17, 1999

:: Copyright (c) 1999-2021 Association of Mizar Users

definition

let C be FormalContext;

let CP be strict FormalConcept of C;

coherence

CP is Element of (ConceptLattice C)

end;
let CP be strict FormalConcept of C;

coherence

CP is Element of (ConceptLattice C)

proof end;

:: deftheorem defines @ CONLAT_2:def 1 :

for C being FormalContext

for CP being strict FormalConcept of C holds @ CP = CP;

for C being FormalContext

for CP being strict FormalConcept of C holds @ CP = CP;

theorem Th1: :: CONLAT_2:1

for C being FormalContext holds

( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )

( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )

proof end;

theorem Th2: :: CONLAT_2:2

for C being FormalContext

for D being non empty Subset-Family of the carrier of C holds (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }

for D being non empty Subset-Family of the carrier of C holds (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }

proof end;

theorem Th3: :: CONLAT_2:3

for C being FormalContext

for D being non empty Subset-Family of the carrier' of C holds (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }

for D being non empty Subset-Family of the carrier' of C holds (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }

proof end;

theorem Th4: :: CONLAT_2:4

for C being FormalContext

for D being Subset of (ConceptLattice C) holds

( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )

for D being Subset of (ConceptLattice C) holds

( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )

proof end;

definition

let C be FormalContext;

let D be Subset of (ConceptLattice C);

coherence

"/\" (D,(ConceptLattice C)) is FormalConcept of C by Th4;

coherence

"\/" (D,(ConceptLattice C)) is FormalConcept of C by Th4;

end;
let D be Subset of (ConceptLattice C);

coherence

"/\" (D,(ConceptLattice C)) is FormalConcept of C by Th4;

coherence

"\/" (D,(ConceptLattice C)) is FormalConcept of C by Th4;

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

for C being FormalContext

for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C));

for C being FormalContext

for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C));

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

for C being FormalContext

for D being Subset of (ConceptLattice C) holds "\/" (D,C) = "\/" (D,(ConceptLattice C));

for C being FormalContext

for D being Subset of (ConceptLattice C) holds "\/" (D,C) = "\/" (D,(ConceptLattice C));

theorem :: CONLAT_2:5

for C being FormalContext holds

( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C )

( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C )

proof end;

theorem :: CONLAT_2:6

for C being FormalContext holds

( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C )

( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C )

proof end;

theorem :: CONLAT_2:7

for C being FormalContext

for D being non empty Subset of (ConceptLattice C) holds

( the Extent of ("\/" (D,C)) = (AttributeDerivation C) . ((ObjectDerivation C) . (union { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) & the Intent of ("\/" (D,C)) = meet { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )

for D being non empty Subset of (ConceptLattice C) holds

( the Extent of ("\/" (D,C)) = (AttributeDerivation C) . ((ObjectDerivation C) . (union { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) & the Intent of ("\/" (D,C)) = meet { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )

proof end;

theorem :: CONLAT_2:8

for C being FormalContext

for D being non empty Subset of (ConceptLattice C) holds

( the Extent of ("/\" (D,C)) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) )

for D being non empty Subset of (ConceptLattice C) holds

( the Extent of ("/\" (D,C)) = meet { the Extent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } & the Intent of ("/\" (D,C)) = (ObjectDerivation C) . ((AttributeDerivation C) . (union { the Intent of ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(# E,I #) in D } )) )

proof end;

theorem Th9: :: CONLAT_2:9

for C being FormalContext

for CP being strict FormalConcept of C holds "\/" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st

( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(ConceptLattice C)) = CP

for CP being strict FormalConcept of C holds "\/" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex o being Object of C st

( o in the Extent of CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } ,(ConceptLattice C)) = CP

proof end;

theorem Th10: :: CONLAT_2:10

for C being FormalContext

for CP being strict FormalConcept of C holds "/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st

( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = CP

for CP being strict FormalConcept of C holds "/\" ( { ConceptStr(# O,A #) where O is Subset of the carrier of C, A is Subset of the carrier' of C : ex a being Attribute of C st

( a in the Intent of CP & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) } ,(ConceptLattice C)) = CP

proof end;

definition

let C be FormalContext;

ex b_{1} being Function of the carrier of C, the carrier of (ConceptLattice C) st

for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{1} . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )

for b_{1}, b_{2} being Function of the carrier of C, the carrier of (ConceptLattice C) st ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{1} . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{2} . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) holds

b_{1} = b_{2}

end;
func gamma C -> Function of the carrier of C, the carrier of (ConceptLattice C) means :Def4: :: CONLAT_2:def 4

for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( it . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} );

existence for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( it . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} );

ex b

for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def4 defines gamma CONLAT_2:def 4 :

for C being FormalContext

for b_{2} being Function of the carrier of C, the carrier of (ConceptLattice C) holds

( b_{2} = gamma C iff for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{2} . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) );

for C being FormalContext

for b

( b

( b

definition

let C be FormalContext;

ex b_{1} being Function of the carrier' of C, the carrier of (ConceptLattice C) st

for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{1} . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )

for b_{1}, b_{2} being Function of the carrier' of C, the carrier of (ConceptLattice C) st ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{1} . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{2} . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) holds

b_{1} = b_{2}

end;
func delta C -> Function of the carrier' of C, the carrier of (ConceptLattice C) means :Def5: :: CONLAT_2:def 5

for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( it . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) );

existence for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( it . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) );

ex b

for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def5 defines delta CONLAT_2:def 5 :

for C being FormalContext

for b_{2} being Function of the carrier' of C, the carrier of (ConceptLattice C) holds

( b_{2} = delta C iff for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

( b_{2} . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) );

for C being FormalContext

for b

( b

( b

theorem :: CONLAT_2:11

for C being FormalContext

for o being Object of C

for a being Attribute of C holds

( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )

for o being Object of C

for a being Attribute of C holds

( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )

proof end;

theorem Th12: :: CONLAT_2:12

for C being FormalContext holds

( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )

( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )

proof end;

theorem Th13: :: CONLAT_2:13

for C being FormalContext

for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff (gamma C) . o [= (delta C) . a )

for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff (gamma C) . o [= (delta C) . a )

proof end;

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

proof end;

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

proof end;

Lm3: for C being FormalContext

for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds

not CS is empty

proof end;

theorem Th14: :: CONLAT_2:14

for L being complete Lattice

for C being FormalContext holds

( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex d being Function of the carrier' of C, the carrier of L st

( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff g . o [= d . a ) ) ) )

for C being FormalContext holds

( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex d being Function of the carrier' of C, the carrier of L st

( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff g . o [= d . a ) ) ) )

proof end;

definition

let L be Lattice;

ContextStr(# the carrier of L, the carrier of L,(LattRel L) #) is non empty non void strict ContextStr ;

end;
func Context L -> non empty non void strict ContextStr equals :: CONLAT_2:def 6

ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);

coherence ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);

ContextStr(# the carrier of L, the carrier of L,(LattRel L) #) is non empty non void strict ContextStr ;

:: deftheorem defines Context CONLAT_2:def 6 :

for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);

for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);

theorem :: CONLAT_2:16

for L being Lattice holds

( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )

( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )

proof end;

registration
end;

definition

let C be FormalContext;

ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is non empty non void strict ContextStr ;

end;
func C .: -> non empty non void strict ContextStr equals :: CONLAT_2:def 7

ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);

coherence ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);

ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is non empty non void strict ContextStr ;

:: deftheorem defines .: CONLAT_2:def 7 :

for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);

for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);

theorem Th18: :: CONLAT_2:18

for C being FormalContext

for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O

for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O

proof end;

theorem Th19: :: CONLAT_2:19

for C being FormalContext

for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A

for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A

proof end;

definition

let C be FormalContext;

let CP be ConceptStr over C;

ex b_{1} being strict ConceptStr over C .: st

( the Extent of b_{1} = the Intent of CP & the Intent of b_{1} = the Extent of CP )

for b_{1}, b_{2} being strict ConceptStr over C .: st the Extent of b_{1} = the Intent of CP & the Intent of b_{1} = the Extent of CP & the Extent of b_{2} = the Intent of CP & the Intent of b_{2} = the Extent of CP holds

b_{1} = b_{2}
;

end;
let CP be ConceptStr over C;

func CP .: -> strict ConceptStr over C .: means :Def8: :: CONLAT_2:def 8

( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP );

existence ( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP );

ex b

( the Extent of b

proof end;

uniqueness for b

b

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

for C being FormalContext

for CP being ConceptStr over C

for b_{3} being strict ConceptStr over C .: holds

( b_{3} = CP .: iff ( the Extent of b_{3} = the Intent of CP & the Intent of b_{3} = the Extent of CP ) );

for C being FormalContext

for CP being ConceptStr over C

for b

( b

registration

let C be FormalContext;

let CP be FormalConcept of C;

coherence

( not CP .: is empty & CP .: is concept-like )

end;
let CP be FormalConcept of C;

coherence

( not CP .: is empty & CP .: is concept-like )

proof end;

definition

let C be FormalContext;

ex b_{1} being Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) st

for CP being strict FormalConcept of C holds b_{1} . CP = CP .:

for b_{1}, b_{2} being Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) st ( for CP being strict FormalConcept of C holds b_{1} . CP = CP .: ) & ( for CP being strict FormalConcept of C holds b_{2} . CP = CP .: ) holds

b_{1} = b_{2}

end;
func DualHomomorphism C -> Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) means :Def9: :: CONLAT_2:def 9

for CP being strict FormalConcept of C holds it . CP = CP .: ;

existence for CP being strict FormalConcept of C holds it . CP = CP .: ;

ex b

for CP being strict FormalConcept of C holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def 9 :

for C being FormalContext

for b_{2} being Homomorphism of ((ConceptLattice C) .:),(ConceptLattice (C .:)) holds

( b_{2} = DualHomomorphism C iff for CP being strict FormalConcept of C holds b_{2} . CP = CP .: );

for C being FormalContext

for b

( b