:: CONLAT_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
attr c1 is strict;
struct 2-sorted -> ;
aggr 2-sorted(# Objects, Attributes #) -> 2-sorted ;
sel Objects c1 -> set ;
sel Attributes c1 -> set ;
end;

definition
let C be 2-sorted ;
attr C is empty means :Def1: :: CONLAT_1:def 1
( the Objects of C is empty & the Attributes of C is empty );
attr C is quasi-empty means :Def2: :: CONLAT_1:def 2
( the Objects of C is empty or the Attributes of C is empty );
end;

:: deftheorem Def1 defines empty CONLAT_1:def 1 :
for C being 2-sorted holds
( C is empty iff ( the Objects of C is empty & the Attributes of C is empty ) );

:: deftheorem Def2 defines quasi-empty CONLAT_1:def 2 :
for C being 2-sorted holds
( C is quasi-empty iff ( the Objects of C is empty or the Attributes of C is empty ) );

registration
cluster strict non empty 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is empty )
proof end;
cluster strict non quasi-empty 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty )
proof end;
end;

registration
cluster strict empty quasi-empty 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is quasi-empty )
proof end;
end;

definition
attr c1 is strict;
struct ContextStr -> 2-sorted ;
aggr ContextStr(# Objects, Attributes, Information #) -> ContextStr ;
sel Information c1 -> Relation of the Objects of c1,the Attributes of c1;
end;

registration
cluster non empty strict ContextStr ;
existence
ex b1 being ContextStr st
( b1 is strict & not b1 is empty )
proof end;
cluster non quasi-empty strict ContextStr ;
existence
ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty )
proof end;
end;

definition
mode FormalContext is non quasi-empty ContextStr ;
end;

definition
let C be 2-sorted ;
mode Object of C is Element of the Objects of C;
mode Attribute of C is Element of the Attributes of C;
end;

registration
let C be non quasi-empty 2-sorted ;
cluster the Attributes of C -> non empty ;
coherence
not the Attributes of C is empty
by Def2;
cluster the Objects of C -> non empty ;
coherence
not the Objects of C is empty
by Def2;
end;

registration
let C be non quasi-empty 2-sorted ;
cluster non empty Element of bool the Objects of C;
existence
not for b1 being Subset of the Objects of C holds b1 is empty
proof end;
cluster non empty Element of bool the Attributes of C;
existence
not for b1 being Subset of the Attributes of C holds b1 is empty
proof end;
end;

definition
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
canceled;
canceled;
pred o is-connected-with a means :Def5: :: CONLAT_1:def 5
[o,a] in the Information of C;
end;

:: deftheorem CONLAT_1:def 3 :
canceled;

:: deftheorem CONLAT_1:def 4 :
canceled;

:: deftheorem Def5 defines is-connected-with CONLAT_1:def 5 :
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;

definition
let C be FormalContext;
func ObjectDerivation C -> Function of bool the Objects of C, bool the Attributes of C means :Def6: :: CONLAT_1:def 6
for O being Subset of the Objects 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
ex b1 being Function of bool the Objects of C, bool the Attributes of C st
for O being Subset of the Objects of C holds b1 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a
}
proof end;
uniqueness
for b1, b2 being Function of bool the Objects of C, bool the Attributes of C st ( for O being Subset of the Objects of C holds b1 . 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 Objects of C holds b2 . 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
b1 = b2
proof end;
end;

:: deftheorem Def6 defines ObjectDerivation CONLAT_1:def 6 :
for C being FormalContext
for b2 being Function of bool the Objects of C, bool the Attributes of C holds
( b2 = ObjectDerivation C iff for O being Subset of the Objects of C holds b2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a
}
);

definition
let C be FormalContext;
func AttributeDerivation C -> Function of bool the Attributes of C, bool the Objects of C means :Def7: :: CONLAT_1:def 7
for A being Subset of the Attributes 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
ex b1 being Function of bool the Attributes of C, bool the Objects of C st
for A being Subset of the Attributes of C holds b1 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a
}
proof end;
uniqueness
for b1, b2 being Function of bool the Attributes of C, bool the Objects of C st ( for A being Subset of the Attributes of C holds b1 . 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 Attributes of C holds b2 . 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
b1 = b2
proof end;
end;

:: deftheorem Def7 defines AttributeDerivation CONLAT_1:def 7 :
for C being FormalContext
for b2 being Function of bool the Attributes of C, bool the Objects of C holds
( b2 = AttributeDerivation C iff for A being Subset of the Attributes of C holds b2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a
}
);

theorem :: CONLAT_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 }
proof end;

theorem :: CONLAT_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 }
proof end;

theorem Th3: :: CONLAT_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O1, O2 being Subset of the Objects of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
proof end;

