:: by Christoph Schwarzweller

::

:: Received October 2, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

registration

existence

ex b_{1} being 2-sorted st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

proof end;

definition

attr c_{1} is strict ;

struct ContextStr -> 2-sorted ;

aggr ContextStr(# carrier, carrier', Information #) -> ContextStr ;

sel Information c_{1} -> Relation of the carrier of c_{1}, the carrier' of c_{1};

end;
struct ContextStr -> 2-sorted ;

aggr ContextStr(# carrier, carrier', Information #) -> ContextStr ;

sel Information c

registration

existence

ex b_{1} being ContextStr st

( b_{1} is strict & not b_{1} is empty & not b_{1} is void )

end;
ex b

( b

proof end;

definition

let C be 2-sorted ;

mode Object of C is Element of C;

mode Attribute of C is Element of the carrier' of C;

end;
mode Object of C is Element of C;

mode Attribute of C is Element of the carrier' of C;

registration

let C be non empty non void 2-sorted ;

coherence

not the carrier' of C is empty ;

coherence

not the carrier of C is empty ;

end;
coherence

not the carrier' of C is empty ;

coherence

not the carrier of C is empty ;

registration

let C be non empty non void 2-sorted ;

existence

not for b_{1} being Subset of the carrier of C holds b_{1} is empty

not for b_{1} being Subset of the carrier' of C holds b_{1} is empty

end;
existence

not for b

proof end;

existence not for b

proof end;

:: deftheorem defines is-connected-with CONLAT_1:def 2 :

for C being FormalContext

for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff [o,a] in the Information of C );

for C being FormalContext

for o being Object of C

for a being Attribute of C holds

( o is-connected-with a iff [o,a] in the Information of C );

notation

let C be FormalContext;

let o be Object of C;

let a be Attribute of C;

antonym o is-not-connected-with a for o is-connected-with a;

end;
let o be Object of C;

let a be Attribute of C;

antonym o is-not-connected-with a for o is-connected-with a;

definition

let C be FormalContext;

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

for O being Subset of the carrier of C holds b_{1} . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a }

for b_{1}, b_{2} being Function of (bool the carrier of C),(bool the carrier' of C) st ( for O being Subset of the carrier of C holds b_{1} . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a } ) & ( for O being Subset of the carrier of C holds b_{2} . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a } ) holds

b_{1} = b_{2}

end;
func ObjectDerivation C -> Function of (bool the carrier of C),(bool the carrier' of C) means :Def2: :: CONLAT_1:def 3

for O being Subset of the carrier of C holds it . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a } ;

existence for O being Subset of the carrier of C holds it . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a } ;

ex b

for O being Subset of the carrier of C holds b

o is-connected-with a }

proof end;

uniqueness for b

o is-connected-with a } ) & ( for O being Subset of the carrier of C holds b

o is-connected-with a } ) holds

b

proof end;

:: deftheorem Def2 defines ObjectDerivation CONLAT_1:def 3 :

for C being FormalContext

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

( b_{2} = ObjectDerivation C iff for O being Subset of the carrier of C holds b_{2} . O = { a where a is Attribute of C : for o being Object of C st o in O holds

o is-connected-with a } );

for C being FormalContext

for b

( b

o is-connected-with a } );

definition

let C be FormalContext;

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

for A being Subset of the carrier' of C holds b_{1} . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a }

for b_{1}, b_{2} being Function of (bool the carrier' of C),(bool the carrier of C) st ( for A being Subset of the carrier' of C holds b_{1} . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a } ) & ( for A being Subset of the carrier' of C holds b_{2} . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a } ) holds

b_{1} = b_{2}

end;
func AttributeDerivation C -> Function of (bool the carrier' of C),(bool the carrier of C) means :Def3: :: CONLAT_1:def 4

for A being Subset of the carrier' of C holds it . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a } ;

existence for A being Subset of the carrier' of C holds it . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a } ;

ex b

for A being Subset of the carrier' of C holds b

o is-connected-with a }

proof end;

uniqueness for b

o is-connected-with a } ) & ( for A being Subset of the carrier' of C holds b

o is-connected-with a } ) holds

b

proof end;

:: deftheorem Def3 defines AttributeDerivation CONLAT_1:def 4 :

for C being FormalContext

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

( b_{2} = AttributeDerivation C iff for A being Subset of the carrier' of C holds b_{2} . A = { o where o is Object of C : for a being Attribute of C st a in A holds

o is-connected-with a } );

for C being FormalContext

for b

