:: CONLAT_1 semantic presentation
begin
definition
let C be 2-sorted ;
attrC is quasi-empty means :Def1: :: CONLAT_1:def 1
( the carrier of C is empty or the carrier' of C is empty );
end;
:: deftheorem Def1 defines quasi-empty CONLAT_1:def_1_:_
for C being 2-sorted holds
( C is quasi-empty iff ( the carrier of C is empty or the carrier' of C is empty ) );
registration
cluster non empty strict non void for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void )
proof
( not 2-sorted(# {{}},{{}} #) is empty & not 2-sorted(# {{}},{{}} #) is void ) ;
hence ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void ) ; ::_thesis: verum
end;
cluster strict non quasi-empty for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty )
proof
not 2-sorted(# {{}},{{}} #) is quasi-empty by Def1;
hence ex b1 being 2-sorted st
( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum
end;
end;
registration
cluster empty strict void quasi-empty for 2-sorted ;
existence
ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty )
proof
( 2-sorted(# {},{} #) is empty & 2-sorted(# {},{} #) is void & 2-sorted(# {},{} #) is quasi-empty ) by Def1;
hence ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void & b1 is quasi-empty ) ; ::_thesis: verum
end;
end;
definition
attrc1 is strict ;
struct ContextStr -> 2-sorted ;
aggrContextStr(# carrier, carrier', Information #) -> ContextStr ;
sel Information c1 -> Relation of the carrier of c1, the carrier' of c1;
end;
registration
cluster non empty strict for ContextStr ;
existence
ex b1 being ContextStr st
( b1 is strict & not b1 is empty )
proof
set I = the Relation of {{}},{{}};
not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is empty ;
hence ex b1 being ContextStr st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
cluster non quasi-empty strict for ContextStr ;
existence
ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty )
proof
set I = the Relation of {{}},{{}};
not ContextStr(# {{}},{{}}, the Relation of {{}},{{}} #) is quasi-empty by Def1;
hence ex b1 being ContextStr st
( b1 is strict & not b1 is quasi-empty ) ; ::_thesis: verum
end;
end;
definition
mode FormalContext is non quasi-empty ContextStr ;
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;
registration
let C be non quasi-empty 2-sorted ;
cluster the carrier' of C -> non empty ;
coherence
not the carrier' of C is empty by Def1;
cluster the carrier of C -> non empty ;
coherence
not the carrier of C is empty by Def1;
end;
registration
let C be non quasi-empty 2-sorted ;
cluster non empty for Element of bool the carrier of C;
existence
not for b1 being Subset of the carrier of C holds b1 is empty
proof
take the carrier of C ; ::_thesis: ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty )
the carrier of C c= the carrier of C ;
hence ( the carrier of C is Subset of the carrier of C & not the carrier of C is empty ) ; ::_thesis: verum
end;
cluster non empty for Element of bool the carrier' of C;
existence
not for b1 being Subset of the carrier' of C holds b1 is empty
proof
take the carrier' of C ; ::_thesis: ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty )
the carrier' of C c= the carrier' of C ;
hence ( the carrier' of C is Subset of the carrier' of C & not the carrier' of C is empty ) ; ::_thesis: verum
end;
end;
definition
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
predo is-connected-with a means :Def2: :: CONLAT_1:def 2
[o,a] in the Information of C;
end;
:: deftheorem Def2 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 );
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;
begin
definition
let C be FormalContext;
func ObjectDerivation C -> Function of (bool the carrier of C),(bool the carrier' of C) means :Def3: :: 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
ex b1 being Function of (bool the carrier of C),(bool the carrier' of C) st
for O being Subset of the carrier 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
set f = { [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } ;
for u being set st u in { [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } holds
ex v, w being set st u = [v,w]
proof
let u be set ; ::_thesis: ( u in { [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } implies ex v, w being set st u = [v,w] )
assume u in { [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } ; ::_thesis: ex v, w being set st u = [v,w]
then ex O being Subset of the carrier of C st u = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] ;
hence ex v, w being set st u = [v,w] ; ::_thesis: verum
end;
then reconsider f = { [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] where O is Subset of the carrier of C : verum } as Relation by RELAT_1:def_1;
for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that
A1: [u,v1] in f and
A2: [u,v2] in f ; ::_thesis: v1 = v2
consider O being Subset of the carrier of C such that
A3: [u,v1] = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] by A1;
A4: v1 = [u,v1] `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 } ] `2 by A3
.= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
consider O9 being Subset of the carrier of C such that
A5: [u,v2] = [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] by A2;
A6: v2 = [u,v2] `2
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `2 by A5
.= { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
O = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] `1
.= [u,v1] `1 by A3
.= u
.= [u,v2] `1
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `1 by A5
.= O9 ;
hence v1 = v2 by A4, A6; ::_thesis: verum
end;
then reconsider f = f as Function by FUNCT_1:def_1;
A7: for x being set st x in dom f holds
x in bool the carrier of C
proof
let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier of C )
assume x in dom f ; ::_thesis: x in bool the carrier of C
then consider y being set such that
A8: [x,y] in f by XTUPLE_0:def_12;
consider O being Subset of the carrier of C such that
A9: [x,y] = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] by A8;
x = [x,y] `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 } ] `1 by A9
.= O ;
hence x in bool the carrier of C ; ::_thesis: verum
end;
for x being set st x in bool the carrier of C holds
x in dom f
proof
let x be set ; ::_thesis: ( x in bool the carrier of C implies x in dom f )
assume x in bool the carrier of C ; ::_thesis: x in dom f
then reconsider x = x as Subset of the carrier of C ;
[x, { a where a is Attribute of C : for o being Object of C st o in x holds
o is-connected-with a } ] in f ;
hence x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A10: dom f = bool the carrier of C by A7, TARSKI:1;
rng f c= bool the carrier' of C
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier' of C )
assume y in rng f ; ::_thesis: y in bool the carrier' of C
then consider x being set such that
A11: [x,y] in f by XTUPLE_0:def_13;
consider O being Subset of the carrier of C such that
A12: [x,y] = [O, { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ] by A11;
A13: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= the carrier' of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or u in the carrier' of C )
assume u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: u in the carrier' of C
then ex u9 being Attribute of C st
( u9 = u & ( for o being Object of C st o in O holds
o is-connected-with u9 ) ) ;
hence u in the carrier' of C ; ::_thesis: verum
end;
y = [x,y] `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 } ] `2 by A12
.= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
hence y in bool the carrier' of C by A13; ::_thesis: verum
end;
then reconsider f = f as Function of (bool the carrier of C),(bool the carrier' of C) by A10, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for O being Subset of the carrier of C holds f . 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 f . 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
let O be Subset of the carrier of C; ::_thesis: f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
consider y being set such that
A14: [O,y] in f by A10, XTUPLE_0:def_12;
consider O9 being Subset of the carrier of C such that
A15: [O,y] = [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] by A14;
A16: y = [O,y] `2
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `2 by A15
.= { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
O = [O,y] `1
.= [O9, { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ] `1 by A15
.= O9 ;
hence f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum
end;
hence for O being Subset of the carrier of C holds f . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (bool the carrier of C),(bool the carrier' of C) st ( for O being Subset of the carrier 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 carrier 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
let F1, F2 be Function of (bool the carrier of C),(bool the carrier' of C); ::_thesis: ( ( for O being Subset of the carrier of C holds F1 . 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 F2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ) implies F1 = F2 )
assume A17: for O being Subset of the carrier of C holds F1 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: ( ex O being Subset of the carrier of C st not F2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or F1 = F2 )
assume A18: for O being Subset of the carrier of C holds F2 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: F1 = F2
A19: for O being set st O in bool the carrier of C holds
F1 . O = F2 . O
proof
let O be set ; ::_thesis: ( O in bool the carrier of C implies F1 . O = F2 . O )
assume O in bool the carrier of C ; ::_thesis: F1 . O = F2 . O
then reconsider O = O as Subset of the carrier of C ;
F1 . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by A17
.= F2 . O by A18 ;
hence F1 . O = F2 . O ; ::_thesis: verum
end;
( dom F1 = bool the carrier of C & dom F2 = bool the carrier of C ) by FUNCT_2:def_1;
hence F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines ObjectDerivation CONLAT_1:def_3_:_
for C being FormalContext
for b2 being Function of (bool the carrier of C),(bool the carrier' of C) holds
( b2 = ObjectDerivation C iff for O being Subset of the carrier 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 carrier' of C),(bool the carrier of C) means :Def4: :: 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
ex b1 being Function of (bool the carrier' of C),(bool the carrier of C) st
for A being Subset of the carrier' 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
set f = { [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } ;
for u being set st u in { [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } holds
ex v, w being set st u = [v,w]
proof
let u be set ; ::_thesis: ( u in { [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } implies ex v, w being set st u = [v,w] )
assume u in { [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } ; ::_thesis: ex v, w being set st u = [v,w]
then ex A being Subset of the carrier' of C st u = [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] ;
hence ex v, w being set st u = [v,w] ; ::_thesis: verum
end;
then reconsider f = { [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] where A is Subset of the carrier' of C : verum } as Relation by RELAT_1:def_1;
for u, v1, v2 being set st [u,v1] in f & [u,v2] in f holds
v1 = v2
proof
let u, v1, v2 be set ; ::_thesis: ( [u,v1] in f & [u,v2] in f implies v1 = v2 )
assume that
A1: [u,v1] in f and
A2: [u,v2] in f ; ::_thesis: v1 = v2
consider A being Subset of the carrier' of C such that
A3: [u,v1] = [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] by A1;
A4: v1 = [u,v1] `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 } ] `2 by A3
.= { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
consider A9 being Subset of the carrier' of C such that
A5: [u,v2] = [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] by A2;
A6: v2 = [u,v2] `2
.= [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2 by A5
.= [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2
.= { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
A = [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] `1
.= [u,v1] `1 by A3
.= u
.= [u,v2] `1
.= [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `1 by A5
.= A9 ;
hence v1 = v2 by A4, A6; ::_thesis: verum
end;
then reconsider f = f as Function by FUNCT_1:def_1;
A7: for x being set st x in dom f holds
x in bool the carrier' of C
proof
let x be set ; ::_thesis: ( x in dom f implies x in bool the carrier' of C )
assume x in dom f ; ::_thesis: x in bool the carrier' of C
then consider y being set such that
A8: [x,y] in f by XTUPLE_0:def_12;
consider A being Subset of the carrier' of C such that
A9: [x,y] = [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] by A8;
x = [x,y] `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 } ] `1 by A9
.= A ;
hence x in bool the carrier' of C ; ::_thesis: verum
end;
for x being set st x in bool the carrier' of C holds
x in dom f
proof
let x be set ; ::_thesis: ( x in bool the carrier' of C implies x in dom f )
assume x in bool the carrier' of C ; ::_thesis: x in dom f
then reconsider x = x as Subset of the carrier' of C ;
[x, { o where o is Object of C : for a being Attribute of C st a in x holds
o is-connected-with a } ] in f ;
hence x in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A10: dom f = bool the carrier' of C by A7, TARSKI:1;
rng f c= bool the carrier of C
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in bool the carrier of C )
assume y in rng f ; ::_thesis: y in bool the carrier of C
then consider x being set such that
A11: [x,y] in f by XTUPLE_0:def_13;
consider A being Subset of the carrier' of C such that
A12: [x,y] = [A, { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ] by A11;
A13: { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } or u in the carrier of C )
assume u in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & ( for a being Attribute of C st a in A holds
u9 is-connected-with a ) ) ;
hence u in the carrier of C ; ::_thesis: verum
end;
y = [x,y] `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 } ] `2 by A12
.= { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
hence y in bool the carrier of C by A13; ::_thesis: verum
end;
then reconsider f = f as Function of (bool the carrier' of C),(bool the carrier of C) by A10, FUNCT_2:def_1, RELSET_1:4;
take f ; ::_thesis: for A being Subset of the carrier' of C holds f . 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 f . 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
let A be Subset of the carrier' of C; ::_thesis: f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
consider y being set such that
A14: [A,y] in f by A10, XTUPLE_0:def_12;
consider A9 being Subset of the carrier' of C such that
A15: [A,y] = [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] by A14;
A16: y = [A,y] `2
.= [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `2 by A15
.= { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
A = [A,y] `1
.= [A9, { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ] `1 by A15
.= A9 ;
hence f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by A10, A14, A16, FUNCT_1:def_2; ::_thesis: verum
end;
hence for A being Subset of the carrier' of C holds f . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of (bool the carrier' of C),(bool the carrier of C) st ( for A being Subset of the carrier' 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 carrier' 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
let F1, F2 be Function of (bool the carrier' of C),(bool the carrier of C); ::_thesis: ( ( for A being Subset of the carrier' of C holds F1 . 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 F2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ) implies F1 = F2 )
assume A17: for A being Subset of the carrier' of C holds F1 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: ( ex A being Subset of the carrier' of C st not F2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } or F1 = F2 )
assume A18: for A being Subset of the carrier' of C holds F2 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: F1 = F2
A19: for A being set st A in bool the carrier' of C holds
F1 . A = F2 . A
proof
let A be set ; ::_thesis: ( A in bool the carrier' of C implies F1 . A = F2 . A )
assume A in bool the carrier' of C ; ::_thesis: F1 . A = F2 . A
then reconsider A = A as Subset of the carrier' of C ;
F1 . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by A17
.= F2 . A by A18 ;
hence F1 . A = F2 . A ; ::_thesis: verum
end;
( dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C ) by FUNCT_2:def_1;
hence F1 = F2 by A19, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines AttributeDerivation CONLAT_1:def_4_:_
for C being FormalContext
for b2 being Function of (bool the carrier' of C),(bool the carrier of C) holds
( b2 = AttributeDerivation C iff for A being Subset of the carrier' 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
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
let C be FormalContext; ::_thesis: for o being Object of C holds (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }
let o be Object of C; ::_thesis: (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a }
{o} c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {o} or x in the carrier of C )
assume x in {o} ; ::_thesis: x in the carrier of C
then x = o by TARSKI:def_1;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider t = {o} as Subset of the carrier of C ;
A1: for x being set st x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } holds
x in { a where a is Attribute of C : o is-connected-with a }
proof
set o9 = the Element of t;
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } implies x in { a where a is Attribute of C : o is-connected-with a } )
reconsider o9 = the Element of t as Object of C by TARSKI:def_1;
A2: o9 = o by TARSKI:def_1;
assume x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } ; ::_thesis: x in { a where a is Attribute of C : o is-connected-with a }
then A3: ex x9 being Attribute of C st
( x9 = x & ( for o9 being Object of C st o9 in t holds
o9 is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
o9 is-connected-with x by A3;
hence x in { a where a is Attribute of C : o is-connected-with a } by A2; ::_thesis: verum
end;
A4: for x being set st x in { a where a is Attribute of C : o is-connected-with a } holds
x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a }
proof
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : o is-connected-with a } implies x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } )
assume x in { a where a is Attribute of C : o is-connected-with a } ; ::_thesis: x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a }
then A5: ex x9 being Attribute of C st
( x9 = x & o is-connected-with x9 ) ;
then reconsider x = x as Attribute of C ;
for o9 being Object of C st o9 in t holds
o9 is-connected-with x by A5, TARSKI:def_1;
hence x in { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } ; ::_thesis: verum
end;
(ObjectDerivation C) . t = { a where a is Attribute of C : for o9 being Object of C st o9 in t holds
o9 is-connected-with a } by Def3;
hence (ObjectDerivation C) . {o} = { a where a is Attribute of C : o is-connected-with a } by A1, A4, TARSKI:1; ::_thesis: verum
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 }
proof
let C be FormalContext; ::_thesis: for a being Attribute of C holds (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }
let a be Attribute of C; ::_thesis: (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a }
{a} c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {a} or x in the carrier' of C )
assume x in {a} ; ::_thesis: x in the carrier' of C
then x = a by TARSKI:def_1;
hence x in the carrier' of C ; ::_thesis: verum
end;
then reconsider t = {a} as Subset of the carrier' of C ;
A1: for x being set st x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } holds
x in { o where o is Object of C : o is-connected-with a }
proof
set a9 = the Element of t;
let x be set ; ::_thesis: ( x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } implies x in { o where o is Object of C : o is-connected-with a } )
reconsider a9 = the Element of t as Attribute of C by TARSKI:def_1;
A2: a9 = a by TARSKI:def_1;
assume x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } ; ::_thesis: x in { o where o is Object of C : o is-connected-with a }
then A3: ex x9 being Object of C st
( x9 = x & ( for a9 being Attribute of C st a9 in t holds
x9 is-connected-with a9 ) ) ;
then reconsider x = x as Object of C ;
x is-connected-with a9 by A3;
hence x in { o where o is Object of C : o is-connected-with a } by A2; ::_thesis: verum
end;
A4: for x being set st x in { o where o is Object of C : o is-connected-with a } holds
x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 }
proof
let x be set ; ::_thesis: ( x in { o where o is Object of C : o is-connected-with a } implies x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } )
assume x in { o where o is Object of C : o is-connected-with a } ; ::_thesis: x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 }
then A5: ex x9 being Object of C st
( x9 = x & x9 is-connected-with a ) ;
then reconsider x = x as Object of C ;
for a9 being Attribute of C st a9 in t holds
x is-connected-with a9 by A5, TARSKI:def_1;
hence x in { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } ; ::_thesis: verum
end;
(AttributeDerivation C) . t = { o where o is Object of C : for a9 being Attribute of C st a9 in t holds
o is-connected-with a9 } by Def4;
hence (AttributeDerivation C) . {a} = { o where o is Object of C : o is-connected-with a } by A1, A4, TARSKI:1; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for O1, O2 being Subset of the carrier of C st O1 c= O2 holds
(ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let O1, O2 be Subset of the carrier of C; ::_thesis: ( O1 c= O2 implies (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1 )
assume A1: O1 c= O2 ; ::_thesis: (ObjectDerivation C) . O2 c= (ObjectDerivation C) . O1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . O2 or x in (ObjectDerivation C) . O1 )
assume x in (ObjectDerivation C) . O2 ; ::_thesis: x in (ObjectDerivation C) . O1
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } by Def3;
then consider x9 being Attribute of C such that
A2: x9 = x and
A3: for o being Object of C st o in O2 holds
o is-connected-with x9 ;
for o being Object of C st o in O1 holds
o is-connected-with x9 by A1, A3;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } by A2;
hence x in (ObjectDerivation C) . O1 by Def3; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for A1, A2 being Subset of the carrier' of C st A1 c= A2 holds
(AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
let A1, A2 be Subset of the carrier' of C; ::_thesis: ( A1 c= A2 implies (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1 )
assume A1: A1 c= A2 ; ::_thesis: (AttributeDerivation C) . A2 c= (AttributeDerivation C) . A1
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . A2 or x in (AttributeDerivation C) . A1 )
assume x in (AttributeDerivation C) . A2 ; ::_thesis: x in (AttributeDerivation C) . A1
then x in { o where o is Object of C : for a being Attribute of C st a in A2 holds
o is-connected-with a } by Def4;
then consider x9 being Object of C such that
A2: x9 = x and
A3: for a being Attribute of C st a in A2 holds
x9 is-connected-with a ;
for a being Attribute of C st a in A1 holds
x9 is-connected-with a by A1, A3;
then x in { o where o is Object of C : for a being Attribute of C st a in A1 holds
o is-connected-with a } by A2;
hence x in (AttributeDerivation C) . A1 by Def4; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for O being Subset of the carrier of C holds O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
let O be Subset of the carrier of C; ::_thesis: O c= (AttributeDerivation C) . ((ObjectDerivation C) . O)
set A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
for x being set st x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
x in the carrier' of C
proof
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } implies x in the carrier' of C )
assume x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: x in the carrier' of C
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } as Subset of the carrier' of C by TARSKI:def_3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . ((ObjectDerivation C) . O) )
assume A1: x in O ; ::_thesis: x in (AttributeDerivation C) . ((ObjectDerivation C) . O)
then reconsider x = x as Object of C ;
A2: for a being Attribute of C st a in A holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A implies x is-connected-with a )
assume a in A ; ::_thesis: x is-connected-with a
then ex a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in O holds
o is-connected-with a9 ) ) ;
hence x is-connected-with a by A1; ::_thesis: verum
end;
(AttributeDerivation C) . A = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by Def4;
then x in (AttributeDerivation C) . A by A2;
hence x in (AttributeDerivation C) . ((ObjectDerivation C) . O) by Def3; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for A being Subset of the carrier' of C holds A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
let A be Subset of the carrier' of C; ::_thesis: A c= (ObjectDerivation C) . ((AttributeDerivation C) . A)
set O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
for x being set st x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
x in the carrier of C
proof
let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } implies x in the carrier of C )
assume x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: x in the carrier of C
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } as Subset of the carrier of C by TARSKI:def_3;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . ((AttributeDerivation C) . A) )
assume A1: x in A ; ::_thesis: x in (ObjectDerivation C) . ((AttributeDerivation C) . A)
then reconsider x = x as Attribute of C ;
A2: for o being Object of C st o in O holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O implies o is-connected-with x )
assume o in O ; ::_thesis: o is-connected-with x
then ex o9 being Object of C st
( o9 = o & ( for a being Attribute of C st a in A holds
o9 is-connected-with a ) ) ;
hence o is-connected-with x by A1; ::_thesis: verum
end;
(ObjectDerivation C) . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by Def3;
then x in (ObjectDerivation C) . O by A2;
hence x in (ObjectDerivation C) . ((AttributeDerivation C) . A) by Def4; ::_thesis: verum
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))
proof
let C be FormalContext; ::_thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
let O be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O))
set A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
set O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ;
set A9 = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ;
A1: for x being set st x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } holds
x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } implies x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } )
assume x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
then A2: ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O implies o is-connected-with x )
assume A3: o in O ; ::_thesis: o is-connected-with x
now__::_thesis:_(_(_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_o_is-connected-with_x_)_or_(_not_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in_O_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_o_is-connected-with_x_)_)
percases ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } or not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ) ;
case o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: o is-connected-with x
hence o is-connected-with x by A2; ::_thesis: verum
end;
case not o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: o is-connected-with x
then consider a being Attribute of C such that
A4: a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } and
A5: not o is-connected-with a ;
ex a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in O holds
o is-connected-with a9 ) ) by A4;
hence o is-connected-with x by A3, A5; ::_thesis: verum
end;
end;
end;
hence o is-connected-with x ; ::_thesis: verum
end;
hence x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: verum
end;
for x being set st x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } implies x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } )
assume A6: x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } implies o is-connected-with x )
assume o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: o is-connected-with x
then ex o9 being Object of C st
( o9 = o & ( for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o9 is-connected-with a ) ) ;
hence o is-connected-with x by A6; ::_thesis: verum
end;
hence x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: verum
end;
then A7: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } by A1, TARSKI:1;
{ a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or x in the carrier' of C )
assume x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: x in the carrier' of C
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } as Subset of the carrier' of C ;
{ o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } or x in the carrier of C )
assume x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x in the carrier of C
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } holds
o is-connected-with a } as Subset of the carrier of C ;
( A = (ObjectDerivation C) . O & O9 = (AttributeDerivation C) . A ) by Def3, Def4;
hence (ObjectDerivation C) . O = (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . O)) by A7, Def3; ::_thesis: verum
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))
proof
let C be FormalContext; ::_thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
let A be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A))
set O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
set A9 = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ;
set O9 = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ;
A1: for x being set st x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } holds
x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } implies x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } )
assume x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a }
then A2: ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
x9 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A implies x is-connected-with a )
assume A3: a in A ; ::_thesis: x is-connected-with a
now__::_thesis:_(_(_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_x_is-connected-with_a_)_or_(_not_a_in__{__a_where_a_is_Attribute_of_C_:_for_o_being_Object_of_C_st_o_in__{__o_where_o_is_Object_of_C_:_for_a_being_Attribute_of_C_st_a_in_A_holds_
o_is-connected-with_a__}__holds_
o_is-connected-with_a__}__&_x_is-connected-with_a_)_)
percases ( a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } or not a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ) ;
case a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x is-connected-with a
hence x is-connected-with a by A2; ::_thesis: verum
end;
case not a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x is-connected-with a
then consider o being Object of C such that
A4: o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } and
A5: not o is-connected-with a ;
ex o9 being Object of C st
( o9 = o & ( for a being Attribute of C st a in A holds
o9 is-connected-with a ) ) by A4;
hence x is-connected-with a by A3, A5; ::_thesis: verum
end;
end;
end;
hence x is-connected-with a ; ::_thesis: verum
end;
hence x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: verum
end;
for x being set st x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } implies x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } )
assume A6: x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a }
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } implies x is-connected-with a )
assume a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x is-connected-with a
then ex a9 being Attribute of C st
( a9 = a & ( for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a9 ) ) ;
hence x is-connected-with a by A6; ::_thesis: verum
end;
hence x in { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: verum
end;
then A7: { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } = { o where o is Object of C : for a being Attribute of C st a in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } holds
o is-connected-with a } by A1, TARSKI:1;
{ o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } or x in the carrier of C )
assume x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ; ::_thesis: x in the carrier of C
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider O = { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } as Subset of the carrier of C ;
{ a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } or x in the carrier' of C )
assume x in { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } ; ::_thesis: x in the carrier' of C
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A9 = { a where a is Attribute of C : for o being Object of C st o in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } holds
o is-connected-with a } as Subset of the carrier' of C ;
( O = (AttributeDerivation C) . A & A9 = (ObjectDerivation C) . O ) by Def3, Def4;
hence (AttributeDerivation C) . A = (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . A)) by A7, Def4; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )
let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C )
A1: ( [:O,A:] c= the Information of C implies O c= (AttributeDerivation C) . A )
proof
assume A2: [:O,A:] c= the Information of C ; ::_thesis: O c= (AttributeDerivation C) . A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in O or x in (AttributeDerivation C) . A )
assume A3: x in O ; ::_thesis: x in (AttributeDerivation C) . A
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A implies x is-connected-with a )
consider z being set such that
A4: z = [x,a] ;
assume a in A ; ::_thesis: x is-connected-with a
then z in [:O,A:] by A3, A4, ZFMISC_1:def_2;
hence x is-connected-with a by A2, A4, Def2; ::_thesis: verum
end;
then x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } ;
hence x in (AttributeDerivation C) . A by Def4; ::_thesis: verum
end;
( O c= (AttributeDerivation C) . A implies [:O,A:] c= the Information of C )
proof
assume O c= (AttributeDerivation C) . A ; ::_thesis: [:O,A:] c= the Information of C
then A5: O c= { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by Def4;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C )
assume z in [:O,A:] ; ::_thesis: z in the Information of C
then consider x, y being set such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def_2;
reconsider y = y as Attribute of C by A7;
reconsider x = x as Object of C by A6;
x in { o where o is Object of C : for a being Attribute of C st a in A holds
o is-connected-with a } by A5, A6;
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A holds
x9 is-connected-with a ) ) ;
then x is-connected-with y by A7;
hence z in the Information of C by A8, Def2; ::_thesis: verum
end;
hence ( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )
let A be Subset of the carrier' of C; ::_thesis: ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C )
A1: ( [:O,A:] c= the Information of C implies A c= (ObjectDerivation C) . O )
proof
assume A2: [:O,A:] c= the Information of C ; ::_thesis: A c= (ObjectDerivation C) . O
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in (ObjectDerivation C) . O )
assume A3: x in A ; ::_thesis: x in (ObjectDerivation C) . O
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O implies o is-connected-with x )
consider z being set such that
A4: z = [o,x] ;
assume o in O ; ::_thesis: o is-connected-with x
then z in [:O,A:] by A3, A4, ZFMISC_1:def_2;
hence o is-connected-with x by A2, A4, Def2; ::_thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ;
hence x in (ObjectDerivation C) . O by Def3; ::_thesis: verum
end;
( A c= (ObjectDerivation C) . O implies [:O,A:] c= the Information of C )
proof
assume A c= (ObjectDerivation C) . O ; ::_thesis: [:O,A:] c= the Information of C
then A5: A c= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by Def3;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in [:O,A:] or z in the Information of C )
assume z in [:O,A:] ; ::_thesis: z in the Information of C
then consider x, y being set such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def_2;
reconsider y = y as Attribute of C by A7;
reconsider x = x as Object of C by A6;
y in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } by A5, A7;
then ex y9 being Attribute of C st
( y9 = y & ( for o being Object of C st o in O holds
o is-connected-with y9 ) ) ;
then x is-connected-with y by A6;
hence z in the Information of C by A8, Def2; ::_thesis: verum
end;
hence ( A c= (ObjectDerivation C) . O iff [:O,A:] c= the Information of C ) by A1; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: for A being Subset of the carrier' of C holds
( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
let A be Subset of the carrier' of C; ::_thesis: ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O )
( O c= (AttributeDerivation C) . A iff [:O,A:] c= the Information of C ) by Th9;
hence ( O c= (AttributeDerivation C) . A iff A c= (ObjectDerivation C) . O ) by Th10; ::_thesis: verum
end;
definition
let C be FormalContext;
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 is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C)
proof
A1: rng (ObjectDerivation C) c= the carrier of (BoolePoset the carrier' of C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (ObjectDerivation C) or x in the carrier of (BoolePoset the carrier' of C) )
assume x in rng (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of C)
then x in bool the carrier' of C ;
then A2: x in the carrier of (BooleLatt the carrier' of C) by LATTICE3:def_1;
LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) by LATTICE3:def_2;
hence x in the carrier of (BoolePoset the carrier' of C) by A2, YELLOW_1:def_2; ::_thesis: verum
end;
A3: LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) by LATTICE3:def_2;
A4: for x being set st x in the carrier of (BoolePoset the carrier of C) holds
x in dom (ObjectDerivation C)
proof
let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier of C) implies x in dom (ObjectDerivation C) )
assume x in the carrier of (BoolePoset the carrier of C) ; ::_thesis: x in dom (ObjectDerivation C)
then x in the carrier of (LattPOSet (BooleLatt the carrier of C)) by YELLOW_1:def_2;
then x in bool the carrier of C by A3, LATTICE3:def_1;
hence x in dom (ObjectDerivation C) by FUNCT_2:def_1; ::_thesis: verum
end;
for x being set st x in dom (ObjectDerivation C) holds
x in the carrier of (BoolePoset the carrier of C)
proof
let x be set ; ::_thesis: ( x in dom (ObjectDerivation C) implies x in the carrier of (BoolePoset the carrier of C) )
assume x in dom (ObjectDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of C)
then x in bool the carrier of C ;
then x in the carrier of (BooleLatt the carrier of C) by LATTICE3:def_1;
hence x in the carrier of (BoolePoset the carrier of C) by A3, YELLOW_1:def_2; ::_thesis: verum
end;
then dom (ObjectDerivation C) = the carrier of (BoolePoset the carrier of C) by A4, TARSKI:1;
then reconsider g = ObjectDerivation C as Function of the carrier of (BoolePoset the carrier of C), the carrier of (BoolePoset the carrier' of C) by A1, FUNCT_2:def_1, RELSET_1:4;
g is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ;
hence ObjectDerivation C is Function of (BoolePoset the carrier of C),(BoolePoset the carrier' of C) ; ::_thesis: verum
end;
end;
:: deftheorem defines phi CONLAT_1:def_5_:_
for C being FormalContext holds phi C = ObjectDerivation C;
definition
let C be FormalContext;
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 is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C)
proof
A1: rng (AttributeDerivation C) c= the carrier of (BoolePoset the carrier of C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (AttributeDerivation C) or x in the carrier of (BoolePoset the carrier of C) )
assume x in rng (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier of C)
then x in bool the carrier of C ;
then A2: x in the carrier of (BooleLatt the carrier of C) by LATTICE3:def_1;
LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) by LATTICE3:def_2;
hence x in the carrier of (BoolePoset the carrier of C) by A2, YELLOW_1:def_2; ::_thesis: verum
end;
A3: LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) by LATTICE3:def_2;
A4: for x being set st x in the carrier of (BoolePoset the carrier' of C) holds
x in dom (AttributeDerivation C)
proof
let x be set ; ::_thesis: ( x in the carrier of (BoolePoset the carrier' of C) implies x in dom (AttributeDerivation C) )
assume x in the carrier of (BoolePoset the carrier' of C) ; ::_thesis: x in dom (AttributeDerivation C)
then x in the carrier of (LattPOSet (BooleLatt the carrier' of C)) by YELLOW_1:def_2;
then x in bool the carrier' of C by A3, LATTICE3:def_1;
hence x in dom (AttributeDerivation C) by FUNCT_2:def_1; ::_thesis: verum
end;
for x being set st x in dom (AttributeDerivation C) holds
x in the carrier of (BoolePoset the carrier' of C)
proof
let x be set ; ::_thesis: ( x in dom (AttributeDerivation C) implies x in the carrier of (BoolePoset the carrier' of C) )
assume x in dom (AttributeDerivation C) ; ::_thesis: x in the carrier of (BoolePoset the carrier' of C)
then x in bool the carrier' of C ;
then x in the carrier of (BooleLatt the carrier' of C) by LATTICE3:def_1;
hence x in the carrier of (BoolePoset the carrier' of C) by A3, YELLOW_1:def_2; ::_thesis: verum
end;
then dom (AttributeDerivation C) = the carrier of (BoolePoset the carrier' of C) by A4, TARSKI:1;
hence AttributeDerivation C is Function of (BoolePoset the carrier' of C),(BoolePoset the carrier of C) by A1, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum
end;
end;
:: deftheorem defines psi CONLAT_1:def_6_:_
for C being FormalContext holds psi C = AttributeDerivation C;
definition
let P, R be non empty RelStr ;
let Con be Connection of P,R;
attrCon is co-Galois means :Def7: :: CONLAT_1:def 7
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 Def7 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) ) ) ) );
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 ) )
proof
let P, R be non empty Poset; ::_thesis: 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 ) )
let Con be Connection of P,R; ::_thesis: 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 ) )
let f be Function of P,R; ::_thesis: 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 ) )
let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( 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 ) ) )
assume A1: Con = [f,g] ; ::_thesis: ( 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 ) )
A2: now__::_thesis:_(_(_for_p_being_Element_of_P
for_r_being_Element_of_R_holds_
(_p_<=_g_._r_iff_r_<=_f_._p_)_)_implies_Con_is_co-Galois_)
assume A3: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ; ::_thesis: Con is co-Galois
for p1, p2 being Element of P st p1 <= p2 holds
for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2
proof
let p1, p2 be Element of P; ::_thesis: ( p1 <= p2 implies for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2 )
assume A4: p1 <= p2 ; ::_thesis: for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2
let r1, r2 be Element of R; ::_thesis: ( r1 = f . p1 & r2 = f . p2 implies r1 >= r2 )
assume A5: ( r1 = f . p1 & r2 = f . p2 ) ; ::_thesis: r1 >= r2
p2 <= g . (f . p2) by A3;
then p1 <= g . (f . p2) by A4, ORDERS_2:3;
hence r1 >= r2 by A3, A5; ::_thesis: verum
end;
then A6: f is antitone by WAYBEL_0:def_5;
for r1, r2 being Element of R st r1 <= r2 holds
for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2
proof
let r1, r2 be Element of R; ::_thesis: ( r1 <= r2 implies for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2 )
assume A7: r1 <= r2 ; ::_thesis: for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2
let p1, p2 be Element of P; ::_thesis: ( p1 = g . r1 & p2 = g . r2 implies p1 >= p2 )
assume A8: ( p1 = g . r1 & p2 = g . r2 ) ; ::_thesis: p1 >= p2
r2 <= f . (g . r2) by A3;
then r1 <= f . (g . r2) by A7, ORDERS_2:3;
hence p1 >= p2 by A3, A8; ::_thesis: verum
end;
then A9: g is antitone by WAYBEL_0:def_5;
for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g . (f . p1) & r1 <= f . (g . r1) ) by A3;
hence Con is co-Galois by A1, A6, A9, Def7; ::_thesis: verum
end;
now__::_thesis:_(_Con_is_co-Galois_implies_for_p_being_Element_of_P
for_r_being_Element_of_R_holds_
(_p_<=_g_._r_iff_r_<=_f_._p_)_)
assume Con is co-Galois ; ::_thesis: for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p )
then consider f9 being Function of P,R, g9 being Function of R,P such that
A10: Con = [f9,g9] and
A11: f9 is antitone and
A12: g9 is antitone and
A13: for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7;
A14: g = [f,g] `2
.= Con `2 by A1
.= [f9,g9] `2 by A10
.= g9 ;
A15: f = [f,g] `1
.= Con `1 by A1
.= [f9,g9] `1 by A10
.= f9 ;
A16: for p being Element of P
for r being Element of R st r <= f . p holds
p <= g . r
proof
let p be Element of P; ::_thesis: for r being Element of R st r <= f . p holds
p <= g . r
let r be Element of R; ::_thesis: ( r <= f . p implies p <= g . r )
assume r <= f . p ; ::_thesis: p <= g . r
then A17: g . r >= g . (f . p) by A12, A14, WAYBEL_0:def_5;
p <= g . (f . p) by A13, A15, A14;
hence p <= g . r by A17, ORDERS_2:3; ::_thesis: verum
end;
for p being Element of P
for r being Element of R st p <= g . r holds
r <= f . p
proof
let p be Element of P; ::_thesis: for r being Element of R st p <= g . r holds
r <= f . p
let r be Element of R; ::_thesis: ( p <= g . r implies r <= f . p )
assume p <= g . r ; ::_thesis: r <= f . p
then A18: f . p >= f . (g . r) by A11, A15, WAYBEL_0:def_5;
r <= f . (g . r) by A13, A15, A14;
hence r <= f . p by A18, ORDERS_2:3; ::_thesis: verum
end;
hence for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) by A16; ::_thesis: verum
end;
hence ( 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 ) ) by A2; ::_thesis: verum
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) )
proof
let P, R be non empty Poset; ::_thesis: 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) )
let Con be Connection of P,R; ::_thesis: ( Con is co-Galois implies 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) ) )
assume Con is co-Galois ; ::_thesis: 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) )
then consider f9 being Function of P,R, g9 being Function of R,P such that
A1: Con = [f9,g9] and
A2: f9 is antitone and
A3: g9 is antitone and
A4: for p1, p2 being Element of P
for r1, r2 being Element of R holds
( p1 <= g9 . (f9 . p1) & r1 <= f9 . (g9 . r1) ) by Def7;
let f be Function of P,R; ::_thesis: for g being Function of R,P st Con = [f,g] holds
( f = f * (g * f) & g = g * (f * g) )
let g be Function of R,P; ::_thesis: ( Con = [f,g] implies ( f = f * (g * f) & g = g * (f * g) ) )
assume A5: Con = [f,g] ; ::_thesis: ( f = f * (g * f) & g = g * (f * g) )
A6: f = [f,g] `1
.= Con `1 by A5
.= [f9,g9] `1 by A1
.= f9 ;
A7: g = [f,g] `2
.= Con `2 by A5
.= [f9,g9] `2 by A1
.= g9 ;
A8: dom g = the carrier of R by FUNCT_2:def_1;
A9: dom f = the carrier of P by FUNCT_2:def_1;
A10: for x being set st x in the carrier of P holds
f . x = (f * (g * f)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of P implies f . x = (f * (g * f)) . x )
assume x in the carrier of P ; ::_thesis: f . x = (f * (g * f)) . x
then reconsider x = x as Element of P ;
x <= g . (f . x) by A4, A6, A7;
then A11: f . x >= f . (g . (f . x)) by A2, A6, WAYBEL_0:def_5;
f . x <= f . (g . (f . x)) by A4, A6, A7;
then f . x = f . (g . (f . x)) by A11, ORDERS_2:2;
then A12: f . x = f . ((g * f) . x) by A9, FUNCT_1:13;
f . x is Element of R ;
then x in dom (g * f) by A9, A8, FUNCT_1:11;
hence f . x = (f * (g * f)) . x by A12, FUNCT_1:13; ::_thesis: verum
end;
A13: for x being set st x in the carrier of R holds
g . x = (g * (f * g)) . x
proof
let x be set ; ::_thesis: ( x in the carrier of R implies g . x = (g * (f * g)) . x )
assume x in the carrier of R ; ::_thesis: g . x = (g * (f * g)) . x
then reconsider x = x as Element of R ;
x <= f . (g . x) by A4, A6, A7;
then A14: g . x >= g . (f . (g . x)) by A3, A7, WAYBEL_0:def_5;
g . x <= g . (f . (g . x)) by A4, A6, A7;
then g . x = g . (f . (g . x)) by A14, ORDERS_2:2;
then A15: g . x = g . ((f * g) . x) by A8, FUNCT_1:13;
g . x is Element of P ;
then x in dom (f * g) by A9, A8, FUNCT_1:11;
hence g . x = (g * (f * g)) . x by A15, FUNCT_1:13; ::_thesis: verum
end;
( dom (f * (g * f)) = the carrier of P & dom (g * (f * g)) = the carrier of R ) by FUNCT_2:def_1;
hence ( f = f * (g * f) & g = g * (f * g) ) by A9, A8, A10, A13, FUNCT_1:2; ::_thesis: verum
end;
theorem :: CONLAT_1:14
for C being FormalContext holds [(phi C),(psi C)] is co-Galois
proof
let C be FormalContext; ::_thesis: [(phi C),(psi C)] is co-Galois
A1: LattPOSet (BooleLatt the carrier' of C) = RelStr(# the carrier of (BooleLatt the carrier' of C),(LattRel (BooleLatt the carrier' of C)) #) by LATTICE3:def_2;
A2: LattPOSet (BooleLatt the carrier of C) = RelStr(# the carrier of (BooleLatt the carrier of C),(LattRel (BooleLatt the carrier of C)) #) by LATTICE3:def_2;
A3: for x being Element of (BoolePoset the carrier of C)
for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds
x <= (psi C) . y
proof
let x be Element of (BoolePoset the carrier of C); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st y <= (phi C) . x holds
x <= (psi C) . y
let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( y <= (phi C) . x implies x <= (psi C) . y )
assume y <= (phi C) . x ; ::_thesis: x <= (psi C) . y
then [y,((phi C) . x)] in the InternalRel of (BoolePoset the carrier' of C) by ORDERS_2:def_5;
then A4: [y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
reconsider x9 = (phi C) . x as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
reconsider x = x as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
reconsider x = x as Subset of the carrier of C by LATTICE3:def_1;
reconsider y = y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
y [= x9 by A4, FILTER_1:31;
then A5: y "\/" x9 = x9 by LATTICES:def_3;
reconsider x9 = x9 as Subset of the carrier' of C by LATTICE3:def_1;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1;
for z being set st z in y holds
z in x9 by A5, XBOOLE_0:def_3;
then y c= x9 by TARSKI:def_3;
then A6: (AttributeDerivation C) . x9 c= (AttributeDerivation C) . y by Th4;
reconsider y = y as Element of (BoolePoset the carrier' of C) ;
reconsider y9 = (psi C) . y as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
reconsider y9 = y9 as Subset of the carrier of C by LATTICE3:def_1;
reconsider y9 = y9 as Element of (BooleLatt the carrier of C) ;
A7: x c= (AttributeDerivation C) . ((ObjectDerivation C) . x) by Th5;
reconsider x = x as Subset of the carrier of C ;
reconsider x = x as Element of (BooleLatt the carrier of C) ;
x "\/" y9 = y9 by A6, A7, XBOOLE_1:1, XBOOLE_1:12;
then x [= y9 by LATTICES:def_3;
then [x,((psi C) . y)] in LattRel (BooleLatt the carrier of C) by FILTER_1:31;
then [x,((psi C) . y)] in the InternalRel of (BoolePoset the carrier of C) by A2, YELLOW_1:def_2;
hence x <= (psi C) . y by ORDERS_2:def_5; ::_thesis: verum
end;
for x being Element of (BoolePoset the carrier of C)
for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . x
proof
let x be Element of (BoolePoset the carrier of C); ::_thesis: for y being Element of (BoolePoset the carrier' of C) st x <= (psi C) . y holds
y <= (phi C) . x
let y be Element of (BoolePoset the carrier' of C); ::_thesis: ( x <= (psi C) . y implies y <= (phi C) . x )
assume x <= (psi C) . y ; ::_thesis: y <= (phi C) . x
then [x,((psi C) . y)] in the InternalRel of (BoolePoset the carrier of C) by ORDERS_2:def_5;
then A8: [x,((psi C) . y)] in LattRel (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
reconsider y9 = (psi C) . y as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
reconsider y = y as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
reconsider y = y as Subset of the carrier' of C by LATTICE3:def_1;
reconsider x = x as Element of (BooleLatt the carrier of C) by A2, YELLOW_1:def_2;
x [= y9 by A8, FILTER_1:31;
then A9: x "\/" y9 = y9 by LATTICES:def_3;
reconsider y9 = y9 as Subset of the carrier of C by LATTICE3:def_1;
reconsider x = x as Subset of the carrier of C by LATTICE3:def_1;
for z being set st z in x holds
z in y9 by A9, XBOOLE_0:def_3;
then A10: x c= y9 by TARSKI:def_3;
reconsider x = x, y9 = y9 as Subset of the carrier of C ;
A11: (ObjectDerivation C) . y9 c= (ObjectDerivation C) . x by A10, Th3;
reconsider x = x as Element of (BoolePoset the carrier of C) ;
reconsider x9 = (phi C) . x as Element of (BooleLatt the carrier' of C) by A1, YELLOW_1:def_2;
reconsider x9 = x9 as Subset of the carrier' of C by LATTICE3:def_1;
reconsider x9 = x9 as Element of (BooleLatt the carrier' of C) ;
A12: y c= (ObjectDerivation C) . ((AttributeDerivation C) . y) by Th6;
reconsider y = y as Element of (BooleLatt the carrier' of C) ;
y "\/" x9 = x9 by A11, A12, XBOOLE_1:1, XBOOLE_1:12;
then y [= x9 by LATTICES:def_3;
then [y,((phi C) . x)] in LattRel (BooleLatt the carrier' of C) by FILTER_1:31;
then [y,((phi C) . x)] in the InternalRel of (BoolePoset the carrier' of C) by A1, YELLOW_1:def_2;
hence y <= (phi C) . x by ORDERS_2:def_5; ::_thesis: verum
end;
hence [(phi C),(psi C)] is co-Galois by A3, Th12; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for O1, O2 being Subset of the carrier of C holds (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
let O1, O2 be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
reconsider O9 = O1 \/ O2 as Subset of the carrier of C ;
A1: for x being set st x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) holds
x in (ObjectDerivation C) . O9
proof
let x be set ; ::_thesis: ( x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) implies x in (ObjectDerivation C) . O9 )
assume A2: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) ; ::_thesis: x in (ObjectDerivation C) . O9
then x in (ObjectDerivation C) . O1 by XBOOLE_0:def_4;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } by Def3;
then A3: ex x1 being Attribute of C st
( x1 = x & ( for o being Object of C st o in O1 holds
o is-connected-with x1 ) ) ;
x in (ObjectDerivation C) . O2 by A2, XBOOLE_0:def_4;
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } by Def3;
then A4: ex x2 being Attribute of C st
( x2 = x & ( for o being Object of C st o in O2 holds
o is-connected-with x2 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O1 \/ O2 holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O1 \/ O2 implies o is-connected-with x )
assume A5: o in O1 \/ O2 ; ::_thesis: o is-connected-with x
now__::_thesis:_(_(_o_in_O1_&_o_is-connected-with_x_)_or_(_o_in_O2_&_o_is-connected-with_x_)_)
percases ( o in O1 or o in O2 ) by A5, XBOOLE_0:def_3;
case o in O1 ; ::_thesis: o is-connected-with x
hence o is-connected-with x by A3; ::_thesis: verum
end;
case o in O2 ; ::_thesis: o is-connected-with x
hence o is-connected-with x by A4; ::_thesis: verum
end;
end;
end;
hence o is-connected-with x ; ::_thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } ;
hence x in (ObjectDerivation C) . O9 by Def3; ::_thesis: verum
end;
for x being set st x in (ObjectDerivation C) . (O1 \/ O2) holds
x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
proof
let x be set ; ::_thesis: ( x in (ObjectDerivation C) . (O1 \/ O2) implies x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) )
assume x in (ObjectDerivation C) . (O1 \/ O2) ; ::_thesis: x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2)
then x in { a where a is Attribute of C : for o being Object of C st o in O9 holds
o is-connected-with a } by Def3;
then A6: ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in O9 holds
o is-connected-with x9 ) ) ;
then reconsider x = x as Attribute of C ;
for o being Object of C st o in O2 holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O2 implies o is-connected-with x )
assume o in O2 ; ::_thesis: o is-connected-with x
then o in O9 by XBOOLE_0:def_3;
hence o is-connected-with x by A6; ::_thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O2 holds
o is-connected-with a } ;
then A7: x in (ObjectDerivation C) . O2 by Def3;
for o being Object of C st o in O1 holds
o is-connected-with x
proof
let o be Object of C; ::_thesis: ( o in O1 implies o is-connected-with x )
assume o in O1 ; ::_thesis: o is-connected-with x
then o in O9 by XBOOLE_0:def_3;
hence o is-connected-with x by A6; ::_thesis: verum
end;
then x in { a where a is Attribute of C : for o being Object of C st o in O1 holds
o is-connected-with a } ;
then x in (ObjectDerivation C) . O1 by Def3;
hence x in ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (ObjectDerivation C) . (O1 \/ O2) = ((ObjectDerivation C) . O1) /\ ((ObjectDerivation C) . O2) by A1, TARSKI:1; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for A1, A2 being Subset of the carrier' of C holds (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
let A1, A2 be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
reconsider A9 = A1 \/ A2 as Subset of the carrier' of C ;
A1: for x being set st x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) holds
x in (AttributeDerivation C) . A9
proof
let x be set ; ::_thesis: ( x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) implies x in (AttributeDerivation C) . A9 )
assume A2: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) ; ::_thesis: x in (AttributeDerivation C) . A9
then x in (AttributeDerivation C) . A1 by XBOOLE_0:def_4;
then x in { o where o is Object of C : for a being Attribute of C st a in A1 holds
o is-connected-with a } by Def4;
then A3: ex x1 being Object of C st
( x1 = x & ( for a being Attribute of C st a in A1 holds
x1 is-connected-with a ) ) ;
x in (AttributeDerivation C) . A2 by A2, XBOOLE_0:def_4;
then x in { o where o is Object of C : for a being Attribute of C st a in A2 holds
o is-connected-with a } by Def4;
then A4: ex x2 being Object of C st
( x2 = x & ( for a being Attribute of C st a in A2 holds
x2 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A1 \/ A2 holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A1 \/ A2 implies x is-connected-with a )
assume A5: a in A1 \/ A2 ; ::_thesis: x is-connected-with a
now__::_thesis:_(_(_a_in_A1_&_x_is-connected-with_a_)_or_(_a_in_A2_&_x_is-connected-with_a_)_)
percases ( a in A1 or a in A2 ) by A5, XBOOLE_0:def_3;
case a in A1 ; ::_thesis: x is-connected-with a
hence x is-connected-with a by A3; ::_thesis: verum
end;
case a in A2 ; ::_thesis: x is-connected-with a
hence x is-connected-with a by A4; ::_thesis: verum
end;
end;
end;
hence x is-connected-with a ; ::_thesis: verum
end;
then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
hence x in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum
end;
for x being set st x in (AttributeDerivation C) . (A1 \/ A2) holds
x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
proof
let x be set ; ::_thesis: ( x in (AttributeDerivation C) . (A1 \/ A2) implies x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) )
assume x in (AttributeDerivation C) . (A1 \/ A2) ; ::_thesis: x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2)
then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } by Def4;
then A6: ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in A9 holds
x9 is-connected-with a ) ) ;
then reconsider x = x as Object of C ;
for a being Attribute of C st a in A2 holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A2 implies x is-connected-with a )
assume a in A2 ; ::_thesis: x is-connected-with a
then a in A9 by XBOOLE_0:def_3;
hence x is-connected-with a by A6; ::_thesis: verum
end;
then x in { o where o is Object of C : for a being Attribute of C st a in A2 holds
o is-connected-with a } ;
then A7: x in (AttributeDerivation C) . A2 by Def4;
for a being Attribute of C st a in A1 holds
x is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A1 implies x is-connected-with a )
assume a in A1 ; ::_thesis: x is-connected-with a
then a in A9 by XBOOLE_0:def_3;
hence x is-connected-with a by A6; ::_thesis: verum
end;
then x in { o where o is Object of C : for a being Attribute of C st a in A1 holds
o is-connected-with a } ;
then x in (AttributeDerivation C) . A1 by Def4;
hence x in ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A7, XBOOLE_0:def_4; ::_thesis: verum
end;
hence (AttributeDerivation C) . (A1 \/ A2) = ((AttributeDerivation C) . A1) /\ ((AttributeDerivation C) . A2) by A1, TARSKI:1; ::_thesis: verum
end;
theorem Th17: :: CONLAT_1:17
for C being FormalContext holds (ObjectDerivation C) . {} = the carrier' of C
proof
let C be FormalContext; ::_thesis: (ObjectDerivation C) . {} = the carrier' of C
reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
set A = { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } ;
A1: for x being set st x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } holds
x in the carrier' of C
proof
let x be set ; ::_thesis: ( x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } implies x in the carrier' of C )
assume x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } ; ::_thesis: x in the carrier' of C
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in e holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; ::_thesis: verum
end;
A2: for x being set st x in the carrier' of C holds
x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in the carrier' of C implies x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } )
assume x in the carrier' of C ; ::_thesis: x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a }
then reconsider x = x as Attribute of C ;
for o being Object of C st o in e holds
o is-connected-with x ;
hence x in { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } ; ::_thesis: verum
end;
(ObjectDerivation C) . e = { a where a is Attribute of C : for o being Object of C st o in e holds
o is-connected-with a } by Def3;
hence (ObjectDerivation C) . {} = the carrier' of C by A1, A2, TARSKI:1; ::_thesis: verum
end;
theorem Th18: :: CONLAT_1:18
for C being FormalContext holds (AttributeDerivation C) . {} = the carrier of C
proof
let C be FormalContext; ::_thesis: (AttributeDerivation C) . {} = the carrier of C
reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
set O = { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } ;
A1: for x being set st x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } holds
x in the carrier of C
proof
let x be set ; ::_thesis: ( x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } implies x in the carrier of C )
assume x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } ; ::_thesis: x in the carrier of C
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in e holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; ::_thesis: verum
end;
A2: for x being set st x in the carrier of C holds
x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a }
proof
let x be set ; ::_thesis: ( x in the carrier of C implies x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } )
assume x in the carrier of C ; ::_thesis: x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a }
then reconsider x = x as Object of C ;
for a being Attribute of C st a in e holds
x is-connected-with a ;
hence x in { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } ; ::_thesis: verum
end;
(AttributeDerivation C) . e = { o where o is Object of C : for a being Attribute of C st a in e holds
o is-connected-with a } by Def4;
hence (AttributeDerivation C) . {} = the carrier of C by A1, A2, TARSKI:1; ::_thesis: verum
end;
begin
definition
let C be 2-sorted ;
attrc2 is strict ;
struct ConceptStr over C -> ;
aggrConceptStr(# Extent, Intent #) -> ConceptStr over C;
sel Extent c2 -> Subset of the carrier of C;
sel Intent c2 -> Subset of the carrier' of C;
end;
definition
let C be 2-sorted ;
let CP be ConceptStr over C;
attrCP is empty means :Def8: :: CONLAT_1:def 8
( the Extent of CP is empty & the Intent of CP is empty );
attrCP is quasi-empty means :Def9: :: CONLAT_1:def 9
( the Extent of CP is empty or the Intent of CP is empty );
end;
:: deftheorem Def8 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 ) );
:: deftheorem Def9 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 ) );
registration
let C be non quasi-empty 2-sorted ;
cluster strict non empty for ConceptStr over C;
existence
ex b1 being ConceptStr over C st
( b1 is strict & not b1 is empty )
proof
set A = the non empty Subset of the carrier' of C;
set O = the non empty Subset of the carrier of C;
not ConceptStr(# the non empty Subset of the carrier of C, the non empty Subset of the carrier' of C #) is empty by Def8;
hence ex b1 being ConceptStr over C st
( b1 is strict & not b1 is empty ) ; ::_thesis: verum
end;
cluster strict quasi-empty for ConceptStr over C;
existence
ex b1 being ConceptStr over C st
( b1 is strict & b1 is quasi-empty )
proof
reconsider A = {} as Subset of the carrier' of C by XBOOLE_1:2;
reconsider O = {} as Subset of the carrier of C by XBOOLE_1:2;
ConceptStr(# O,A #) is quasi-empty by Def9;
hence ex b1 being ConceptStr over C st
( b1 is strict & b1 is quasi-empty ) ; ::_thesis: verum
end;
end;
registration
let C be empty void 2-sorted ;
cluster -> empty for ConceptStr over C;
coherence
for b1 being ConceptStr over C holds b1 is empty
proof
let CP be ConceptStr over C; ::_thesis: CP is empty
( the Extent of CP is empty & the Intent of CP is empty ) ;
hence CP is empty by Def8; ::_thesis: verum
end;
end;
registration
let C be quasi-empty 2-sorted ;
cluster -> quasi-empty for ConceptStr over C;
coherence
for b1 being ConceptStr over C holds b1 is quasi-empty
proof
let CP be ConceptStr over C; ::_thesis: CP is quasi-empty
( the Extent of CP is empty or the Intent of CP is empty )
proof
set x = the Element of the Extent of CP;
assume not the Extent of CP is empty ; ::_thesis: the Intent of CP is empty
then A1: the Element of the Extent of CP in the Extent of CP ;
thus the Intent of CP is empty ::_thesis: verum
proof
set x = the Element of the Intent of CP;
assume not the Intent of CP is empty ; ::_thesis: contradiction
then the Element of the Intent of CP in the Intent of CP ;
hence contradiction by A1, Def1; ::_thesis: verum
end;
end;
hence CP is quasi-empty by Def9; ::_thesis: verum
end;
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
let C be FormalContext; ::_thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
let CS be ConceptStr over C; ::_thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty )
assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; ::_thesis: not CS is empty
now__::_thesis:_(_(_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_or_(_not_the_Extent_of_CS_is_empty_&_not_CS_is_empty_)_)
percases ( the Extent of CS is empty or not the Extent of CS is empty ) ;
case the Extent of CS is empty ; ::_thesis: not CS is empty
then the Intent of CS = the carrier' of C by A1, Th17;
hence not CS is empty by Def8; ::_thesis: verum
end;
case not the Extent of CS is empty ; ::_thesis: not CS is empty
hence not CS is empty by Def8; ::_thesis: verum
end;
end;
end;
hence not CS is empty ; ::_thesis: verum
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is concept-like means :Def10: :: CONLAT_1:def 10
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP );
end;
:: deftheorem Def10 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 ) );
registration
let C be FormalContext;
cluster non empty concept-like for ConceptStr over C;
existence
ex b1 being ConceptStr over C st
( b1 is concept-like & not b1 is empty )
proof
set o = the Object of C;
set A = (ObjectDerivation C) . { the Object of C};
{ the Object of C} c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { the Object of C} or x in the carrier of C )
assume x in { the Object of C} ; ::_thesis: x in the carrier of C
then x = the Object of C by TARSKI:def_1;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider t = { the Object of C} as Subset of the carrier of C ;
(ObjectDerivation C) . { the Object of C} c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . { the Object of C} or x in the carrier' of C )
assume x in (ObjectDerivation C) . { the Object of C} ; ::_thesis: x in the carrier' of C
then x in { a where a is Attribute of C : for o being Object of C st o in t holds
o is-connected-with a } by Def3;
then ex x9 being Attribute of C st
( x9 = x & ( for o being Object of C st o in t holds
o is-connected-with x9 ) ) ;
hence x in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = (ObjectDerivation C) . { the Object of C} as Subset of the carrier' of C ;
set O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C});
(AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) c= the carrier of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) or x in the carrier of C )
assume x in (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) ; ::_thesis: x in the carrier of C
then x in { o9 where o9 is Object of C : for a being Attribute of C st a in (ObjectDerivation C) . t holds
o9 is-connected-with a } by Def4;
then ex x9 being Object of C st
( x9 = x & ( for a being Attribute of C st a in (ObjectDerivation C) . t holds
x9 is-connected-with a ) ) ;
hence x in the carrier of C ; ::_thesis: verum
end;
then reconsider O = (AttributeDerivation C) . ((ObjectDerivation C) . { the Object of C}) as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
( the Object of C in { the Object of C} & t c= (AttributeDerivation C) . ((ObjectDerivation C) . t) ) by Th5, TARSKI:def_1;
then reconsider M9 = ConceptStr(# O,A #) as non empty ConceptStr over C by Def8;
(ObjectDerivation C) . the Extent of M9 = (ObjectDerivation C) . t by Th7
.= the Intent of M9 ;
then M9 is concept-like by Def10;
hence ex b1 being ConceptStr over C st
( b1 is concept-like & not b1 is empty ) ; ::_thesis: verum
end;
end;
definition
let C be FormalContext;
mode FormalConcept of C is non empty concept-like ConceptStr over C;
end;
registration
let C be FormalContext;
cluster strict non empty concept-like for ConceptStr over C;
existence
ex b1 being FormalConcept of C st b1 is strict
proof
set CP = the FormalConcept of C;
A1: ( (ObjectDerivation C) . the Extent of the FormalConcept of C = the Intent of the FormalConcept of C & (AttributeDerivation C) . the Intent of the FormalConcept of C = the Extent of the FormalConcept of C ) by Def10;
( not the Intent of the FormalConcept of C is empty or not the Extent of the FormalConcept of C is empty ) by Def8;
then ConceptStr(# the Extent of the FormalConcept of C, the Intent of the FormalConcept of C #) is FormalConcept of C by A1, Def8, Def10;
hence ex b1 being FormalConcept of C st b1 is strict ; ::_thesis: verum
end;
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 ) )
proof
let C be FormalContext; ::_thesis: 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 ) )
let O be Subset of the carrier of C; ::_thesis: ( 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 ) )
A1: 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
let O9 be Subset of the carrier of C; ::_thesis: 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
let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & O c= O9 implies (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: O c= O9 ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9
reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2;
A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10
.= O9 ;
A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10
.= A9 ;
(ObjectDerivation C) . O9 c= (ObjectDerivation C) . O by A3, Th3;
hence (AttributeDerivation C) . ((ObjectDerivation C) . O) c= O9 by A4, A5, Th4; ::_thesis: verum
end;
ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C
proof
set M9 = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #);
(ObjectDerivation C) . the Extent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) = the Intent of ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) by Th7;
hence ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . O)),((ObjectDerivation C) . O) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum
end;
hence ( 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 ) ) by A1; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let O be Subset of the carrier of C; ::_thesis: ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O )
A1: now__::_thesis:_(_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_)
O c= (AttributeDerivation C) . ((ObjectDerivation C) . O) by Th5;
then A2: for x being set st x in O holds
x in (AttributeDerivation C) . ((ObjectDerivation C) . O) ;
given A being Subset of the carrier' of C such that A3: ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: (AttributeDerivation C) . ((ObjectDerivation C) . O) = O
(AttributeDerivation C) . ((ObjectDerivation C) . O) c= O by A3, Th19;
then for x being set st x in (AttributeDerivation C) . ((ObjectDerivation C) . O) holds
x in O ;
hence (AttributeDerivation C) . ((ObjectDerivation C) . O) = O by A2, TARSKI:1; ::_thesis: verum
end;
now__::_thesis:_(_(AttributeDerivation_C)_._((ObjectDerivation_C)_._O)_=_O_implies_ex_A_being_Subset_of_the_carrier'_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_)
reconsider A = (ObjectDerivation C) . O as Subset of the carrier' of C ;
set M9 = ConceptStr(# O,A #);
assume (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ; ::_thesis: ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C
then ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1;
hence ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum
end;
hence ( ex A being Subset of the carrier' of C st ConceptStr(# O,A #) is FormalConcept of C iff (AttributeDerivation C) . ((ObjectDerivation C) . O) = O ) by A1; ::_thesis: verum
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 ) )
proof
let C be FormalContext; ::_thesis: 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 ) )
let A be Subset of the carrier' of C; ::_thesis: ( 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 ) )
A1: 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
let O9 be Subset of the carrier of C; ::_thesis: 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
let A9 be Subset of the carrier' of C; ::_thesis: ( ConceptStr(# O9,A9 #) is FormalConcept of C & A c= A9 implies (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 )
assume that
A2: ConceptStr(# O9,A9 #) is FormalConcept of C and
A3: A c= A9 ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9
reconsider M9 = ConceptStr(# O9,A9 #) as FormalConcept of C by A2;
A4: (AttributeDerivation C) . A9 = the Extent of M9 by Def10
.= O9 ;
A5: (ObjectDerivation C) . O9 = the Intent of M9 by Def10
.= A9 ;
(AttributeDerivation C) . A9 c= (AttributeDerivation C) . A by A3, Th4;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) c= A9 by A4, A5, Th3; ::_thesis: verum
end;
ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C
proof
set M9 = ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #);
(AttributeDerivation C) . the Intent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) = the Extent of ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) by Th8;
hence ConceptStr(# ((AttributeDerivation C) . A),((ObjectDerivation C) . ((AttributeDerivation C) . A)) #) is FormalConcept of C by Def10, Lm1; ::_thesis: verum
end;
hence ( 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 ) ) by A1; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let A be Subset of the carrier' of C; ::_thesis: ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A )
A1: now__::_thesis:_(_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_implies_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_)
A c= (ObjectDerivation C) . ((AttributeDerivation C) . A) by Th6;
then A2: for x being set st x in A holds
x in (ObjectDerivation C) . ((AttributeDerivation C) . A) ;
given O being Subset of the carrier of C such that A3: ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: (ObjectDerivation C) . ((AttributeDerivation C) . A) = A
(ObjectDerivation C) . ((AttributeDerivation C) . A) c= A by A3, Th21;
then for x being set st x in (ObjectDerivation C) . ((AttributeDerivation C) . A) holds
x in A ;
hence (ObjectDerivation C) . ((AttributeDerivation C) . A) = A by A2, TARSKI:1; ::_thesis: verum
end;
now__::_thesis:_(_(ObjectDerivation_C)_._((AttributeDerivation_C)_._A)_=_A_implies_ex_O_being_Subset_of_the_carrier_of_C_st_ConceptStr(#_O,A_#)_is_FormalConcept_of_C_)
reconsider O = (AttributeDerivation C) . A as Subset of the carrier of C ;
set M9 = ConceptStr(# O,A #);
assume (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ; ::_thesis: ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C
then ConceptStr(# O,A #) is FormalConcept of C by Def10, Lm1;
hence ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C ; ::_thesis: verum
end;
hence ( ex O being Subset of the carrier of C st ConceptStr(# O,A #) is FormalConcept of C iff (ObjectDerivation C) . ((AttributeDerivation C) . A) = A ) by A1; ::_thesis: verum
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is universal means :Def11: :: CONLAT_1:def 11
the Extent of CP = the carrier of C;
end;
:: deftheorem Def11 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 );
definition
let C be FormalContext;
let CP be ConceptStr over C;
attrCP is co-universal means :Def12: :: CONLAT_1:def 12
the Intent of CP = the carrier' of C;
end;
:: deftheorem Def12 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 );
registration
let C be FormalContext;
cluster strict non empty concept-like universal for ConceptStr over C;
existence
ex b1 being FormalConcept of C st
( b1 is strict & b1 is universal )
proof
reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
reconsider CP = ConceptStr(# ((AttributeDerivation C) . e),((ObjectDerivation C) . ((AttributeDerivation C) . e)) #) as FormalConcept of C by Th21;
(AttributeDerivation C) . {} = the carrier of C by Th18;
then CP is universal by Def11;
hence ex b1 being FormalConcept of C st
( b1 is strict & b1 is universal ) ; ::_thesis: verum
end;
cluster strict non empty concept-like co-universal for ConceptStr over C;
existence
ex b1 being FormalConcept of C st
( b1 is strict & b1 is co-universal )
proof
reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
reconsider CP = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . e)),((ObjectDerivation C) . e) #) as FormalConcept of C by Th19;
(ObjectDerivation C) . {} = the carrier' of C by Th17;
then CP is co-universal by Def12;
hence ex b1 being FormalConcept of C st
( b1 is strict & b1 is co-universal ) ; ::_thesis: verum
end;
end;
definition
let C be FormalContext;
func Concept-with-all-Objects C -> strict universal FormalConcept of C means :Def13: :: 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 b1 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
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) )
proof
reconsider e = {} as Subset of the carrier' of C by XBOOLE_1:2;
reconsider CP = ConceptStr(# ((AttributeDerivation C) . e),((ObjectDerivation C) . ((AttributeDerivation C) . e)) #) as FormalConcept of C by Th21;
(AttributeDerivation C) . {} = the carrier of C by Th18;
then CP is universal by Def11;
hence ex b1 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
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 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
( b1 = 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
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {}) ) holds
b1 = b2 ;
end;
:: deftheorem Def13 defines Concept-with-all-Objects CONLAT_1:def_13_:_
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 carrier of C ex A being Subset of the carrier' 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 :Def14: :: 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 b1 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
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} )
proof
reconsider e = {} as Subset of the carrier of C by XBOOLE_1:2;
reconsider CP = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . e)),((ObjectDerivation C) . e) #) as FormalConcept of C by Th19;
(ObjectDerivation C) . {} = the carrier' of C by Th17;
then CP is co-universal by Def12;
hence ex b1 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
( b1 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 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
( b1 = 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
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) holds
b1 = b2 ;
end;
:: deftheorem Def14 defines Concept-with-all-Attributes CONLAT_1:def_14_:_
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 carrier of C ex A being Subset of the carrier' of C st
( b2 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) );
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 )
proof
let C be FormalContext; ::_thesis: ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C )
( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( Concept-with-all-Objects C = 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
( Concept-with-all-Attributes C = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {}) & A = (ObjectDerivation C) . {} ) ) by Def13, Def14;
hence ( the Extent of (Concept-with-all-Objects C) = the carrier of C & the Intent of (Concept-with-all-Attributes C) = the carrier' of C ) by Th17, Th18; ::_thesis: verum
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 ) )
proof
let C be FormalContext; ::_thesis: for CP being FormalConcept of C holds
( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
let CP be FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) )
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_is_universal_)
assume the Intent of CP = {} ; ::_thesis: CP is universal
then the Extent of CP = the carrier of C by A1, Th18;
hence CP is universal by Def11; ::_thesis: verum
end;
A3: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_is_co-universal_)
assume the Extent of CP = {} ; ::_thesis: CP is co-universal
then the Intent of CP = the carrier' of C by A3, Th17;
hence CP is co-universal by Def12; ::_thesis: verum
end;
hence ( ( the Extent of CP = {} implies CP is co-universal ) & ( the Intent of CP = {} implies CP is universal ) ) by A2; ::_thesis: verum
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 ) )
proof
let C be FormalContext; ::_thesis: 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 ) )
let CP be strict FormalConcept of C; ::_thesis: ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) )
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
A3: now__::_thesis:_(_the_Intent_of_CP_=_{}_implies_CP_=_Concept-with-all-Objects_C_)
assume A4: the Intent of CP = {} ; ::_thesis: CP = Concept-with-all-Objects C
then the Extent of CP = the carrier of C by A1, Th18;
then CP is universal by Def11;
hence CP = Concept-with-all-Objects C by A2, A1, A4, Def13; ::_thesis: verum
end;
now__::_thesis:_(_the_Extent_of_CP_=_{}_implies_CP_=_Concept-with-all-Attributes_C_)
assume A5: the Extent of CP = {} ; ::_thesis: CP = Concept-with-all-Attributes C
then the Intent of CP = the carrier' of C by A2, Th17;
then CP is co-universal by Def12;
hence CP = Concept-with-all-Attributes C by A2, A1, A5, Def14; ::_thesis: verum
end;
hence ( ( the Extent of CP = {} implies CP = Concept-with-all-Attributes C ) & ( the Intent of CP = {} implies CP = Concept-with-all-Objects C ) ) by A3; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: for CP being quasi-empty ConceptStr over C holds
( not CP is FormalConcept of C or CP is universal or CP is co-universal )
let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is FormalConcept of C or CP is universal or CP is co-universal )
assume CP is FormalConcept of C ; ::_thesis: ( CP is universal or CP is co-universal )
then reconsider CP = CP as FormalConcept of C ;
A1: (AttributeDerivation C) . the Intent of CP = the Extent of CP by Def10;
A2: (ObjectDerivation C) . the Extent of CP = the Intent of CP by Def10;
now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_is_universal_)_or_(_the_Extent_of_CP_is_empty_&_CP_is_co-universal_)_)
percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9;
case the Intent of CP is empty ; ::_thesis: CP is universal
then the Extent of CP = the carrier of C by A1, Th18;
hence CP is universal by Def11; ::_thesis: verum
end;
case the Extent of CP is empty ; ::_thesis: CP is co-universal
then the Intent of CP = the carrier' of C by A2, Th17;
hence CP is co-universal by Def12; ::_thesis: verum
end;
end;
end;
hence ( CP is universal or CP is co-universal ) ; ::_thesis: verum
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let CP be quasi-empty ConceptStr over C; ::_thesis: ( not CP is strict FormalConcept of C or CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
assume A1: CP is strict FormalConcept of C ; ::_thesis: ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C )
now__::_thesis:_(_(_the_Intent_of_CP_is_empty_&_CP_=_Concept-with-all-Objects_C_)_or_(_the_Extent_of_CP_is_empty_&_CP_=_Concept-with-all-Attributes_C_)_)
percases ( the Intent of CP is empty or the Extent of CP is empty ) by Def9;
case the Intent of CP is empty ; ::_thesis: CP = Concept-with-all-Objects C
hence CP = Concept-with-all-Objects C by A1, Th25; ::_thesis: verum
end;
case the Extent of CP is empty ; ::_thesis: CP = Concept-with-all-Attributes C
hence CP = Concept-with-all-Attributes C by A1, Th25; ::_thesis: verum
end;
end;
end;
hence ( CP = Concept-with-all-Objects C or CP = Concept-with-all-Attributes C ) ; ::_thesis: verum
end;
definition
let C be FormalContext;
mode Set-of-FormalConcepts of C -> non empty set means :Def15: :: CONLAT_1:def 15
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
set CP = the FormalConcept of C;
for X being set st X in { the FormalConcept of C} holds
X is FormalConcept of C by TARSKI:def_1;
hence ex b1 being non empty set st
for X being set st X in b1 holds
X is FormalConcept of C ; ::_thesis: verum
end;
end;
:: deftheorem Def15 defines Set-of-FormalConcepts CONLAT_1:def_15_:_
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 Def15;
end;
definition
let C be FormalContext;
let CP1, CP2 be FormalConcept of C;
predCP1 is-SubConcept-of CP2 means :Def16: :: CONLAT_1:def 16
the Extent of CP1 c= the Extent of CP2;
end;
:: deftheorem Def16 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 );
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 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 )
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being FormalConcept of C holds
( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
let CP1, CP2 be FormalConcept of C; ::_thesis: ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 )
A1: now__::_thesis:_(_the_Intent_of_CP2_c=_the_Intent_of_CP1_implies_CP1_is-SubConcept-of_CP2_)
assume the Intent of CP2 c= the Intent of CP1 ; ::_thesis: CP1 is-SubConcept-of CP2
then A2: (AttributeDerivation C) . the Intent of CP1 c= (AttributeDerivation C) . the Intent of CP2 by Th4;
( (AttributeDerivation C) . the Intent of CP1 = the Extent of CP1 & (AttributeDerivation C) . the Intent of CP2 = the Extent of CP2 ) by Def10;
hence CP1 is-SubConcept-of CP2 by A2, Def16; ::_thesis: verum
end;
now__::_thesis:_(_CP1_is-SubConcept-of_CP2_implies_the_Intent_of_CP2_c=_the_Intent_of_CP1_)
assume CP1 is-SubConcept-of CP2 ; ::_thesis: the Intent of CP2 c= the Intent of CP1
then A3: the Extent of CP1 c= the Extent of CP2 by Def16;
( (ObjectDerivation C) . the Extent of CP2 = the Intent of CP2 & (ObjectDerivation C) . the Extent of CP1 = the Intent of CP1 ) by Def10;
hence the Intent of CP2 c= the Intent of CP1 by A3, Th3; ::_thesis: verum
end;
hence ( CP1 is-SubConcept-of CP2 iff the Intent of CP2 c= the Intent of CP1 ) by A1; ::_thesis: verum
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;
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 )
proof
let C be FormalContext; ::_thesis: 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 )
let CP be FormalConcept of C; ::_thesis: ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP )
A1: ( the carrier' of C = the Intent of (Concept-with-all-Attributes C) & the Intent of CP c= the carrier' of C ) by Th23;
( the carrier of C = the Extent of (Concept-with-all-Objects C) & the Extent of CP c= the carrier of C ) by Th23;
hence ( CP is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Attributes C is-SubConcept-of CP ) by A1, Def16, Th28; ::_thesis: verum
end;
begin
definition
let C be FormalContext;
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 ) } is non empty set
proof
set M9 = { 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 ) } ;
not { 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 empty
proof
set CP = the FormalConcept of C;
consider O being Subset of the carrier of C such that
A1: O = the Extent of the FormalConcept of C ;
consider A being Subset of the carrier' of C such that
A2: A = the Intent of the FormalConcept of C ;
A3: (AttributeDerivation C) . A = O by A1, A2, Def10;
A4: (ObjectDerivation C) . O = A by A1, A2, Def10;
then not ConceptStr(# O,A #) is empty by Lm1;
then ConceptStr(# O,A #) in { 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 ) } by A4, A3;
hence not { 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 empty ; ::_thesis: verum
end;
then reconsider M9 = { 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 ) } as non empty set ;
for CP being strict non empty ConceptStr over C holds
( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )
proof
let CP be strict non empty ConceptStr over C; ::_thesis: ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) )
now__::_thesis:_(_CP_in_M9_implies_(_(ObjectDerivation_C)_._the_Extent_of_CP_=_the_Intent_of_CP_&_(AttributeDerivation_C)_._the_Intent_of_CP_=_the_Extent_of_CP_)_)
assume CP in M9 ; ::_thesis: ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP )
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ;
hence ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ; ::_thesis: verum
end;
hence ( CP in M9 iff ( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) ) ; ::_thesis: verum
end;
hence { 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 ; ::_thesis: verum
end;
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 ) } ;
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
for X being set st X in B-carrier C holds
X is FormalConcept of C
proof
let X be set ; ::_thesis: ( X in B-carrier C implies X is FormalConcept of C )
assume X in B-carrier C ; ::_thesis: X is FormalConcept of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( X = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ;
hence X is FormalConcept of C by Def10; ::_thesis: verum
end;
hence B-carrier C is Set-of-FormalConcepts of C by Def15; ::_thesis: verum
end;
end;
registration
let C be FormalContext;
cluster B-carrier C -> non empty ;
coherence
not B-carrier C is empty ;
end;
theorem Th31: :: CONLAT_1:31
for C being FormalContext
for CP being set holds
( CP in B-carrier C iff CP is strict FormalConcept of C )
proof
let C be FormalContext; ::_thesis: for CP being set holds
( CP in B-carrier C iff CP is strict FormalConcept of C )
let CP be set ; ::_thesis: ( CP in B-carrier C iff CP is strict FormalConcept of C )
A1: ( CP is strict FormalConcept of C implies CP in B-carrier C )
proof
assume A2: CP is strict FormalConcept of C ; ::_thesis: CP in B-carrier C
then reconsider CP = CP as FormalConcept of C ;
set I9 = the Intent of CP;
set E9 = the Extent of CP;
( (ObjectDerivation C) . the Extent of CP = the Intent of CP & (AttributeDerivation C) . the Intent of CP = the Extent of CP ) by Def10;
hence CP in B-carrier C by A2; ::_thesis: verum
end;
( CP in B-carrier C implies CP is strict FormalConcept of C )
proof
assume CP in B-carrier C ; ::_thesis: CP is strict FormalConcept of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( CP = ConceptStr(# E,I #) & not ConceptStr(# E,I #) is empty & (ObjectDerivation C) . E = I & (AttributeDerivation C) . I = E ) ;
hence CP is strict FormalConcept of C by Def10; ::_thesis: verum
end;
hence ( CP in B-carrier C iff CP is strict FormalConcept of C ) by A1; ::_thesis: verum
end;
definition
let C be FormalContext;
func B-meet C -> BinOp of (B-carrier C) means :Def18: :: 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
ex b1 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
( 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
defpred S1[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $3 = ConceptStr(# O,A #) & O = the Extent of $1 /\ the Extent of $2 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of $1 \/ the Intent of $2)) );
A1: for CP1, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
proof
let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
set O = the Extent of CP1 /\ the Extent of CP2;
set A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2));
reconsider A9 = the Intent of CP1 \/ the Intent of CP2 as Subset of the carrier' of C ;
set CP = ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #);
A2: (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) = (AttributeDerivation C) . A9 by Th8
.= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2) by Th16
.= the Extent of CP1 /\ ((AttributeDerivation C) . the Intent of CP2) by Def10
.= the Extent of CP1 /\ the Extent of CP2 by Def10 ;
then A3: (ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2) = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) by Th7;
then not ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) is empty by Lm1;
then ConceptStr(# ( the Extent of CP1 /\ the Extent of CP2),((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) #) in { 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 ) } by A2, A3;
hence ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum
end;
consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A4: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take f ; ::_thesis: 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
( f . (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
( f . (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
let CP1, CP2 be strict FormalConcept of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (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)) )
( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31;
hence ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (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)) ) by A4; ::_thesis: verum
end;
hence 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
( f . (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)) ) ; ::_thesis: verum
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 carrier of C ex A being Subset of the carrier' 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 carrier of C ex A being Subset of the carrier' 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
let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( 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
( F1 . (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
( F2 . (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)) ) ) implies F1 = F2 )
assume A5: 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
( F1 . (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)) ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = the Extent of CP1 /\ the Extent of CP2 or not A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) ) or F1 = F2 )
assume A6: 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
( F2 . (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)) ) ; ::_thesis: F1 = F2
A7: for X being set st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X
proof
let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X
then consider A, B being set such that
A8: A in B-carrier C and
A9: B in B-carrier C and
A10: X = [A,B] by ZFMISC_1:def_2;
reconsider B = B as strict FormalConcept of C by A9, Th31;
reconsider A = A as strict FormalConcept of C by A8, Th31;
( ex O being Subset of the carrier of C ex At being Subset of the carrier' of C st
( F1 . (A,B) = ConceptStr(# O,At #) & O = the Extent of A /\ the Extent of B & At = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of A \/ the Intent of B)) ) & ex O9 being Subset of the carrier of C ex At9 being Subset of the carrier' of C st
( F2 . (A,B) = ConceptStr(# O9,At9 #) & O9 = the Extent of A /\ the Extent of B & At9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of A \/ the Intent of B)) ) ) by A5, A6;
hence F1 . X = F2 . X by A10; ::_thesis: verum
end;
( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1;
hence F1 = F2 by A7, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines B-meet CONLAT_1:def_18_:_
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 carrier of C ex A being Subset of the carrier' 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 :Def19: :: 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
ex b1 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
( 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
defpred S1[ FormalConcept of C, FormalConcept of C, set ] means ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( $3 = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of $1 \/ the Extent of $2)) & A = the Intent of $1 /\ the Intent of $2 );
A1: for CP1, CP2 being Element of B-carrier C ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
proof
let CP1, CP2 be Element of B-carrier C; ::_thesis: ex CP being Element of B-carrier C st S1[CP1,CP2,CP]
set O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2));
set A = the Intent of CP1 /\ the Intent of CP2;
reconsider O9 = the Extent of CP1 \/ the Extent of CP2 as Subset of the carrier of C ;
set CP = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #);
A2: (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) = (ObjectDerivation C) . O9 by Th7
.= ((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2) by Th15
.= the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2) by Def10
.= the Intent of CP1 /\ the Intent of CP2 by Def10 ;
then ( (AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2) = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) & not ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) is empty ) by Lm1, Th7;
then ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))),( the Intent of CP1 /\ the Intent of CP2) #) in { 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 ) } by A2;
hence ex CP being Element of B-carrier C st S1[CP1,CP2,CP] ; ::_thesis: verum
end;
consider f being Function of [:(B-carrier C),(B-carrier C):],(B-carrier C) such that
A3: for CP1, CP2 being Element of B-carrier C holds S1[CP1,CP2,f . (CP1,CP2)] from BINOP_1:sch_3(A1);
reconsider f = f as BinOp of (B-carrier C) ;
take f ; ::_thesis: 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
( f . (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
( f . (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
let CP1, CP2 be strict FormalConcept of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (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 )
( CP1 is Element of B-carrier C & CP2 is Element of B-carrier C ) by Th31;
hence ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . (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 ) by A3; ::_thesis: verum
end;
hence 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
( f . (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 ) ; ::_thesis: verum
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 carrier of C ex A being Subset of the carrier' 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 carrier of C ex A being Subset of the carrier' 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
let F1, F2 be BinOp of (B-carrier C); ::_thesis: ( ( 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
( F1 . (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
( F2 . (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 ) ) implies F1 = F2 )
assume A4: 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
( F1 . (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 ) ; ::_thesis: ( ex CP1, CP2 being strict FormalConcept of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . (CP1,CP2) = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) or not A = the Intent of CP1 /\ the Intent of CP2 ) or F1 = F2 )
assume A5: 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
( F2 . (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 ) ; ::_thesis: F1 = F2
A6: for X being set st X in [:(B-carrier C),(B-carrier C):] holds
F1 . X = F2 . X
proof
let X be set ; ::_thesis: ( X in [:(B-carrier C),(B-carrier C):] implies F1 . X = F2 . X )
assume X in [:(B-carrier C),(B-carrier C):] ; ::_thesis: F1 . X = F2 . X
then consider A, B being set such that
A7: A in B-carrier C and
A8: B in B-carrier C and
A9: X = [A,B] by ZFMISC_1:def_2;
reconsider B = B as strict FormalConcept of C by A8, Th31;
reconsider A = A as strict FormalConcept of C by A7, Th31;
( ex O being Subset of the carrier of C ex At being Subset of the carrier' of C st
( F1 . (A,B) = ConceptStr(# O,At #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of A \/ the Extent of B)) & At = the Intent of A /\ the Intent of B ) & ex O9 being Subset of the carrier of C ex At9 being Subset of the carrier' of C st
( F2 . (A,B) = ConceptStr(# O9,At9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of A \/ the Extent of B)) & At9 = the Intent of A /\ the Intent of B ) ) by A4, A5;
hence F1 . X = F2 . X by A9; ::_thesis: verum
end;
( dom F1 = [:(B-carrier C),(B-carrier C):] & dom F2 = [:(B-carrier C),(B-carrier C):] ) by FUNCT_2:def_1;
hence F1 = F2 by A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def19 defines B-join CONLAT_1:def_19_:_
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 carrier of C ex A being Subset of the carrier' 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
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) in rng (B-meet C)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) in rng (B-meet C)
( CP1 in B-carrier C & CP2 in B-carrier C ) by Th31;
then [CP1,CP2] in [:(B-carrier C),(B-carrier C):] by ZFMISC_1:def_2;
then [CP1,CP2] in dom (B-meet C) by FUNCT_2:def_1;
hence (B-meet C) . (CP1,CP2) in rng (B-meet C) by FUNCT_1:def_3; ::_thesis: verum
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
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) in rng (B-join C)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) in rng (B-join C)
( CP1 in B-carrier C & CP2 in B-carrier C ) by Th31;
then [CP1,CP2] in [:(B-carrier C),(B-carrier C):] by ZFMISC_1:def_2;
then [CP1,CP2] in dom (B-join C) by FUNCT_2:def_1;
hence (B-join C) . (CP1,CP2) in rng (B-join C) by FUNCT_1:def_3; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1)
( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-meet C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-meet C) . (CP2,CP1) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP2 /\ the Extent of CP1 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP1)) ) ) by Def18;
hence (B-meet C) . (CP1,CP2) = (B-meet C) . (CP2,CP1) ; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1)
( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP2,CP1) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP1)) & A9 = the Intent of CP2 /\ the Intent of CP1 ) ) by Def19;
hence (B-join C) . (CP1,CP2) = (B-join C) . (CP2,CP1) ; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: 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)
let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3)
(B-meet C) . (CP1,CP2) in rng (B-meet C) by Lm2;
then reconsider CP = (B-meet C) . (CP1,CP2) as strict FormalConcept of C by Th31;
A1: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-meet C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-meet C) . (CP,CP3) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP /\ the Extent of CP3 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of CP3)) ) ) by Def18;
(B-meet C) . (CP2,CP3) in rng (B-meet C) by Lm2;
then reconsider CP9 = (B-meet C) . (CP2,CP3) as strict FormalConcept of C by Th31;
A2: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-meet C) . (CP2,CP3) = ConceptStr(# O,A #) & O = the Extent of CP2 /\ the Extent of CP3 & A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3)) ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-meet C) . (CP1,CP9) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP1 /\ the Extent of CP9 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP9)) ) ) by Def18;
(ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3))))) = (ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3))))) by Th16
.= (ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP2 \/ the Intent of CP3))) by Th8
.= (ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ (((AttributeDerivation C) . the Intent of CP2) /\ ((AttributeDerivation C) . the Intent of CP3))) by Th16
.= (ObjectDerivation C) . ((((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2)) /\ ((AttributeDerivation C) . the Intent of CP3)) by XBOOLE_1:16
.= (ObjectDerivation C) . (((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)) /\ ((AttributeDerivation C) . the Intent of CP3)) by Th16
.= (ObjectDerivation C) . (((AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2)))) /\ ((AttributeDerivation C) . the Intent of CP3)) by Th8
.= (ObjectDerivation C) . ((AttributeDerivation C) . (((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) \/ the Intent of CP3)) by Th16 ;
hence (B-meet C) . (CP1,((B-meet C) . (CP2,CP3))) = (B-meet C) . (((B-meet C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum
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)
proof
let C be FormalContext; ::_thesis: 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)
let CP1, CP2, CP3 be strict FormalConcept of C; ::_thesis: (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3)
(B-join C) . (CP1,CP2) in rng (B-join C) by Lm3;
then reconsider CP = (B-join C) . (CP1,CP2) as strict FormalConcept of C by Th31;
A1: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP,CP3) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ the Extent of CP3)) & A9 = the Intent of CP /\ the Intent of CP3 ) ) by Def19;
(B-join C) . (CP2,CP3) in rng (B-join C) by Lm3;
then reconsider CP9 = (B-join C) . (CP2,CP3) as strict FormalConcept of C by Th31;
A2: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (CP2,CP3) = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3)) & A = the Intent of CP2 /\ the Intent of CP3 ) & ex O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP1,CP9) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP9)) & A9 = the Intent of CP1 /\ the Intent of CP9 ) ) by Def19;
(AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))))) = (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))))) by Th15
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . ( the Extent of CP2 \/ the Extent of CP3))) by Th7
.= (AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ (((ObjectDerivation C) . the Extent of CP2) /\ ((ObjectDerivation C) . the Extent of CP3))) by Th15
.= (AttributeDerivation C) . ((((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by XBOOLE_1:16
.= (AttributeDerivation C) . (((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th15
.= (AttributeDerivation C) . (((ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2)))) /\ ((ObjectDerivation C) . the Extent of CP3)) by Th7
.= (AttributeDerivation C) . ((ObjectDerivation C) . (((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) \/ the Extent of CP3)) by Th15 ;
hence (B-join C) . (CP1,((B-join C) . (CP2,CP3))) = (B-join C) . (((B-join C) . (CP1,CP2)),CP3) by A1, A2, XBOOLE_1:16; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2
A1: the Extent of CP1 /\ the Extent of CP2 c= the Extent of CP2 by XBOOLE_1:17;
(B-meet C) . (CP1,CP2) in rng (B-meet C) by Lm2;
then reconsider CP9 = (B-meet C) . (CP1,CP2) as strict FormalConcept of C by Th31;
A2: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-meet C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-join C) . (CP9,CP2) = ConceptStr(# O9,A9 #) & O9 = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP9 \/ the Extent of CP2)) & A9 = the Intent of CP9 /\ the Intent of CP2 ) ) by Def18, Def19;
(AttributeDerivation C) . ((ObjectDerivation C) . (( the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2)) = (AttributeDerivation C) . (((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2)) by Th15;
then A3: (AttributeDerivation C) . ((ObjectDerivation C) . (( the Extent of CP1 /\ the Extent of CP2) \/ the Extent of CP2)) = (AttributeDerivation C) . ((ObjectDerivation C) . the Extent of CP2) by A1, Th3, XBOOLE_1:28
.= (AttributeDerivation C) . the Intent of CP2 by Def10
.= the Extent of CP2 by Def10 ;
((ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP2))) /\ the Intent of CP2 = ((ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2 by Th16
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ ((AttributeDerivation C) . the Intent of CP2))) /\ the Intent of CP2 by Def10
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ the Intent of CP2 by Def10
.= ((ObjectDerivation C) . ( the Extent of CP1 /\ the Extent of CP2)) /\ ((ObjectDerivation C) . the Extent of CP2) by Def10
.= (ObjectDerivation C) . the Extent of CP2 by A1, Th3, XBOOLE_1:28
.= the Intent of CP2 by Def10 ;
hence (B-join C) . (((B-meet C) . (CP1,CP2)),CP2) = CP2 by A2, A3; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being strict FormalConcept of C holds (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1
let CP1, CP2 be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1
A1: the Intent of CP1 /\ the Intent of CP2 c= the Intent of CP1 by XBOOLE_1:17;
(B-join C) . (CP1,CP2) in rng (B-join C) by Lm3;
then reconsider CP9 = (B-join C) . (CP1,CP2) as strict FormalConcept of C by Th31;
A2: ( ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . (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 O9 being Subset of the carrier of C ex A9 being Subset of the carrier' of C st
( (B-meet C) . (CP1,CP9) = ConceptStr(# O9,A9 #) & O9 = the Extent of CP1 /\ the Extent of CP9 & A9 = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ the Intent of CP9)) ) ) by Def18, Def19;
(ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ ( the Intent of CP1 /\ the Intent of CP2))) = (ObjectDerivation C) . (((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2))) by Th16;
then A3: (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP1 \/ ( the Intent of CP1 /\ the Intent of CP2))) = (ObjectDerivation C) . ((AttributeDerivation C) . the Intent of CP1) by A1, Th4, XBOOLE_1:28
.= (ObjectDerivation C) . the Extent of CP1 by Def10
.= the Intent of CP1 by Def10 ;
the Extent of CP1 /\ ((AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP1 \/ the Extent of CP2))) = the Extent of CP1 /\ ((AttributeDerivation C) . (((ObjectDerivation C) . the Extent of CP1) /\ ((ObjectDerivation C) . the Extent of CP2))) by Th15
.= the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ ((ObjectDerivation C) . the Extent of CP2))) by Def10
.= the Extent of CP1 /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10
.= ((AttributeDerivation C) . the Intent of CP1) /\ ((AttributeDerivation C) . ( the Intent of CP1 /\ the Intent of CP2)) by Def10
.= (AttributeDerivation C) . the Intent of CP1 by A1, Th4, XBOOLE_1:28
.= the Extent of CP1 by Def10 ;
hence (B-meet C) . (CP1,((B-join C) . (CP1,CP2))) = CP1 by A2, A3; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-meet C) . (CP,(Concept-with-all-Objects C)) = ConceptStr(# O,A #) and
A2: O = the Extent of CP /\ the Extent of (Concept-with-all-Objects C) and
A3: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Objects C))) by Def18;
A4: O = the Extent of CP /\ the carrier of C by A2, Th23
.= the Extent of CP by XBOOLE_1:28 ;
the carrier of C c= the carrier of C ;
then reconsider O9 = the carrier of C as Subset of the carrier of C ;
A5: ((ObjectDerivation C) . the Extent of CP) \/ ((ObjectDerivation C) . O9) = (ObjectDerivation C) . the Extent of CP by Th3, XBOOLE_1:12;
A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)))) by A3, Def10
.= (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ ((ObjectDerivation C) . the carrier of C))) by Th23
.= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . the Extent of CP)) by A5, Def10
.= (ObjectDerivation C) . the Extent of CP by Th7
.= the Intent of CP by Def10 ;
hence (B-meet C) . (CP,(Concept-with-all-Objects C)) = CP by A1, A4; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C
let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-join C) . (CP,(Concept-with-all-Objects C)) = ConceptStr(# O,A #) and
A2: O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ the Extent of (Concept-with-all-Objects C))) and
A3: A = the Intent of CP /\ the Intent of (Concept-with-all-Objects C) by Def19;
A4: O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ the carrier of C)) by A2, Th23
.= (AttributeDerivation C) . ((ObjectDerivation C) . the carrier of C) by XBOOLE_1:12
.= (AttributeDerivation C) . ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)) by Th23
.= (AttributeDerivation C) . the Intent of (Concept-with-all-Objects C) by Def10
.= the Extent of (Concept-with-all-Objects C) by Def10 ;
A = ((ObjectDerivation C) . the Extent of CP) /\ the Intent of (Concept-with-all-Objects C) by A3, Def10
.= ((ObjectDerivation C) . the Extent of CP) /\ ((ObjectDerivation C) . the Extent of (Concept-with-all-Objects C)) by Def10
.= (ObjectDerivation C) . ( the Extent of CP \/ the Extent of (Concept-with-all-Objects C)) by Th15
.= (ObjectDerivation C) . ( the Extent of CP \/ the carrier of C) by Th23
.= (ObjectDerivation C) . the carrier of C by XBOOLE_1:12
.= (ObjectDerivation C) . the Extent of (Concept-with-all-Objects C) by Th23
.= the Intent of (Concept-with-all-Objects C) by Def10 ;
hence (B-join C) . (CP,(Concept-with-all-Objects C)) = Concept-with-all-Objects C by A1, A4; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP
let CP be strict FormalConcept of C; ::_thesis: (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-join C) . (CP,(Concept-with-all-Attributes C)) = ConceptStr(# O,A #) and
A2: O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ the Extent of (Concept-with-all-Attributes C))) and
A3: A = the Intent of CP /\ the Intent of (Concept-with-all-Attributes C) by Def19;
A4: A = the Intent of CP /\ the carrier' of C by A3, Th23
.= the Intent of CP by XBOOLE_1:28 ;
the carrier' of C c= the carrier' of C ;
then reconsider A9 = the carrier' of C as Subset of the carrier' of C ;
A5: ((AttributeDerivation C) . the Intent of CP) \/ ((AttributeDerivation C) . A9) = (AttributeDerivation C) . the Intent of CP by Th4, XBOOLE_1:12;
O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)))) by A2, Def10
.= (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of CP \/ ((AttributeDerivation C) . the carrier' of C))) by Th23
.= (AttributeDerivation C) . ((ObjectDerivation C) . ((AttributeDerivation C) . the Intent of CP)) by A5, Def10
.= (AttributeDerivation C) . the Intent of CP by Th8
.= the Extent of CP by Def10 ;
hence (B-join C) . (CP,(Concept-with-all-Attributes C)) = CP by A1, A4; ::_thesis: verum
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
proof
let C be FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C
let CP be strict FormalConcept of C; ::_thesis: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A1: (B-meet C) . (CP,(Concept-with-all-Attributes C)) = ConceptStr(# O,A #) and
A2: O = the Extent of CP /\ the Extent of (Concept-with-all-Attributes C) and
A3: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Attributes C))) by Def18;
A4: A = (ObjectDerivation C) . ((AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C)) by A3, Th23
.= (ObjectDerivation C) . ((AttributeDerivation C) . the carrier' of C) by XBOOLE_1:12
.= (ObjectDerivation C) . ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Th23
.= (ObjectDerivation C) . the Extent of (Concept-with-all-Attributes C) by Def10
.= the Intent of (Concept-with-all-Attributes C) by Def10 ;
O = ((AttributeDerivation C) . the Intent of CP) /\ the Extent of (Concept-with-all-Attributes C) by A2, Def10
.= ((AttributeDerivation C) . the Intent of CP) /\ ((AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C)) by Def10
.= (AttributeDerivation C) . ( the Intent of CP \/ the Intent of (Concept-with-all-Attributes C)) by Th16
.= (AttributeDerivation C) . ( the Intent of CP \/ the carrier' of C) by Th23
.= (AttributeDerivation C) . the carrier' of C by XBOOLE_1:12
.= (AttributeDerivation C) . the Intent of (Concept-with-all-Attributes C) by Th23
.= the Extent of (Concept-with-all-Attributes C) by Def10 ;
hence (B-meet C) . (CP,(Concept-with-all-Attributes C)) = Concept-with-all-Attributes C by A1, A4; ::_thesis: verum
end;
definition
let C be FormalContext;
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) #) is non empty strict LattStr ;
end;
:: deftheorem defines ConceptLattice CONLAT_1:def_20_:_
for C being FormalContext holds ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
theorem Th42: :: CONLAT_1:42
for C being FormalContext holds ConceptLattice C is Lattice
proof
let C be FormalContext; ::_thesis: ConceptLattice C is Lattice
set L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #);
reconsider L = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) as non empty strict LattStr ;
A1: for a, b, c being Element of L holds a "\/" (b "\/" c) = (a "\/" b) "\/" c
proof
let a, b, c be Element of L; ::_thesis: a "\/" (b "\/" c) = (a "\/" b) "\/" c
reconsider b = b, c = c as Element of B-carrier C ;
reconsider d = (B-join C) . (b,c) as Element of L ;
reconsider b = b, c = c as Element of L ;
reconsider a = a, b = b as Element of B-carrier C ;
reconsider e = (B-join C) . (a,b) as Element of L ;
reconsider a = a, b = b as Element of L ;
A2: a "\/" (b "\/" c) = a "\/" d by LATTICES:def_1
.= (B-join C) . (a,((B-join C) . (b,c))) by LATTICES:def_1 ;
A3: (a "\/" b) "\/" c = e "\/" c by LATTICES:def_1
.= (B-join C) . (((B-join C) . (a,b)),c) by LATTICES:def_1 ;
reconsider a = a, b = b, c = c as strict FormalConcept of C by Th31;
(B-join C) . (a,((B-join C) . (b,c))) = (B-join C) . (((B-join C) . (a,b)),c) by Th35;
hence a "\/" (b "\/" c) = (a "\/" b) "\/" c by A2, A3; ::_thesis: verum
end;
A4: for a, b being Element of L holds (a "/\" b) "\/" b = b
proof
let a, b be Element of L; ::_thesis: (a "/\" b) "\/" b = b
reconsider a = a, b = b as Element of B-carrier C ;
reconsider d = (B-meet C) . (a,b) as Element of L ;
reconsider a = a, b = b as Element of L ;
A5: (a "/\" b) "\/" b = d "\/" b by LATTICES:def_2
.= (B-join C) . (((B-meet C) . (a,b)),b) by LATTICES:def_1 ;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
(B-join C) . (((B-meet C) . (a,b)),b) = b by Th36;
hence (a "/\" b) "\/" b = b by A5; ::_thesis: verum
end;
A6: for a, b, c being Element of L holds a "/\" (b "/\" c) = (a "/\" b) "/\" c
proof
let a, b, c be Element of L; ::_thesis: a "/\" (b "/\" c) = (a "/\" b) "/\" c
reconsider b = b, c = c as Element of B-carrier C ;
reconsider d = (B-meet C) . (b,c) as Element of L ;
reconsider b = b, c = c as Element of L ;
A7: a "/\" (b "/\" c) = a "/\" d by LATTICES:def_2
.= (B-meet C) . (a,((B-meet C) . (b,c))) by LATTICES:def_2 ;
reconsider a = a, b = b as Element of B-carrier C ;
reconsider e = (B-meet C) . (a,b) as Element of L ;
reconsider a = a, b = b as Element of L ;
A8: (a "/\" b) "/\" c = e "/\" c by LATTICES:def_2
.= (B-meet C) . (((B-meet C) . (a,b)),c) by LATTICES:def_2 ;
reconsider a = a, b = b, c = c as strict FormalConcept of C by Th31;
(B-meet C) . (a,((B-meet C) . (b,c))) = (B-meet C) . (((B-meet C) . (a,b)),c) by Th34;
hence a "/\" (b "/\" c) = (a "/\" b) "/\" c by A7, A8; ::_thesis: verum
end;
A9: for a, b being Element of L holds a "/\" b = b "/\" a
proof
let a, b be Element of L; ::_thesis: a "/\" b = b "/\" a
A10: b "/\" a = (B-meet C) . (b,a) by LATTICES:def_2;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
(B-meet C) . (a,b) = (B-meet C) . (b,a) by Th32;
hence a "/\" b = b "/\" a by A10, LATTICES:def_2; ::_thesis: verum
end;
A11: for a, b being Element of L holds a "/\" (a "\/" b) = a
proof
let a, b be Element of L; ::_thesis: a "/\" (a "\/" b) = a
reconsider a = a, b = b as Element of B-carrier C ;
reconsider d = (B-join C) . (a,b) as Element of L ;
reconsider a = a, b = b as Element of L ;
A12: a "/\" (a "\/" b) = a "/\" d by LATTICES:def_1
.= (B-meet C) . (a,((B-join C) . (a,b))) by LATTICES:def_2 ;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
(B-meet C) . (a,((B-join C) . (a,b))) = a by Th37;
hence a "/\" (a "\/" b) = a by A12; ::_thesis: verum
end;
for a, b being Element of L holds a "\/" b = b "\/" a
proof
let a, b be Element of L; ::_thesis: a "\/" b = b "\/" a
A13: b "\/" a = (B-join C) . (b,a) by LATTICES:def_1;
reconsider a = a, b = b as strict FormalConcept of C by Th31;
(B-join C) . (a,b) = (B-join C) . (b,a) by Th33;
hence a "\/" b = b "\/" a by A13, LATTICES:def_1; ::_thesis: verum
end;
then ( L is join-commutative & L is join-associative & L is meet-absorbing & L is meet-commutative & L is meet-associative & L is join-absorbing ) by A1, A4, A9, A6, A11, LATTICES:def_4, LATTICES:def_5, LATTICES:def_6, LATTICES:def_7, LATTICES:def_8, LATTICES:def_9;
hence ConceptLattice C is Lattice ; ::_thesis: verum
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 Th42;
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
let s be Element of S; ::_thesis: s is FormalConcept of C
s is Element of B-carrier C ;
hence s is FormalConcept of C ; ::_thesis: verum
end;
end;
definition
let C be FormalContext;
let CP be Element of (ConceptLattice C);
funcCP @ -> strict FormalConcept of C equals :: CONLAT_1:def 21
CP;
coherence
CP is strict FormalConcept of C by Th31;
end;
:: deftheorem defines @ CONLAT_1:def_21_:_
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 @ )
proof
let C be FormalContext; ::_thesis: for CP1, CP2 being Element of (ConceptLattice C) holds
( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
let CP1, CP2 be Element of (ConceptLattice C); ::_thesis: ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ )
set CL = ConceptLattice C;
A1: now__::_thesis:_(_CP1_@_is-SubConcept-of_CP2_@_implies_CP1_[=_CP2_)
assume A2: CP1 @ is-SubConcept-of CP2 @ ; ::_thesis: CP1 [= CP2
then the Intent of (CP2 @) c= the Intent of (CP1 @) by Th28;
then A3: the Intent of (CP1 @) /\ the Intent of (CP2 @) = the Intent of (CP2 @) by XBOOLE_1:28;
consider O being Subset of the carrier of C, A being Subset of the carrier' of C such that
A4: (B-join C) . ((CP1 @),(CP2 @)) = ConceptStr(# O,A #) and
A5: O = (AttributeDerivation C) . ((ObjectDerivation C) . ( the Extent of (CP1 @) \/ the Extent of (CP2 @))) and
A6: A = the Intent of (CP1 @) /\ the Intent of (CP2 @) by Def19;
the Extent of (CP1 @) c= the Extent of (CP2 @) by A2, Def16;
then the Extent of (CP1 @) \/ the Extent of (CP2 @) = the Extent of (CP2 @) by XBOOLE_1:12;
then O = (AttributeDerivation C) . the Intent of (CP2 @) by A5, Def10
.= the Extent of (CP2 @) by Def10 ;
then CP1 "\/" CP2 = CP2 by A3, A4, A6, LATTICES:def_1;
hence CP1 [= CP2 by LATTICES:def_3; ::_thesis: verum
end;
now__::_thesis:_(_CP1_[=_CP2_implies_CP1_@_is-SubConcept-of_CP2_@_)
assume CP1 [= CP2 ; ::_thesis: CP1 @ is-SubConcept-of CP2 @
then CP1 "\/" CP2 = CP2 by LATTICES:def_3;
then A7: the L_join of (ConceptLattice C) . (CP1,CP2) = CP2 by LATTICES:def_1;
ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( (B-join C) . ((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 @) ) by Def19;
then for x being set st x in the Intent of (CP2 @) holds
x in the Intent of (CP1 @) by A7, XBOOLE_0:def_4;
then the Intent of (CP2 @) c= the Intent of (CP1 @) by TARSKI:def_3;
hence CP1 @ is-SubConcept-of CP2 @ by Th28; ::_thesis: verum
end;
hence ( CP1 [= CP2 iff CP1 @ is-SubConcept-of CP2 @ ) by A1; ::_thesis: verum
end;
theorem Th44: :: CONLAT_1:44
for C being FormalContext holds ConceptLattice C is complete Lattice
proof
let C be FormalContext; ::_thesis: ConceptLattice C is complete Lattice
for X being Subset of (ConceptLattice C) ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )
proof
let X be Subset of (ConceptLattice C); ::_thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )
percases ( X = {} or X <> {} ) ;
supposeA1: X = {} ; ::_thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )
A2: for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= Top (ConceptLattice C)
proof
let b be Element of (ConceptLattice C); ::_thesis: ( b is_less_than X implies b [= Top (ConceptLattice C) )
assume b is_less_than X ; ::_thesis: b [= Top (ConceptLattice C)
ex c being Element of (ConceptLattice C) st
for a being Element of (ConceptLattice C) holds
( c "\/" a = c & a "\/" c = c )
proof
reconsider CO = Concept-with-all-Objects C as Element of (ConceptLattice C) by Th31;
for CP being Element of (ConceptLattice C) holds
( CO "\/" CP = CO & CP "\/" CO = CO )
proof
let CP be Element of (ConceptLattice C); ::_thesis: ( CO "\/" CP = CO & CP "\/" CO = CO )
reconsider CP = CP as strict FormalConcept of C by Th31;
reconsider CO = CO as strict FormalConcept of C ;
(B-join C) . (CO,CP) = (B-join C) . (CP,CO) by Th33
.= CO by Th39 ;
hence ( CO "\/" CP = CO & CP "\/" CO = CO ) by LATTICES:def_1; ::_thesis: verum
end;
hence ex c being Element of (ConceptLattice C) st
for a being Element of (ConceptLattice C) holds
( c "\/" a = c & a "\/" c = c ) ; ::_thesis: verum
end;
then ConceptLattice C is upper-bounded by LATTICES:def_14;
then (Top (ConceptLattice C)) "\/" b = Top (ConceptLattice C) ;
hence b [= Top (ConceptLattice C) by LATTICES:def_3; ::_thesis: verum
end;
for q being Element of (ConceptLattice C) st q in X holds
Top (ConceptLattice C) [= q by A1;
then Top (ConceptLattice C) is_less_than X by LATTICE3:def_16;
hence ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) ) by A2; ::_thesis: verum
end;
suppose X <> {} ; ::_thesis: ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) )
then reconsider X = X as non empty Subset of (ConceptLattice C) ;
set ExX = { the Extent of x where x is Element of B-carrier C : x in X } ;
A3: for x being Element of X holds the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X }
proof
let x be Element of X; ::_thesis: the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X }
x in X ;
then reconsider x = x as Element of B-carrier C ;
the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ;
hence the Extent of x in { the Extent of x where x is Element of B-carrier C : x in X } ; ::_thesis: verum
end;
then reconsider ExX = { the Extent of x where x is Element of B-carrier C : x in X } as non empty set ;
set E1 = meet ExX;
A4: for o being Object of C holds
( o in meet ExX iff for x being Element of X holds o in the Extent of x )
proof
let o be Object of C; ::_thesis: ( o in meet ExX iff for x being Element of X holds o in the Extent of x )
A5: ( ( for x being Element of X holds o in the Extent of x ) implies o in meet ExX )
proof
assume A6: for x being Element of X holds o in the Extent of x ; ::_thesis: o in meet ExX
for Y being set st Y in ExX holds
o in Y
proof
let Y be set ; ::_thesis: ( Y in ExX implies o in Y )
assume Y in ExX ; ::_thesis: o in Y
then ex Y9 being Element of B-carrier C st
( Y = the Extent of Y9 & Y9 in X ) ;
hence o in Y by A6; ::_thesis: verum
end;
hence o in meet ExX by SETFAM_1:def_1; ::_thesis: verum
end;
( o in meet ExX implies for x being Element of X holds o in the Extent of x )
proof
assume A7: o in meet ExX ; ::_thesis: for x being Element of X holds o in the Extent of x
let x be Element of X; ::_thesis: o in the Extent of x
the Extent of x in ExX by A3;
hence o in the Extent of x by A7, SETFAM_1:def_1; ::_thesis: verum
end;
hence ( o in meet ExX iff for x being Element of X holds o in the Extent of x ) by A5; ::_thesis: verum
end;
meet ExX c= the carrier of C
proof
set Y = the Element of ExX;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet ExX or x in the carrier of C )
the Element of ExX in ExX ;
then consider Y9 being Element of B-carrier C such that
A8: the Element of ExX = the Extent of Y9 and
Y9 in X ;
assume x in meet ExX ; ::_thesis: x in the carrier of C
then x in the Extent of Y9 by A8, SETFAM_1:def_1;
hence x in the carrier of C ; ::_thesis: verum
end;
then consider O being Subset of the carrier of C such that
A9: for o being Object of C holds
( o in O iff for x being Element of X holds o in the Extent of x ) by A4;
set InX = { the Intent of x where x is Element of B-carrier C : x in X } ;
set In = union { the Intent of x where x is Element of B-carrier C : x in X } ;
A10: for a being Attribute of C holds
( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x )
proof
let a be Attribute of C; ::_thesis: ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x )
A11: ( ex x being Element of X st a in the Intent of x implies a in union { the Intent of x where x is Element of B-carrier C : x in X } )
proof
assume A12: ex x being Element of X st a in the Intent of x ; ::_thesis: a in union { the Intent of x where x is Element of B-carrier C : x in X }
ex Y being set st
( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } )
proof
consider x being Element of X such that
A13: a in the Intent of x by A12;
x in X ;
then the Intent of x in { the Intent of x where x is Element of B-carrier C : x in X } ;
hence ex Y being set st
( a in Y & Y in { the Intent of x where x is Element of B-carrier C : x in X } ) by A13; ::_thesis: verum
end;
hence a in union { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4; ::_thesis: verum
end;
( a in union { the Intent of x where x is Element of B-carrier C : x in X } implies ex x being Element of X st a in the Intent of x )
proof
assume a in union { the Intent of x where x is Element of B-carrier C : x in X } ; ::_thesis: ex x being Element of X st a in the Intent of x
then consider Y being set such that
A14: a in Y and
A15: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4;
ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A15;
hence ex x being Element of X st a in the Intent of x by A14; ::_thesis: verum
end;
hence ( a in union { the Intent of x where x is Element of B-carrier C : x in X } iff ex x being Element of X st a in the Intent of x ) by A11; ::_thesis: verum
end;
union { the Intent of x where x is Element of B-carrier C : x in X } c= the carrier' of C
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union { the Intent of x where x is Element of B-carrier C : x in X } or x in the carrier' of C )
assume x in union { the Intent of x where x is Element of B-carrier C : x in X } ; ::_thesis: x in the carrier' of C
then consider Y being set such that
A16: x in Y and
A17: Y in { the Intent of x where x is Element of B-carrier C : x in X } by TARSKI:def_4;
ex Y9 being Element of B-carrier C st
( Y = the Intent of Y9 & Y9 in X ) by A17;
hence x in the carrier' of C by A16; ::_thesis: verum
end;
then consider A9 being Subset of the carrier' of C such that
A18: for a being Attribute of C holds
( a in A9 iff ex x being Element of X st a in the Intent of x ) by A10;
A19: for o being Object of C holds
( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )
proof
let o be Object of C; ::_thesis: ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )
A20: ( ( for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) implies o in O )
proof
assume A21: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; ::_thesis: o in O
for x being Element of X holds o in the Extent of x
proof
let x be Element of X; ::_thesis: o in the Extent of x
o in (AttributeDerivation C) . the Intent of x by A21;
hence o in the Extent of x by Def10; ::_thesis: verum
end;
hence o in O by A9; ::_thesis: verum
end;
( o in O implies for x being Element of X holds o in (AttributeDerivation C) . the Intent of x )
proof
assume A22: o in O ; ::_thesis: for x being Element of X holds o in (AttributeDerivation C) . the Intent of x
for x being Element of X holds o in (AttributeDerivation C) . the Intent of x
proof
let x be Element of X; ::_thesis: o in (AttributeDerivation C) . the Intent of x
o in the Extent of x by A9, A22;
hence o in (AttributeDerivation C) . the Intent of x by Def10; ::_thesis: verum
end;
hence for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ; ::_thesis: verum
end;
hence ( o in O iff for x being Element of X holds o in (AttributeDerivation C) . the Intent of x ) by A20; ::_thesis: verum
end;
A23: for x being set st x in (AttributeDerivation C) . A9 holds
x in O
proof
let x be set ; ::_thesis: ( x in (AttributeDerivation C) . A9 implies x in O )
assume x in (AttributeDerivation C) . A9 ; ::_thesis: x in O
then x in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } by Def4;
then consider x9 being Object of C such that
A24: x9 = x and
A25: for a being Attribute of C st a in A9 holds
x9 is-connected-with a ;
for x being Element of X holds x9 in (AttributeDerivation C) . the Intent of x
proof
let x be Element of X; ::_thesis: x9 in (AttributeDerivation C) . the Intent of x
for a being Attribute of C st a in the Intent of x holds
x9 is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in the Intent of x implies x9 is-connected-with a )
assume a in the Intent of x ; ::_thesis: x9 is-connected-with a
then a in A9 by A18;
hence x9 is-connected-with a by A25; ::_thesis: verum
end;
then x9 in { o where o is Object of C : for a being Attribute of C st a in the Intent of x holds
o is-connected-with a } ;
hence x9 in (AttributeDerivation C) . the Intent of x by Def4; ::_thesis: verum
end;
hence x in O by A19, A24; ::_thesis: verum
end;
consider A being Subset of the carrier' of C such that
A26: A = (ObjectDerivation C) . ((AttributeDerivation C) . A9) ;
set p = ConceptStr(# O,A #);
for x being set st x in O holds
x in (AttributeDerivation C) . A9
proof
let x9 be set ; ::_thesis: ( x9 in O implies x9 in (AttributeDerivation C) . A9 )
assume A27: x9 in O ; ::_thesis: x9 in (AttributeDerivation C) . A9
then reconsider x9 = x9 as Object of C ;
for a being Attribute of C st a in A9 holds
x9 is-connected-with a
proof
let a be Attribute of C; ::_thesis: ( a in A9 implies x9 is-connected-with a )
assume a in A9 ; ::_thesis: x9 is-connected-with a
then consider x being Element of X such that
A28: a in the Intent of x by A18;
x9 in (AttributeDerivation C) . the Intent of x by A19, A27;
then x9 in { o where o is Object of C : for a being Attribute of C st a in the Intent of x holds
o is-connected-with a } by Def4;
then ex y being Object of C st
( y = x9 & ( for a being Attribute of C st a in the Intent of x holds
y is-connected-with a ) ) ;
hence x9 is-connected-with a by A28; ::_thesis: verum
end;
then x9 in { o where o is Object of C : for a being Attribute of C st a in A9 holds
o is-connected-with a } ;
hence x9 in (AttributeDerivation C) . A9 by Def4; ::_thesis: verum
end;
then O = (AttributeDerivation C) . A9 by A23, TARSKI:1;
then ConceptStr(# O,A #) is FormalConcept of C by A26, Th21;
then reconsider p = ConceptStr(# O,A #) as Element of (ConceptLattice C) by Th31;
A29: for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= p
proof
let b be Element of (ConceptLattice C); ::_thesis: ( b is_less_than X implies b [= p )
assume A30: b is_less_than X ; ::_thesis: b [= p
the Extent of (b @) c= the Extent of (p @)
proof
let x9 be set ; :: according to TARSKI:def_3 ::_thesis: ( not x9 in the Extent of (b @) or x9 in the Extent of (p @) )
assume A31: x9 in the Extent of (b @) ; ::_thesis: x9 in the Extent of (p @)
then reconsider x9 = x9 as Object of C ;
for x being Element of X holds x9 in the Extent of x
proof
let x be Element of X; ::_thesis: x9 in the Extent of x
x in X ;
then reconsider x = x as Element of (ConceptLattice C) ;
b [= x by A30, LATTICE3:def_16;
then b @ is-SubConcept-of x @ by Th43;
then the Extent of (b @) c= the Extent of (x @) by Def16;
hence x9 in the Extent of x by A31; ::_thesis: verum
end;
hence x9 in the Extent of (p @) by A9; ::_thesis: verum
end;
then b @ is-SubConcept-of p @ by Def16;
hence b [= p by Th43; ::_thesis: verum
end;
for q being Element of (ConceptLattice C) st q in X holds
p [= q
proof
let q be Element of (ConceptLattice C); ::_thesis: ( q in X implies p [= q )
assume A32: q in X ; ::_thesis: p [= q
the Extent of (p @) c= the Extent of (q @)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of (p @) or x in the Extent of (q @) )
assume x in the Extent of (p @) ; ::_thesis: x in the Extent of (q @)
hence x in the Extent of (q @) by A9, A32; ::_thesis: verum
end;
then p @ is-SubConcept-of q @ by Def16;
hence p [= q by Th43; ::_thesis: verum
end;
then p is_less_than X by LATTICE3:def_16;
hence ex a being Element of (ConceptLattice C) st
( a is_less_than X & ( for b being Element of (ConceptLattice C) st b is_less_than X holds
b [= a ) ) by A29; ::_thesis: verum
end;
end;
end;
hence ConceptLattice C is complete Lattice by VECTSP_8:def_6; ::_thesis: verum
end;
registration
let C be FormalContext;
cluster ConceptLattice C -> non empty strict complete ;
coherence
ConceptLattice C is complete by Th44;
end;