theorem Th4: :: CONLAT_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A1, A2 being Subset of the Attributes of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
proof end;

theorem Th5: :: CONLAT_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
proof end;

theorem Th6: :: CONLAT_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A being Subset of the Attributes of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
proof end;

theorem Th7: :: CONLAT_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
proof end;

theorem Th8: :: CONLAT_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A being Subset of the Attributes of C holds (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
proof end;

theorem Th9: :: CONLAT_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C
for A being Subset of the Attributes of C holds
( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )
proof end;

theorem Th10: :: CONLAT_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C
for A being Subset of the Attributes of C holds
( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )
proof end;

theorem :: CONLAT_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C
for A being Subset of the Attributes of C holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
proof end;

definition
let C be FormalContext;
func phi C -> Function of (BoolePoset the Objects of C),(BoolePoset the Attributes of C) equals :: CONLAT_1:def 8
ObjectDerivation C;
coherence
ObjectDerivation C is Function of (BoolePoset the Objects of C),(BoolePoset the Attributes of C)
proof end;
end;

:: deftheorem defines phi CONLAT_1:def 8 :
for C being FormalContext holds phi C = ObjectDerivation C;

definition
let C be FormalContext;
func psi C -> Function of (BoolePoset the Attributes of C),(BoolePoset the Objects of C) equals :: CONLAT_1:def 9
AttributeDerivation C;
coherence
AttributeDerivation C is Function of (BoolePoset the Attributes of C),(BoolePoset the Objects of C)
proof end;
end;

:: deftheorem defines psi CONLAT_1:def 9 :
for C being FormalContext holds psi C = AttributeDerivation C;

definition
let P, R be non empty RelStr ;
let Con be Connection of P,R;
attr Con is co-Galois means :Def10: :: CONLAT_1:def 10
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) ) ) );
end;

:: deftheorem Def10 defines co-Galois CONLAT_1:def 10 :
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 :: CONLAT_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th13: :: CONLAT_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: CONLAT_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem :: CONLAT_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds [(phi C),(psi C)] is co-Galois
proof end;

theorem Th16: :: CONLAT_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O1, O2 being Subset of the Objects of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
proof end;

theorem Th17: :: CONLAT_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A1, A2 being Subset of the Attributes of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
proof end;

theorem Th18: :: CONLAT_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds (ObjectDerivation C) . {} = the Attributes of C
proof end;

theorem Th19: :: CONLAT_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds (AttributeDerivation C) . {} = the Objects of C
proof end;

definition
let C be 2-sorted ;
attr c2 is strict;
struct ConceptStr of C -> ;
aggr ConceptStr(# Extent, Intent #) -> ConceptStr of C;
sel Extent c2 -> Subset of the Objects of C;
sel Intent c2 -> Subset of the Attributes of C;
end;

definition
let C be 2-sorted ;
let CP be ConceptStr of C;
attr CP is empty means :Def11: :: CONLAT_1:def 11
( the Extent of CP is empty & the Intent of CP is empty );
attr CP is quasi-empty means :Def12: :: CONLAT_1:def 12
( the Extent of CP is empty or the Intent of CP is empty );
end;

:: deftheorem Def11 defines empty CONLAT_1:def 11 :
for C being 2-sorted
for CP being ConceptStr of C holds
( CP is empty iff ( the Extent of CP is empty & the Intent of CP is empty ) );

:: deftheorem Def12 defines quasi-empty CONLAT_1:def 12 :
for C being 2-sorted
for CP being ConceptStr of 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 quasi-empty 2-sorted ;
cluster strict non empty ConceptStr of C;
existence
ex b1 being ConceptStr of C st
( b1 is strict & not b1 is empty )
proof end;
cluster strict quasi-empty ConceptStr of C;
existence
ex b1 being ConceptStr of C st
( b1 is strict & b1 is quasi-empty )
proof end;
end;

registration
let C be empty 2-sorted ;
cluster -> empty ConceptStr of C;
coherence
for b1 being ConceptStr of C holds b1 is empty
proof end;
end;

registration
let C be quasi-empty 2-sorted ;
cluster -> quasi-empty ConceptStr of C;
coherence
for b1 being ConceptStr of C holds b1 is quasi-empty
proof end;
end;

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

definition
let C be FormalContext;
let CP be ConceptStr of C;
attr CP is concept-like means :Def13: :: CONLAT_1:def 13
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP );
end;

:: deftheorem Def13 defines concept-like CONLAT_1:def 13 :
for C being FormalContext
for CP being ConceptStr of 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;
cluster non empty concept-like ConceptStr of C;
existence
ex b1 being ConceptStr of C st
( b1 is concept-like & not b1 is empty )
proof end;
end;