( b

o is-connected-with a } );

theorem :: CONLAT_1:1

for C being FormalContext

for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }

for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }

proof end;

theorem :: CONLAT_1:2

for C being FormalContext

for a being Attribute of C holds (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }

for a being Attribute of C holds (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }

proof end;

theorem Th3: :: CONLAT_1:3

for C being FormalContext

for O1, O2 being Subset of the carrier of C st O1 c= O2 holds

(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1

for O1, O2 being Subset of the carrier of C st O1 c= O2 holds

(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1

proof end;

theorem Th4: :: CONLAT_1:4

for C being FormalContext

for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds

(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1

for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds

(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1

proof end;

theorem Th5: :: CONLAT_1:5

for C being FormalContext

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

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

proof end;

theorem Th6: :: CONLAT_1:6

for C being FormalContext

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

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

proof end;

theorem Th7: :: CONLAT_1:7

for C being FormalContext

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

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

proof end;

theorem Th8: :: CONLAT_1:8

for C being FormalContext

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

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

proof end;

theorem Th9: :: CONLAT_1:9

for C being FormalContext

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )

proof end;

theorem Th10: :: CONLAT_1:10

for C being FormalContext

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )

proof end;

theorem :: CONLAT_1:11

for C being FormalContext

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )

for O being Subset of the carrier of C

for A being Subset of the carrier' of C holds

( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )

proof end;

definition

let C be FormalContext;

ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C)

end;
func phi C -> Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) equals :: CONLAT_1:def 5

ObjectDerivation C;

coherence ObjectDerivation C;

ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C)

proof end;

:: deftheorem defines phi CONLAT_1:def 5 :

for C being FormalContext holds phi C = ObjectDerivation C;

for C being FormalContext holds phi C = ObjectDerivation C;

definition

let C be FormalContext;

AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C)

end;
func psi C -> Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) equals :: CONLAT_1:def 6

AttributeDerivation C;

coherence AttributeDerivation C;

AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C)

proof end;

:: deftheorem defines psi CONLAT_1:def 6 :

for C being FormalContext holds psi C = AttributeDerivation C;

for C being FormalContext holds psi C = AttributeDerivation C;

:: deftheorem defines co-Galois CONLAT_1:def 7 :

for P, R being non empty RelStr

for Con being Connection of P,R holds

( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st

( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P

for r1, r2 being Element of R holds

( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) );

for P, R being non empty RelStr

for Con being Connection of P,R holds

( Con is co-Galois iff ex f being Function of P,R ex g being Function of R,P st

( Con = [f,g] & f is antitone & g is antitone & ( for p1, p2 being Element of P

for r1, r2 being Element of R holds

( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) ) ) );

theorem Th12: :: CONLAT_1:12

for P, R being non empty Poset

for Con being Connection of P,R

for f being Function of P,R

for g being Function of R,P st Con = [f,g] holds

( Con is co-Galois iff for p being Element of P

for r being Element of R holds

( p <= g . r iff r <= f . p ) )

for Con being Connection of P,R

for f being Function of P,R

for g being Function of R,P st Con = [f,g] holds

( Con is co-Galois iff for p being Element of P

for r being Element of R holds

( p <= g . r iff r <= f . p ) )

proof end;

theorem :: CONLAT_1:13

for P, R being non empty Poset

for Con being Connection of P,R st Con is co-Galois holds

for f being Function of P,R

for g being Function of R,P st Con = [f,g] holds

( f = f * (g * f) & g = g * (f * g) )

for Con being Connection of P,R st Con is co-Galois holds

for f being Function of P,R

for g being Function of R,P st Con = [f,g] holds

( f = f * (g * f) & g = g * (f * g) )

proof end;

theorem Th15: :: CONLAT_1:15

for C being FormalContext

for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)

for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)

proof end;

theorem Th16: :: CONLAT_1:16

for C being FormalContext

for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)

for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)

proof end;

definition

let C be 2-sorted ;

attr c_{2} is strict ;

struct ConceptStr over C -> ;