definition
let C be FormalContext;
mode FormalConcept of C is non empty concept-like ConceptStr of C;
end;

registration
let C be FormalContext;
cluster strict ConceptStr of C;
existence
ex b1 being FormalConcept of C st b1 is strict
proof end;
end;

theorem Th20: :: CONLAT_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C holds
( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C & ( for O' being Subset of the Objects of C
for A' being Subset of the Attributes of C st ConceptStr(# O',A' #) is FormalConcept of C & O c= O' holds
(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O' ) )
proof end;

theorem :: CONLAT_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for O being Subset of the Objects of C holds
( ex A being Subset of the Attributes of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )
proof end;

theorem Th22: :: CONLAT_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A being Subset of the Attributes of C holds
( ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C & ( for O' being Subset of the Objects of C
for A' being Subset of the Attributes of C st ConceptStr(# O',A' #) is FormalConcept of C & A c= A' holds
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A' ) )
proof end;

theorem :: CONLAT_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for A being Subset of the Attributes of C holds
( ex O being Subset of the Objects of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )
proof end;

definition
let C be FormalContext;
let CP be ConceptStr of C;
attr CP is universal means :Def14: :: CONLAT_1:def 14
the Extent of CP = the Objects of C;
end;

:: deftheorem Def14 defines universal CONLAT_1:def 14 :
for C being FormalContext
for CP being ConceptStr of C holds
( CP is universal iff the Extent of CP = the Objects of C );

definition
let C be FormalContext;
let CP be ConceptStr of C;
attr CP is co-universal means :Def15: :: CONLAT_1:def 15
the Intent of CP = the Attributes of C;
end;

:: deftheorem Def15 defines co-universal CONLAT_1:def 15 :
for C being FormalContext
for CP being ConceptStr of C holds
( CP is co-universal iff the Intent of CP = the Attributes of C );

registration
let C be FormalContext;
cluster strict universal ConceptStr of C;
existence
ex b1 being FormalConcept of C st
( b1 is strict & b1 is universal )
proof end;
cluster strict co-universal ConceptStr of C;
existence
ex b1 being FormalConcept of C st
( b1 is strict & b1 is co-universal )
proof end;
end;

definition
let C be FormalContext;
func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def16: :: CONLAT_1:def 16
ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) );
existence
ex b1 being strict universal FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) )
proof end;
uniqueness
for b1, b2 being strict universal FormalConcept of C st ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) ) & ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) ) holds
b1 = b2
;
end;

:: deftheorem Def16 defines Concept-with-all-Objects CONLAT_1:def 16 :
for C being FormalContext
for b2 being strict universal FormalConcept of C holds
( b2 = Concept-with-all-Objects C iff ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {} ) ) );

definition
let C be FormalContext;
func Concept-with-all-Attributes C -> strict co-universal FormalConcept of C means :Def17: :: CONLAT_1:def 17
ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( it = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} );
existence
ex b1 being strict co-universal FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} )
proof end;
uniqueness
for b1, b2 being strict co-universal FormalConcept of C st ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} ) & ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} ) holds
b1 = b2
;
end;

:: deftheorem Def17 defines Concept-with-all-Attributes CONLAT_1:def 17 :
for C being FormalContext
for b2 being strict co-universal FormalConcept of C holds
( b2 = Concept-with-all-Attributes C iff ex O being Subset of the Objects of C ex A being Subset of the Attributes of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {} ) & A = (ObjectDerivation C) . {} ) );

theorem Th24: :: CONLAT_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds
( the Extent of (Concept-with-all-Objects C) = the Objects of C & the Intent of (Concept-with-all-Attributes C) = the Attributes of C )
proof end;

theorem :: CONLAT_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th26: :: CONLAT_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem :: CONLAT_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP being quasi-empty ConceptStr of C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
proof end;

theorem :: CONLAT_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP being quasi-empty ConceptStr of 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;
mode Set-of-FormalConcepts of C -> non empty set means :Def18: :: CONLAT_1:def 18
for X being set st X in it holds
X is FormalConcept of C;
existence
ex b1 being non empty set st
for X being set st X in b1 holds
X is FormalConcept of C
proof end;
end;

:: deftheorem Def18 defines Set-of-FormalConcepts CONLAT_1:def 18 :
for C being FormalContext
for b2 being non empty set holds
( b2 is Set-of-FormalConcepts of C iff for X being set st X in b2 holds
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 b1 being Element of FCS holds b1 is FormalConcept of C
by Def18;
end;

definition
let C be FormalContext;
let CP1, CP2 be FormalConcept of C;
pred CP1 is-SubConcept-of CP2 means :Def19: :: CONLAT_1:def 19
the Extent of CP1 c= the Extent of CP2;
end;

:: deftheorem Def19 defines is-SubConcept-of CONLAT_1:def 19 :
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;

theorem :: CONLAT_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CONLAT_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th31: :: CONLAT_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: CONLAT_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: CONLAT_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 Th31;

theorem :: CONLAT_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let C be FormalContext;
func B-carrier C -> non empty set equals :: CONLAT_1:def 20
{ ConceptStr(# E,I #) where E is Subset of the Objects of C, I is Subset of the Attributes 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 Objects of C, I is Subset of the Attributes of C : ( not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) } is non empty set
proof end;
end;

:: deftheorem defines B-carrier CONLAT_1:def 20 :
for C being FormalContext holds B-carrier C = { ConceptStr(# E,I #) where E is Subset of the Objects of C, I is Subset of the Attributes 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
proof end;
end;

registration
let C be FormalContext;
cluster B-carrier C -> non empty ;
coherence
not B-carrier C is empty
;
end;

theorem Th35: :: CONLAT_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP being set holds
( CP in B-carrier C iff CP is strict FormalConcept of C )
proof end;

definition
let C be FormalContext;
func B-meet C -> BinOp of B-carrier C means :Def21: :: CONLAT_1:def 21
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes 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 Objects of C ex A being Subset of the Attributes 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)) )
proof end;
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 Objects of C ex A being Subset of the Attributes 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 Objects of C ex A being Subset of the Attributes 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
proof end;
end;

:: deftheorem Def21 defines B-meet CONLAT_1:def 21 :
for C being FormalContext
for b2 being BinOp of B-carrier C holds
( b2 = B-meet C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes 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)) ) );

definition
let C be FormalContext;
func B-join C -> BinOp of B-carrier C means :Def22: :: CONLAT_1:def 22
for CP1, CP2 being strict FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes 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 Objects of C ex A being Subset of the Attributes 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 )
proof end;
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 Objects of C ex A being Subset of the Attributes 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 Objects of C ex A being Subset of the Attributes 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
proof end;
end;

:: deftheorem Def22 defines B-join CONLAT_1:def 22 :
for C being FormalContext
for b2 being BinOp of B-carrier C holds
( b2 = B-join C iff for CP1, CP2 being strict FormalConcept of C ex O being Subset of the Objects of C ex A being Subset of the Attributes 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 ) );

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;

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

theorem Th36: :: CONLAT_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . CP1,CP2 = (B-meet C) . CP2,CP1
proof end;

theorem Th37: :: CONLAT_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-join C) . CP1,CP2 = (B-join C) . CP2,CP1
proof end;

theorem Th38: :: CONLAT_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th39: :: CONLAT_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th40: :: CONLAT_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-join C) . ((B-meet C) . CP1,CP2),CP2 = CP2
proof end;

theorem Th41: :: CONLAT_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . CP1,((B-join C) . CP1,CP2) = CP1
proof end;

theorem :: CONLAT_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP being strict FormalConcept of C holds (B-meet C) . CP,(Concept-with-all-Objects C) = CP
proof end;

theorem Th43: :: CONLAT_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: CONLAT_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP being strict FormalConcept of C holds (B-join C) . CP,(Concept-with-all-Attributes C) = CP
proof end;

theorem :: CONLAT_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let C be FormalContext;
func ConceptLattice C -> non empty strict LattStr equals :: CONLAT_1:def 23
LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
coherence
LattStr(# (B-carrier C),(B-join C),(B-meet C) #) is non empty strict LattStr
;
end;

:: deftheorem defines ConceptLattice CONLAT_1:def 23 :
for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);

theorem Th46: :: CONLAT_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds ConceptLattice C is Lattice
proof end;

registration
let C be FormalContext;
cluster ConceptLattice C -> non empty strict Lattice-like ;
coherence
( ConceptLattice C is strict & not ConceptLattice C is empty & ConceptLattice C is Lattice-like )
by Th46;
end;

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 b1 being Element of S holds b1 is FormalConcept of C
proof end;
end;

definition
let C be FormalContext;
let CP be Element of (ConceptLattice C);
func CP @ -> strict FormalConcept of C equals :: CONLAT_1:def 24
CP;
coherence
CP is strict FormalConcept of C
by Th35;
end;

:: deftheorem defines @ CONLAT_1:def 24 :
for C being FormalContext
for CP being Element of (ConceptLattice C) holds CP @ = CP;

theorem Th47: :: CONLAT_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext
for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
proof end;

theorem Th48: :: CONLAT_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being FormalContext holds ConceptLattice C is complete Lattice
proof end;

registration
let C be FormalContext;
cluster ConceptLattice C -> non empty strict Lattice-like complete ;
coherence
ConceptLattice C is complete
by Th48;
end;