aggr ConceptStr(# Extent, Intent #) -> ConceptStr over C;

sel Extent c_{2} -> Subset of the carrier of C;

sel Intent c_{2} -> Subset of the carrier' of C;

end;
attr c

struct ConceptStr over C -> ;

aggr ConceptStr(# Extent, Intent #) -> ConceptStr over C;

sel Extent c

sel Intent c

definition

let C be 2-sorted ;

let CP be ConceptStr over C;

end;
let CP be ConceptStr over C;

attr CP is empty means :Def7: :: CONLAT_1:def 8

( the Extent of CP is empty & the Intent of CP is empty );

( the Extent of CP is empty & the Intent of CP is empty );

attr CP is quasi-empty means :Def8: :: CONLAT_1:def 9

( the Extent of CP is empty or the Intent of CP is empty );

( the Extent of CP is empty or the Intent of CP is empty );

:: deftheorem Def7 defines empty CONLAT_1:def 8 :

for C being 2-sorted

for CP being ConceptStr over C holds

( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) );

for C being 2-sorted

for CP being ConceptStr over C holds

( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) );

:: deftheorem Def8 defines quasi-empty CONLAT_1:def 9 :

for C being 2-sorted

for CP being ConceptStr over C holds

( CP is quasi-empty iff ( the Extent of CP is empty or the Intent of CP is empty ) );

for C being 2-sorted

for CP being ConceptStr over C holds

( CP is quasi-empty iff ( the Extent of CP is empty or the Intent of CP is empty ) );

registration

let C be non empty non void 2-sorted ;

existence

ex b_{1} being ConceptStr over C st

( b_{1} is strict & not b_{1} is empty )

ex b_{1} being ConceptStr over C st

( b_{1} is strict & b_{1} is quasi-empty )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

registration
end;

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

definition

let C be FormalContext;

let CP be ConceptStr over C;

end;
let CP be ConceptStr over C;

attr CP is concept-like means :Def9: :: CONLAT_1:def 10

( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP );

( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP );

:: deftheorem Def9 defines concept-like CONLAT_1:def 10 :

for C being FormalContext

for CP being ConceptStr over C holds

( CP is concept-like iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) );

for C being FormalContext

for CP being ConceptStr over C holds

( CP is concept-like iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) );

registration

let C be FormalContext;

existence

ex b_{1} being ConceptStr over C st

( b_{1} is concept-like & not b_{1} is empty )

end;
existence

ex b

( b

proof end;

definition
end;

registration
end;

theorem Th19: :: CONLAT_1:19

for C being FormalContext

for O being Subset of the carrier of C holds

( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C

for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 holds

(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 ) )

for O being Subset of the carrier of C holds

( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C

for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 holds

(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 ) )

proof end;

theorem :: CONLAT_1:20

for C being FormalContext

for O being Subset of the carrier of C holds

( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )

for O being Subset of the carrier of C holds

( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )

proof end;

theorem Th21: :: CONLAT_1:21

for C being FormalContext

for A being Subset of the carrier' of C holds

( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C

for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 holds

(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) )

for A being Subset of the carrier' of C holds

( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O9 being Subset of the carrier of C

for A9 being Subset of the carrier' of C st ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 holds

(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 ) )

proof end;

theorem :: CONLAT_1:22

for C being FormalContext

for A being Subset of the carrier' of C holds

( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )

for A being Subset of the carrier' of C holds

( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )

proof end;

:: deftheorem defines universal CONLAT_1:def 11 :

for C being FormalContext

for CP being ConceptStr over C holds

( CP is universal iff the Extent of CP = the carrier of C );

for C being FormalContext

for CP being ConceptStr over C holds

( CP is universal iff the Extent of CP = the carrier of C );

:: deftheorem defines co-universal CONLAT_1:def 12 :

for C being FormalContext

for CP being ConceptStr over C holds

( CP is co-universal iff the Intent of CP = the carrier' of C );

for C being FormalContext

for CP being ConceptStr over C holds

( CP is co-universal iff the Intent of CP = the carrier' of C );

registration

let C be FormalContext;

existence

ex b_{1} being FormalConcept of C st

( b_{1} is strict & b_{1} is universal )

ex b_{1} being FormalConcept of C st

( b_{1} is strict & b_{1} is co-universal )

end;
existence

ex b

( b

proof end;

existence ex b

( b

proof end;

definition

let C be FormalContext;

ex b_{1} being strict universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

for b_{1}, b_{2} being strict universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

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

b_{1} = b_{2}
;

end;
func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def12: :: CONLAT_1:def 13

ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

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

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

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def12 defines Concept-with-all-Objects CONLAT_1:def 13 :

for C being FormalContext

for b_{2} being strict universal FormalConcept of C holds

( b_{2} = Concept-with-all-Objects C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

for C being FormalContext

for b

( b

( b

definition

let C be FormalContext;

ex b_{1} being strict co-universal FormalConcept of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

for b_{1}, b_{2} being strict co-universal FormalConcept of C st ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

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

b_{1} = b_{2}
;

end;
func Concept-with-all-Attributes C -> strict co-universal FormalConcept of C means :Def13: :: CONLAT_1:def 14

ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

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

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

ex b

( b

proof end;

uniqueness for b

( b

( b

b

:: deftheorem Def13 defines Concept-with-all-Attributes CONLAT_1:def 14 :

for C being FormalContext

for b_{2} being strict co-universal FormalConcept of C holds

( b_{2} = Concept-with-all-Attributes C iff ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st

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

for C being FormalContext

for b

( b

( b

theorem Th23: :: CONLAT_1:23

for C being FormalContext holds

( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )

( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )

proof end;

theorem :: CONLAT_1:24

for C being FormalContext

for CP being FormalConcept of C holds

( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )

for CP being FormalConcept of C holds

( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )

proof end;

theorem Th25: :: CONLAT_1:25

for C being FormalContext

for CP being strict FormalConcept of C holds

( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )

for CP being strict FormalConcept of C holds

( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )

proof end;

theorem :: CONLAT_1:26

for C being FormalContext

for CP being quasi-empty ConceptStr over C holds

( not CP is FormalConcept of C or CP is universal or CP is co-universal )

for CP being quasi-empty ConceptStr over C holds

( not CP is FormalConcept of C or CP is universal or CP is co-universal )

proof end;

theorem :: CONLAT_1:27

for C being FormalContext

for CP being quasi-empty ConceptStr over C holds

( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )

for CP being quasi-empty ConceptStr over C holds

( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )

proof end;

definition

let C be FormalContext;

ex b_{1} being non empty set st

for X being set st X in b_{1} holds

X is FormalConcept of C

end;
mode Set-of-FormalConcepts of C -> non empty set means :Def14: :: CONLAT_1:def 15

for X being set st X in it holds

X is FormalConcept of C;

existence for X being set st X in it holds

X is FormalConcept of C;

ex b

for X being set st X in b

X is FormalConcept of C

proof end;

:: deftheorem Def14 defines Set-of-FormalConcepts CONLAT_1:def 15 :

for C being FormalContext

for b_{2} being non empty set holds

( b_{2} is Set-of-FormalConcepts of C iff for X being set st X in b_{2} holds

X is FormalConcept of C );

for C being FormalContext

for b

( b

X is FormalConcept of C );

definition

let C be FormalContext;

let FCS be Set-of-FormalConcepts of C;

:: original: Element

redefine mode Element of FCS -> FormalConcept of C;

coherence

for b_{1} being Element of FCS holds b_{1} is FormalConcept of C
by Def14;

end;
let FCS be Set-of-FormalConcepts of C;

:: original: Element

redefine mode Element of FCS -> FormalConcept of C;

coherence

for b

:: deftheorem defines is-SubConcept-of CONLAT_1:def 16 :

for C being FormalContext

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 );

for C being FormalContext

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SubConcept-of CP2 iff the Extent of CP1 c= the Extent of CP2 );

notation

let C be FormalContext;

let CP1, CP2 be FormalConcept of C;

synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2;

end;
let CP1, CP2 be FormalConcept of C;

synonym CP2 is-SuperConcept-of CP1 for CP1 is-SubConcept-of CP2;

theorem Th28: :: CONLAT_1:28

for C being FormalContext

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )

proof end;

theorem :: CONLAT_1:29

for C being FormalContext

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SuperConcept-of CP2 iff the Intent of CP1 c= the Intent of CP2 ) by Th28;

for CP1, CP2 being FormalConcept of C holds

( CP1 is-SuperConcept-of CP2 iff the Intent of CP1 c= the Intent of CP2 ) by Th28;

theorem :: CONLAT_1:30

for C being FormalContext

for CP being FormalConcept of C holds

( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )

for CP being FormalConcept of C holds

( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )

proof end;

definition

let C be FormalContext;

{ ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set

end;
func B-carrier C -> non empty set equals :: CONLAT_1:def 17

{ ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;

coherence { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;

{ ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set

proof end;

:: deftheorem defines B-carrier CONLAT_1:def 17 :

for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;

for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the carrier of C, I is Subset of the carrier' of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } ;

definition

let C be FormalContext;

:: original: B-carrier

redefine func B-carrier C -> Set-of-FormalConcepts of C;

coherence

B-carrier C is Set-of-FormalConcepts of C

end;
:: original: B-carrier

redefine func B-carrier C -> Set-of-FormalConcepts of C;

coherence

B-carrier C is Set-of-FormalConcepts of C

proof end;

registration
end;

theorem Th31: :: CONLAT_1:31

for C being FormalContext

for CP being object holds

( CP in B-carrier C iff CP is strict FormalConcept of C )

for CP being object holds

( CP in B-carrier C iff CP is strict FormalConcept of C )

proof end;

definition

let C be FormalContext;

ex b_{1} 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

( b_{1} . (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 b_{1}, b_{2} 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

( b_{1} . (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

( b_{2} . (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

b_{1} = b_{2}

end;
func B-meet C -> BinOp of (B-carrier C) means :Def17: :: CONLAT_1:def 18

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 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)) );

ex b

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

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def17 defines B-meet CONLAT_1:def 18 :

for C being FormalContext

for b_{2} being BinOp of (B-carrier C) holds

( b_{2} = B-meet C iff 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

( b_{2} . (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 C being FormalContext

for b

( b

( b

definition

let C be FormalContext;

ex b_{1} 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

( b_{1} . (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 b_{1}, b_{2} 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

( b_{1} . (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

( b_{2} . (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

b_{1} = b_{2}

end;
func B-join C -> BinOp of (B-carrier C) means :Def18: :: CONLAT_1:def 19

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 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 );

ex b

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

( b

proof end;

uniqueness for b

( b

( b

b

proof end;

:: deftheorem Def18 defines B-join CONLAT_1:def 19 :

for C being FormalContext

for b_{2} being BinOp of (B-carrier C) holds

( b_{2} = B-join C iff 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

( b_{2} . (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 C being FormalContext

for b

( b

( b

Lm2: for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) in rng (B-meet C)

proof end;

Lm3: for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)

proof end;

theorem Th32: :: CONLAT_1:32

for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)

for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)

proof end;

theorem Th33: :: CONLAT_1:33

for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)

for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)

proof end;

theorem Th34: :: CONLAT_1:34

for C being FormalContext

for CP1, CP2, CP3 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)

for CP1, CP2, CP3 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)

proof end;

theorem Th35: :: CONLAT_1:35

for C being FormalContext

for CP1, CP2, CP3 being strict FormalConcept of C holds (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)

for CP1, CP2, CP3 being strict FormalConcept of C holds (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)

proof end;

theorem Th36: :: CONLAT_1:36

for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2

for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2

proof end;

theorem Th37: :: CONLAT_1:37

for C being FormalContext

for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1

for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1

proof end;

theorem :: CONLAT_1:38

for C being FormalContext

for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP

for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP

proof end;

theorem Th39: :: CONLAT_1:39

for C being FormalContext

for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C

for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C

proof end;

theorem :: CONLAT_1:40

for C being FormalContext

for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP

for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP

proof end;

theorem :: CONLAT_1:41

for C being FormalContext

for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C

for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C

proof end;

definition

let C be FormalContext;

LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr ;

end;
func ConceptLattice C -> non empty strict LattStr equals :: CONLAT_1:def 20

LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

coherence LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr ;

:: deftheorem defines ConceptLattice CONLAT_1:def 20 :

for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

registration

let C be FormalContext;

coherence

( ConceptLattice C is strict & not ConceptLattice C is empty & ConceptLattice C is Lattice-like ) by Th42;

end;
coherence

( ConceptLattice C is strict & not ConceptLattice C is empty & ConceptLattice C is Lattice-like ) by Th42;

definition

let C be FormalContext;

let S be non empty Subset of (ConceptLattice C);

:: original: Element

redefine mode Element of S -> FormalConcept of C;

coherence

for b_{1} being Element of S holds b_{1} is FormalConcept of C

end;
let S be non empty Subset of (ConceptLattice C);

:: original: Element

redefine mode Element of S -> FormalConcept of C;

coherence

for b

proof end;

definition

let C be FormalContext;

let CP be Element of (ConceptLattice C);

coherence

CP is strict FormalConcept of C by Th31;

end;
let CP be Element of (ConceptLattice C);

coherence

CP is strict FormalConcept of C by Th31;

:: deftheorem defines @ CONLAT_1:def 21 :

for C being FormalContext

for CP being Element of (ConceptLattice C) holds CP @ = CP;

for C being FormalContext

for CP being Element of (ConceptLattice C) holds CP @ = CP;

theorem Th43: :: CONLAT_1:43

for C being FormalContext

for CP1, CP2 being Element of (ConceptLattice C) holds

( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )

for CP1, CP2 being Element of (ConceptLattice C) holds

( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )

proof end;