:: Introduction to Concept Lattices
:: by Christoph Schwarzweller
::
:: Received October 2, 1998
:: Copyright (c) 1998-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, XBOOLE_0, RELAT_1, CAT_1, SUBSET_1, TARSKI, FUNCT_1,
ZFMISC_1, MCART_1, YELLOW_1, LATTICE3, ORDERS_2, FILTER_1, WAYBEL_1,
WAYBEL_0, XXREAL_0, PBOOLE, EQREL_1, CLASSES2, BINOP_1, LATTICES,
QC_LANG1, REWRITE1, SETFAM_1, CONLAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XTUPLE_0, MCART_1, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, STRUCT_0, LATTICES,
ORDERS_2, YELLOW_1, WAYBEL_1, LATTICE3, SETFAM_1, WAYBEL_0;
constructors BINOP_1, DOMAIN_1, LATTICE3, WAYBEL_1, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, FUNCT_2, STRUCT_0, LATTICES,
LATTICE3, YELLOW_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
equalities TARSKI, BINOP_1;
expansions TARSKI;
theorems TARSKI, RELAT_1, FUNCT_1, FUNCT_2, ZFMISC_1, LATTICES, LATTICE3,
YELLOW_1, ORDERS_2, FILTER_1, VECTSP_8, SETFAM_1, WAYBEL_0, RELSET_1,
XBOOLE_0, XBOOLE_1, XTUPLE_0;
schemes BINOP_1;
begin
registration
cluster strict non empty non void for 2-sorted;
existence
proof
2-sorted(#{{}},{{}}#) is non empty non void;
hence thesis;
end;
end;
definition
::$CD
struct (2-sorted) ContextStr (# carrier, carrier' -> set, Information ->
Relation of the carrier,the carrier' #);
end;
registration
cluster strict non empty non void for ContextStr;
existence
proof
ContextStr(#{{}},{{}},the Relation of {{}},{{}}#) is non empty non void;
hence thesis;
end;
end;
definition
mode FormalContext is non empty non void 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 empty non void 2-sorted;
cluster the carrier' of C -> non empty;
coherence;
cluster the carrier of C -> non empty;
coherence;
end;
registration
let C be non empty non void 2-sorted;
cluster non empty for Subset of the carrier of C;
existence
proof
take the carrier of C;
the carrier of C c= the carrier of C;
hence thesis;
end;
cluster non empty for Subset of the carrier' of C;
existence
proof
take the carrier' of C;
the carrier' of C c= the carrier' of C;
hence thesis;
end;
end;
definition
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
pred o is-connected-with a means
[o,a] in the Information of C;
end;
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;
:: Derivation Operators
begin
definition
let C be FormalContext;
func ObjectDerivation(C) -> Function of bool the carrier of C,bool the
carrier' of C means
:Def2:
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
proof
set f = the set of all
[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 ;
for u being object st u in f holds ex v,w being object st u = [v,w]
proof
let u be object;
assume u in f;
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 thesis;
end;
then reconsider f as Relation by RELAT_1:def 1;
for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2
proof
let u,v1,v2 be object;
assume that
A1: [u,v1] in f and
A2: [u,v2] in f;
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 thesis by A4,A6;
end;
then reconsider f as Function by FUNCT_1:def 1;
A7: for x being object holds x in dom f implies x in bool the carrier of C
proof
let x be object;
assume x in dom f;
then consider y being object 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 thesis;
end;
for x being object holds x in bool the carrier of C implies x in dom f
proof
let x be object;
assume x in bool the carrier of C;
then reconsider 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 thesis by XTUPLE_0:def 12;
end;
then
A10: dom f = bool the carrier of C by A7,TARSKI:2;
rng f c= bool the carrier' of C
proof
let y be object;
assume y in rng f;
then consider x being object 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 object;
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};
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 thesis;
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 thesis by A13;
end;
then reconsider
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;
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;
consider y being object 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 thesis by A10,A14,A16,FUNCT_1:def 2;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function of bool the carrier of C,bool the carrier' of C;
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}
;
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}
;
A19: for O being object st O in bool the carrier of C holds F1.O = F2.O
proof
let O be object;
assume O in bool the carrier of C;
then reconsider 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 thesis;
end;
dom F1 = bool the carrier of C & dom F2 = bool the carrier of C by
FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:2;
end;
end;
definition
let C be FormalContext;
func AttributeDerivation(C) -> Function of bool the carrier' of C,bool the
carrier of C means
:Def3:
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
proof
set f = the set of all
[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 ;
for u being object st u in f holds ex v,w being object st u = [v,w]
proof
let u be object;
assume u in f;
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 thesis;
end;
then reconsider f as Relation by RELAT_1:def 1;
for u,v1,v2 being object st [u,v1] in f & [u,v2] in f holds v1 = v2
proof
let u,v1,v2 be object;
assume that
A1: [u,v1] in f and
A2: [u,v2] in f;
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 thesis by A4,A6;
end;
then reconsider f as Function by FUNCT_1:def 1;
A7: for x being object holds x in dom f implies x in bool the carrier' of C
proof
let x be object;
assume x in dom f;
then consider y being object 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 thesis;
end;
for x being object holds x in bool the carrier' of C implies x in dom f
proof
let x be object;
assume x in bool the carrier' of C;
then reconsider 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 thesis by XTUPLE_0:def 12;
end;
then
A10: dom f = bool the carrier' of C by A7,TARSKI:2;
rng f c= bool the carrier of C
proof
let y be object;
assume y in rng f;
then consider x being object 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 object;
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};
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 thesis;
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 thesis by A13;
end;
then reconsider
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;
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;
consider y being object 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 thesis by A10,A14,A16,FUNCT_1:def 2;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Function of bool the carrier' of C,bool the carrier of C;
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};
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};
A19: for A being object st A in bool the carrier' of C holds F1.A = F2.A
proof
let A be object;
assume A in bool the carrier' of C;
then reconsider 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 thesis;
end;
dom F1 = bool the carrier' of C & dom F2 = bool the carrier' of C by
FUNCT_2:def 1;
hence thesis by A19,FUNCT_1:2;
end;
end;
theorem
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;
let o be Object of C;
{o} c= the carrier of C
proof
let x be object;
assume x in {o};
then x = o by TARSKI:def 1;
hence thesis;
end;
then reconsider t = {o} as Subset of the carrier of C;
A1: for x being object 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} implies x in {a where a is
Attribute of C : o is-connected-with a}
proof
set o9 = the Element of t;
let x be object;
reconsider o9 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};
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 as Attribute of C;
o9 is-connected-with x by A3;
hence thesis by A2;
end;
A4: for x being object holds 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}
proof
let x be object;
assume x in {a where a is Attribute of C : o is-connected-with a};
then
A5: ex x9 being Attribute of C st x9 = x & o is-connected-with x9;
then reconsider 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 thesis;
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 Def2;
hence thesis by A1,A4,TARSKI:2;
end;
theorem
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;
let a be Attribute of C;
{a} c= the carrier' of C
proof
let x be object;
assume x in {a};
then x = a by TARSKI:def 1;
hence thesis;
end;
then reconsider t = {a} as Subset of the carrier' of C;
A1: for x being object 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} implies x in {o where o
is Object of C : o is-connected-with a}
proof
set a9 = the Element of t;
let x be object;
reconsider a9 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};
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 as Object of C;
x is-connected-with a9 by A3;
hence thesis by A2;
end;
A4: for x being object holds 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}
proof
let x be object;
assume x in {o where o is Object of C : o is-connected-with a};
then
A5: ex x9 being Object of C st x9 = x & x9 is-connected-with a;
then reconsider 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 thesis;
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 Def3;
hence thesis by A1,A4,TARSKI:2;
end;
theorem Th3:
for C being FormalContext for O1,O2 being Subset of the carrier
of C holds O1 c= O2 implies (ObjectDerivation(C)).O2 c= (ObjectDerivation(C)).
O1
proof
let C be FormalContext;
let O1,O2 be Subset of the carrier of C;
assume
A1: O1 c= O2;
let x be object;
assume x in (ObjectDerivation(C)).O2;
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 Def2;
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 thesis by Def2;
end;
theorem Th4:
for C being FormalContext for A1,A2 being Subset of the carrier'
of C holds A1 c= A2 implies (AttributeDerivation(C)).A2 c= (AttributeDerivation
(C)).A1
proof
let C be FormalContext;
let A1,A2 be Subset of the carrier' of C;
assume
A1: A1 c= A2;
let x be object;
assume x in (AttributeDerivation(C)).A2;
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 Def3;
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 thesis by Def3;
end;
theorem Th5:
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;
let O be Subset of the carrier of C;
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 object holds x in A implies x in the carrier' of C
proof
let x be object;
assume x in 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;
hence thesis;
end;
then reconsider A as Subset of the carrier' of C by TARSKI:def 3;
let x be object;
assume
A1: x in O;
then reconsider 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;
assume a in 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 thesis by A1;
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 Def3;
then x in (AttributeDerivation(C)).A by A2;
hence thesis by Def2;
end;
theorem Th6:
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;
let A be Subset of the carrier' of C;
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 object holds x in O implies x in the carrier of C
proof
let x be object;
assume x in O;
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 thesis;
end;
then reconsider O as Subset of the carrier of C by TARSKI:def 3;
let x be object;
assume
A1: x in A;
then reconsider 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;
assume o in O;
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 thesis by A1;
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 Def2;
then x in (ObjectDerivation(C)).O by A2;
hence thesis by Def3;
end;
theorem Th7:
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;
let O be Subset of the carrier of C;
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
holds o is-connected-with a};
set A9 = {a where a is Attribute of C : for o being Object of C st o in O9
holds o is-connected-with a};
A1: for x being object holds x in A9 implies x in A
proof
let x be object;
assume x in A9;
then
A2: 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 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;
assume
A3: o in O;
now
per cases;
case
o in O9;
hence thesis by A2;
end;
case
not o in O9;
then consider a being Attribute of C such that
A4: a in 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 thesis by A3,A5;
end;
end;
hence thesis;
end;
hence thesis;
end;
for x being object holds x in A implies x in A9
proof
let x be object;
assume
A6: x in 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 as Attribute of C;
for o being Object of C st o in O9 holds o is-connected-with x
proof
let o be Object of C;
assume o in O9;
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 thesis by A6;
end;
hence thesis;
end;
then
A7: A = A9 by A1,TARSKI:2;
A c= the carrier' of C
proof
let x be object;
assume x in 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;
hence thesis;
end;
then reconsider A as Subset of the carrier' of C;
O9 c= the carrier of C
proof
let x be object;
assume x in O9;
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 thesis;
end;
then reconsider O9 as Subset of the carrier of C;
A = (ObjectDerivation(C)).O & O9 = (AttributeDerivation(C)).A by Def2,Def3;
hence thesis by A7,Def2;
end;
theorem Th8:
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;
let A be Subset of the carrier' of C;
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
holds o is-connected-with a};
set O9 = {o where o is Object of C : for a being Attribute of C st a in A9
holds o is-connected-with a};
A1: for x being object holds x in O9 implies x in O
proof
let x be object;
assume x in O9;
then
A2: 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 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;
assume
A3: a in A;
now
per cases;
case
a in A9;
hence thesis by A2;
end;
case
not a in A9;
then consider o being Object of C such that
A4: o in O 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 thesis by A3,A5;
end;
end;
hence thesis;
end;
hence thesis;
end;
for x being object holds x in O implies x in O9
proof
let x be object;
assume
A6: x in O;
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 as Object of C;
for a being Attribute of C st a in A9 holds x is-connected-with a
proof
let a be Attribute of C;
assume a in A9;
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 thesis by A6;
end;
hence thesis;
end;
then
A7: O = O9 by A1,TARSKI:2;
O c= the carrier of C
proof
let x be object;
assume x in O;
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 thesis;
end;
then reconsider O as Subset of the carrier of C;
A9 c= the carrier' of C
proof
let x be object;
assume x in A9;
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 thesis;
end;
then reconsider A9 as Subset of the carrier' of C;
O = (AttributeDerivation(C)).A & A9 = (ObjectDerivation(C)).O by Def2,Def3;
hence thesis by A7,Def3;
end;
theorem Th9:
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;
let O be Subset of the carrier of C;
let A be Subset of the carrier' 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;
let x be object;
assume
A3: x in O;
then reconsider 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;
consider z being set such that
A4: z = [x,a];
assume a in A;
then z in [:O,A:] by A3,A4,ZFMISC_1:def 2;
hence thesis by A2,A4;
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 thesis by Def3;
end;
O c= (AttributeDerivation(C)).A implies [:O,A:] c= the Information of C
proof
assume O c= (AttributeDerivation(C)).A;
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 Def3;
let z be object;
assume z in [:O,A:];
then consider x,y being object such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def 2;
reconsider y as Attribute of C by A7;
reconsider 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 thesis by A8;
end;
hence thesis by A1;
end;
theorem Th10:
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;
let O be Subset of the carrier of C;
let A be Subset of the carrier' 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;
let x be object;
assume
A3: x in A;
then reconsider 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;
consider z being set such that
A4: z = [o,x];
assume o in O;
then z in [:O,A:] by A3,A4,ZFMISC_1:def 2;
hence thesis by A2,A4;
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 thesis by Def2;
end;
A c= (ObjectDerivation(C)).O implies [:O,A:] c= the Information of C
proof
assume A c= (ObjectDerivation(C)).O;
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 Def2;
let z be object;
assume z in [:O,A:];
then consider x,y being object such that
A6: x in O and
A7: y in A and
A8: z = [x,y] by ZFMISC_1:def 2;
reconsider y as Attribute of C by A7;
reconsider 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 thesis by A8;
end;
hence thesis by A1;
end;
theorem
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;
let O be Subset of the carrier of C;
let A be Subset of the carrier' of C;
O c= (AttributeDerivation(C)).A iff [:O,A:] c= the Information of C by Th9;
hence thesis by Th10;
end;
definition
let C be FormalContext;
func phi(C) -> Function of BoolePoset the carrier of C, BoolePoset the
carrier' of C equals
ObjectDerivation(C);
coherence
proof
A1: rng(ObjectDerivation(C)) c= the carrier of BoolePoset the carrier' of C
proof
let x be object;
assume x in rng(ObjectDerivation(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 thesis by A2,YELLOW_1:def 2;
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 object holds x in the carrier of BoolePoset the carrier of C
implies x in dom(ObjectDerivation(C))
proof
let x be object;
assume x in the carrier of BoolePoset the carrier of 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 thesis by FUNCT_2:def 1;
end;
for x being object holds x in dom(ObjectDerivation(C)) implies x in the
carrier of BoolePoset the carrier of C
proof
let x be object;
assume x in dom(ObjectDerivation(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 thesis by A3,YELLOW_1:def 2;
end;
then
dom(ObjectDerivation(C)) = the carrier of BoolePoset the carrier of C
by A4,TARSKI:2;
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 thesis;
end;
end;
definition
let C be FormalContext;
func psi(C) -> Function of BoolePoset the carrier' of C, BoolePoset the
carrier of C equals
AttributeDerivation(C);
coherence
proof
A1: rng(AttributeDerivation(C)) c= the carrier of BoolePoset(the carrier of C)
proof
let x be object;
assume x in rng(AttributeDerivation(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 thesis by A2,YELLOW_1:def 2;
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 object holds x in the carrier of BoolePoset(the carrier' of C
) implies x in dom(AttributeDerivation(C))
proof
let x be object;
assume x in the carrier of BoolePoset the carrier' of 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 thesis by FUNCT_2:def 1;
end;
for x being object holds x in dom(AttributeDerivation(C)) implies x in
the carrier of BoolePoset the carrier' of C
proof
let x be object;
assume x in dom(AttributeDerivation(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 thesis by A3,YELLOW_1:def 2;
end;
then dom(AttributeDerivation(C)) = the carrier of BoolePoset the carrier'
of C by A4,TARSKI:2;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
definition
let P,R be non empty RelStr;
let Con be Connection of P,R;
attr Con is co-Galois means
ex f being Function of P,R, g being
Function of R,P st (Con = [f,g] & f is antitone & g is antitone & for p1,p2
being Element of P, r1,r2 being Element of R holds p1 <= g.(f.p1) & r1 <= f.(g.
r1));
end;
theorem Th12:
for P,R being non empty Poset for Con being Connection of P,R
for f being Function of P,R, g being Function of R,P st Con = [f,g] holds Con
is co-Galois iff for p being Element of P, r being Element of R holds p <= g.r
iff r <= f.p
proof
let P,R be non empty Poset;
let Con be Connection of P,R;
let f be Function of P,R, g be Function of R,P;
assume
A1: Con = [f,g];
A2: now
assume
A3: for p being Element of P, r being Element of R holds p <= g.r iff r <= f.p;
for p1,p2 being Element of P st p1 <= p2 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;
assume
A4: p1 <= p2;
let r1,r2 be Element of R;
assume
A5: r1 = f.p1 & r2 = f.p2;
p2 <= g.(f.p2) by A3;
then p1 <= g.(f.p2) by A4,ORDERS_2:3;
hence thesis by A3,A5;
end;
then
A6: f is antitone by WAYBEL_0:def 5;
for r1,r2 being Element of R st r1 <= r2 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;
assume
A7: r1 <= r2;
let p1,p2 be Element of P;
assume
A8: p1 = g.r1 & p2 = g.r2;
r2 <= f.(g.r2) by A3;
then r1 <= f.(g.r2) by A7,ORDERS_2:3;
hence thesis by A3,A8;
end;
then
A9: g is antitone by WAYBEL_0:def 5;
for p1,p2 being Element of P, 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;
end;
now
assume Con is co-Galois;
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, r1,r2 being Element of R holds p1 <=
g9.(f9.p1) & r1 <= f9.(g9.r1);
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, r being Element of R holds r <= f.p implies
p <= g.r
proof
let p be Element of P, r be Element of R;
assume r <= f.p;
then
A17: g.r >= g.(f.p) by A12,A14,WAYBEL_0:def 5;
p <= g.(f.p) by A13,A15,A14;
hence thesis by A17,ORDERS_2:3;
end;
for p being Element of P, r being Element of R holds p <= g.r implies
r <= f.p
proof
let p be Element of P, r be Element of R;
assume p <= g.r;
then
A18: f.p >= f.(g.r) by A11,A15,WAYBEL_0:def 5;
r <= f.(g.r) by A13,A15,A14;
hence thesis by A18,ORDERS_2:3;
end;
hence for p being Element of P, r being Element of R holds p <= g.r iff r
<= f.p by A16;
end;
hence thesis by A2;
end;
theorem
for P,R being non empty Poset for Con being Connection of P,R st Con
is co-Galois for f being Function of P,R, 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;
let Con be Connection of P,R;
assume Con is co-Galois;
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, r1,r2 being Element of R holds p1 <=
g9.(f9.p1) & r1 <= f9.(g9.r1);
let f be Function of P,R, g be Function of R,P;
assume
A5: Con = [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 object st x in the carrier of P holds f.x =(f*(g*f)).x
proof
let x be object;
assume x in the carrier of P;
then reconsider 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 thesis by A12,FUNCT_1:13;
end;
A13: for x being object st x in the carrier of R holds g.x =(g*(f*g)).x
proof
let x be object;
assume x in the carrier of R;
then reconsider 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 thesis by A15,FUNCT_1:13;
end;
dom (f*(g*f)) = the carrier of P & dom (g*(f*g)) = the carrier of R by
FUNCT_2:def 1;
hence thesis by A9,A8,A10,A13,FUNCT_1:2;
end;
theorem
for C being FormalContext holds [phi(C),psi(C)] is co-Galois
proof
let C be FormalContext;
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, 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, y be Element of
BoolePoset the carrier' of C;
assume y <= (phi(C)).x;
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 as Element of BooleLatt the carrier of C by A2,YELLOW_1:def 2;
reconsider x as Subset of the carrier of C by LATTICE3:def 1;
reconsider 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 as Subset of the carrier' of C by LATTICE3:def 1;
reconsider y as Subset of the carrier' of C by LATTICE3:def 1;
for z being object holds z in y implies z in x9 by A5,XBOOLE_0:def 3;
then y c= x9;
then
A6: (AttributeDerivation(C)).x9 c= (AttributeDerivation(C)).y by Th4;
reconsider 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 as Subset of the carrier of C by LATTICE3:def 1;
reconsider y9 as Element of (BooleLatt the carrier of C);
A7: x c= (AttributeDerivation(C)).((ObjectDerivation(C)).x) by Th5;
reconsider x as Subset of the carrier of C;
reconsider x as Element of (BooleLatt the carrier of C);
x "\/" y9 = y9 by A6,A7,XBOOLE_1: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 thesis by ORDERS_2:def 5;
end;
for x being Element of BoolePoset the carrier of C, 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, y be Element of
BoolePoset the carrier' of C;
assume x <= (psi(C)).y;
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 as Element of (BooleLatt the carrier' of C) by A1,
YELLOW_1:def 2;
reconsider y as Subset of the carrier' of C by LATTICE3:def 1;
reconsider 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 as Subset of the carrier of C by LATTICE3:def 1;
reconsider x as Subset of the carrier of C by LATTICE3:def 1;
for z being object holds z in x implies z in y9 by A9,XBOOLE_0:def 3;
then
A10: x c= y9;
reconsider x,y9 as Subset of the carrier of C;
A11: (ObjectDerivation(C)).y9 c= (ObjectDerivation(C)).x by A10,Th3;
reconsider 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 as Subset of the carrier' of C by LATTICE3:def 1;
reconsider x9 as Element of (BooleLatt the carrier' of C);
A12: y c= (ObjectDerivation(C)).((AttributeDerivation(C)).y) by Th6;
reconsider y as Element of (BooleLatt the carrier' of C);
y "\/" x9 = x9 by A11,A12,XBOOLE_1: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 thesis by ORDERS_2:def 5;
end;
hence thesis by A3,Th12;
end;
theorem Th15:
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;
let O1,O2 be Subset of the carrier of C;
reconsider O9 = O1 \/ O2 as Subset of the carrier of C;
A1: for x being object holds x in (ObjectDerivation(C)).O1 /\ (
ObjectDerivation( C ) ) . O2 implies x in (ObjectDerivation(C)).O9
proof
let x be object;
assume
A2: x in (ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2;
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 Def2;
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 Def2;
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 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;
assume
A5: o in (O1 \/ O2);
now
per cases by A5,XBOOLE_0:def 3;
case
o in O1;
hence thesis by A3;
end;
case
o in O2;
hence thesis by A4;
end;
end;
hence thesis;
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 thesis by Def2;
end;
for x being object holds x in (ObjectDerivation(C)).(O1 \/ O2) implies x in
(ObjectDerivation(C)).O1 /\ (ObjectDerivation(C)).O2
proof
let x be object;
assume x in (ObjectDerivation(C)).(O1 \/ 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 Def2;
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 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;
assume o in O2;
then o in O9 by XBOOLE_0:def 3;
hence thesis by A6;
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 Def2;
for o being Object of C st o in O1 holds o is-connected-with x
proof
let o be Object of C;
assume o in O1;
then o in O9 by XBOOLE_0:def 3;
hence thesis by A6;
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 Def2;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th16:
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;
let A1,A2 be Subset of the carrier' of C;
reconsider A9 = A1 \/ A2 as Subset of the carrier' of C;
A1: for x being object holds x in (AttributeDerivation(C)).A1 /\ (
AttributeDerivation(C)).A2 implies x in (AttributeDerivation(C)).A9
proof
let x be object;
assume
A2: x in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2;
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 Def3;
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 Def3;
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 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;
assume
A5: a in (A1 \/ A2);
now
per cases by A5,XBOOLE_0:def 3;
case
a in A1;
hence thesis by A3;
end;
case
a in A2;
hence thesis by A4;
end;
end;
hence thesis;
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 thesis by Def3;
end;
for x being object holds x in (AttributeDerivation(C)).(A1 \/ A2) implies x
in (AttributeDerivation(C)).A1 /\ (AttributeDerivation(C)).A2
proof
let x be object;
assume x in (AttributeDerivation(C)).(A1 \/ 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 Def3;
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 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;
assume a in A2;
then a in A9 by XBOOLE_0:def 3;
hence thesis by A6;
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 Def3;
for a being Attribute of C st a in A1 holds x is-connected-with a
proof
let a be Attribute of C;
assume a in A1;
then a in A9 by XBOOLE_0:def 3;
hence thesis by A6;
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 Def3;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by A1,TARSKI:2;
end;
theorem Th17:
for C being FormalContext holds (ObjectDerivation(C)).{} = the carrier' of C
proof
let C be FormalContext;
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 object holds x in A implies x in the carrier' of C
proof
let x be object;
assume x in A;
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 thesis;
end;
A2: for x being object holds x in the carrier' of C implies x in A
proof
let x be object;
assume x in the carrier' of C;
then reconsider x as Attribute of C;
for o being Object of C st o in e holds o is-connected-with x;
hence thesis;
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 Def2;
hence thesis by A1,A2,TARSKI:2;
end;
theorem Th18:
for C being FormalContext holds (AttributeDerivation(C)).{} =
the carrier of C
proof
let C be FormalContext;
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 object holds x in O implies x in the carrier of C
proof
let x be object;
assume x in O;
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 thesis;
end;
A2: for x being object holds x in the carrier of C implies x in O
proof
let x be object;
assume x in the carrier of C;
then reconsider x as Object of C;
for a being Attribute of C st a in e holds x is-connected-with a;
hence thesis;
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 Def3;
hence thesis by A1,A2,TARSKI:2;
end;
begin :: Formal Concepts
definition
let C be 2-sorted;
struct ConceptStr over C (# Extent -> Subset of the carrier of C, Intent ->
Subset of the carrier' of C #);
end;
definition
let C be 2-sorted;
let CP be ConceptStr over C;
attr CP is empty means
:Def7:
the Extent of CP is empty & the Intent of CP is empty;
attr CP is quasi-empty means
:Def8:
the Extent of CP is empty or the Intent of CP is empty;
end;
registration
let C be non empty non void 2-sorted;
cluster strict non empty for ConceptStr over C;
existence
proof
set A = the non empty Subset of the carrier' of C;
set O = the non empty Subset of the carrier of C;
ConceptStr(#O,A#) is non empty;
hence thesis;
end;
cluster strict quasi-empty for ConceptStr over C;
existence
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;
hence thesis;
end;
end;
registration
let C be empty void 2-sorted;
cluster -> empty for ConceptStr over C;
coherence;
end;
Lm1: for C being FormalContext for CS being ConceptStr over C st (
ObjectDerivation(C)).(the Extent of CS) = the Intent of CS holds CS is non
empty
proof
let C be FormalContext;
let CS be ConceptStr over C;
assume
A1: (ObjectDerivation(C)).(the Extent of CS) = the Intent of CS;
now
per cases;
case
the Extent of CS is empty;
then the Intent of CS = the carrier' of C by A1,Th17;
hence thesis;
end;
case
the Extent of CS is non empty;
hence thesis;
end;
end;
hence thesis;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is concept-like means
:Def9:
(ObjectDerivation(C)).(the Extent of
CP) = the Intent of CP & (AttributeDerivation(C)).(the Intent of CP) = the
Extent of CP;
end;
registration
let C be FormalContext;
cluster concept-like non empty for ConceptStr over C;
existence
proof
set o = the Object of C;
set A = (ObjectDerivation(C)).({o});
{o} c= the carrier of C
proof
let x be object;
assume x in {o};
then x = o by TARSKI:def 1;
hence thesis;
end;
then reconsider t = {o} as Subset of the carrier of C;
A c= the carrier' of C
proof
let x be object;
assume x in A;
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 Def2;
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 thesis;
end;
then reconsider A as Subset of the carrier' of C;
set O = (AttributeDerivation(C)).((ObjectDerivation(C)).({o}));
O c= the carrier of C
proof
let x be object;
assume x in O;
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 Def3;
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 thesis;
end;
then reconsider O as Subset of the carrier of C;
set M9 = ConceptStr(#O,A#);
o in {o} & t c= (AttributeDerivation(C)).((ObjectDerivation(C)).t) by Th5,
TARSKI:def 1;
then reconsider M9 as non empty ConceptStr over C by Def7;
(ObjectDerivation(C)).(the Extent of M9) = (ObjectDerivation(C)).t by Th7
.= the Intent of M9;
then M9 is concept-like;
hence thesis;
end;
end;
definition
let C be FormalContext;
mode FormalConcept of C is concept-like non empty ConceptStr over C;
end;
registration
let C be FormalContext;
cluster strict for FormalConcept of C;
existence
proof
set CP = the FormalConcept of C;
A1: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & (
AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
the Intent of CP is non empty or the Extent of CP is non empty by Def7;
then the ConceptStr of CP is FormalConcept of C by A1,Def7,Def9;
hence thesis;
end;
end;
theorem Th19:
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, 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;
let O be Subset of the carrier of C;
A1: for O9 being Subset of the carrier of C, 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;
let A9 be Subset of the carrier' of C;
assume that
A2: ConceptStr(#O9,A9#) is FormalConcept of C and
A3: O c= O9;
reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2;
A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9
.= O9;
A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9
.= A9;
(ObjectDerivation(C)).(O9) c= (ObjectDerivation(C)).(O) by A3,Th3;
hence thesis by A4,A5,Th4;
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 M9) = the Intent of M9 by Th7;
hence thesis by Def9,Lm1;
end;
hence thesis by A1;
end;
theorem
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;
let O be Subset of the carrier of C;
A1: now
O c= (AttributeDerivation(C)).((ObjectDerivation(C)).O) by Th5;
then
A2: for x being object holds x in O implies 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;
(AttributeDerivation(C)).((ObjectDerivation(C)).O) c= O by A3,Th19;
then
for x being object holds x in (AttributeDerivation(C)).((ObjectDerivation
(C)).O) implies x in O;
hence (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O by A2,TARSKI:2
;
end;
now
reconsider A = (ObjectDerivation(C)).O as Subset of the carrier' of C;
set M9 = ConceptStr(#O,A#);
assume (AttributeDerivation(C)).((ObjectDerivation(C)).O) = O;
then M9 is FormalConcept of C by Def9,Lm1;
hence ex A being Subset of the carrier' of C st ConceptStr(#O,A#) is
FormalConcept of C;
end;
hence thesis by A1;
end;
theorem Th21:
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, 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;
let A be Subset of the carrier' of C;
A1: for O9 being Subset of the carrier of C, 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;
let A9 be Subset of the carrier' of C;
assume that
A2: ConceptStr(#O9,A9#) is FormalConcept of C and
A3: A c= A9;
reconsider M9 = ConceptStr(#O9,A9#) as FormalConcept of C by A2;
A4: (AttributeDerivation(C)).(A9) = the Extent of M9 by Def9
.= O9;
A5: (ObjectDerivation(C)).(O9) = the Intent of M9 by Def9
.= A9;
(AttributeDerivation(C)).(A9) c= (AttributeDerivation(C)).(A) by A3,Th4;
hence thesis by A4,A5,Th3;
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 M9) = the Extent of M9 by Th8;
hence thesis by Def9,Lm1;
end;
hence thesis by A1;
end;
theorem
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;
let A be Subset of the carrier' of C;
A1: now
A c= (ObjectDerivation(C)).((AttributeDerivation(C)).A) by Th6;
then
A2: for x being object holds x in A implies 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;
(ObjectDerivation(C)).((AttributeDerivation(C)).A) c= A by A3,Th21;
then
for x being object holds x in (ObjectDerivation(C)).((AttributeDerivation
(C)).A) implies x in A;
hence (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A by A2,TARSKI:2
;
end;
now
reconsider O = (AttributeDerivation(C)).A as Subset of the carrier of C;
set M9 = ConceptStr(#O,A#);
assume (ObjectDerivation(C)).((AttributeDerivation(C)).A) = A;
then M9 is FormalConcept of C by Def9,Lm1;
hence ex O being Subset of the carrier of C st ConceptStr(#O,A#) is
FormalConcept of C;
end;
hence thesis by A1;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is universal means
the Extent of CP = the carrier of C;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
attr CP is co-universal means
the Intent of CP = the carrier' of C;
end;
registration
let C be FormalContext;
cluster strict universal for FormalConcept of C;
existence
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;
hence thesis;
end;
cluster strict co-universal for FormalConcept of C;
existence
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;
hence thesis;
end;
end;
definition
let C be FormalContext;
func Concept-with-all-Objects(C) -> strict universal FormalConcept of C
means
:Def12:
ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).({}) & A
= (ObjectDerivation(C)).((AttributeDerivation(C)).({}));
existence
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;
hence thesis;
end;
uniqueness;
end;
definition
let C be FormalContext;
func Concept-with-all-Attributes(C) -> strict co-universal FormalConcept of
C means
:Def13:
ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st it = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((
ObjectDerivation(C)).({})) & A = (ObjectDerivation(C)).({});
existence
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;
hence thesis;
end;
uniqueness;
end;
theorem Th23:
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;
(ex O being Subset of the carrier of C, 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, 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 Def12,Def13;
hence thesis by Th17,Th18;
end;
theorem
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;
let CP be FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: the Intent of CP = {} implies CP is universal by A1,Th18;
A3: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
the Extent of CP = {} implies CP is co-universal by A3,Th17;
hence thesis by A2;
end;
theorem Th25:
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;
let CP be strict FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
A3: now
assume
A4: the Intent of CP = {};
then the Extent of CP = the carrier of C by A1,Th18;
then CP is universal;
hence CP = Concept-with-all-Objects(C) by A2,A1,A4,Def12;
end;
now
assume
A5: the Extent of CP = {};
then the Intent of CP = the carrier' of C by A2,Th17;
then CP is co-universal;
hence CP = Concept-with-all-Attributes(C) by A2,A1,A5,Def13;
end;
hence thesis by A3;
end;
theorem
for C being FormalContext for CP being quasi-empty ConceptStr over C
st CP is FormalConcept of C holds CP is universal or CP is co-universal
proof
let C be FormalContext;
let CP be quasi-empty ConceptStr over C;
assume CP is FormalConcept of C;
then reconsider CP as FormalConcept of C;
A1: (AttributeDerivation(C)).(the Intent of CP) = the Extent of CP by Def9;
A2: (ObjectDerivation(C)).(the Extent of CP) = the Intent of CP by Def9;
now
per cases by Def8;
case
the Intent of CP is empty;
then the Extent of CP = the carrier of C by A1,Th18;
hence CP is universal;
end;
case
the Extent of CP is empty;
then the Intent of CP = the carrier' of C by A2,Th17;
hence CP is co-universal;
end;
end;
hence thesis;
end;
theorem
for C being FormalContext for CP being quasi-empty ConceptStr over C
st CP is strict FormalConcept of C holds CP = Concept-with-all-Objects(C) or CP
= Concept-with-all-Attributes(C)
proof
let C be FormalContext;
let CP be quasi-empty ConceptStr over C;
assume
A1: CP is strict FormalConcept of C;
now
per cases by Def8;
case
the Intent of CP is empty;
hence CP = Concept-with-all-Objects(C) by A1,Th25;
end;
case
the Extent of CP is empty;
hence CP = Concept-with-all-Attributes(C) by A1,Th25;
end;
end;
hence thesis;
end;
definition
let C be FormalContext;
mode Set-of-FormalConcepts of C -> non empty set means
:Def14:
for X being set st X in it holds X is FormalConcept of C;
existence
proof
set CP = the FormalConcept of C;
for X being set st X in {CP} holds X is FormalConcept of C by TARSKI:def 1;
hence thesis;
end;
end;
definition
let C be FormalContext;
let FCS be Set-of-FormalConcepts of C;
redefine mode Element of FCS -> FormalConcept of C; :: redefines Element (SUBSET_1, definition)
coherence by Def14;
end;
definition
let C be FormalContext;
let CP1,CP2 be FormalConcept of C;
pred CP1 is-SubConcept-of CP2 means
the Extent of CP1 c= the Extent of CP2;
end;
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:
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;
let CP1,CP2 be FormalConcept of C;
A1: now
assume the Intent of CP2 c= the Intent of CP1;
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 Def9;
hence CP1 is-SubConcept-of CP2 by A2;
end;
now
assume CP1 is-SubConcept-of CP2;
then
A3: the Extent of CP1 c= the Extent of CP2;
(ObjectDerivation(C)).(the Extent of CP2) = the Intent of CP2 & (
ObjectDerivation(C)).(the Extent of CP1) = the Intent of CP1 by Def9;
hence the Intent of CP2 c= the Intent of CP1 by A3,Th3;
end;
hence thesis by A1;
end;
theorem
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
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;
let CP be FormalConcept of C;
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 thesis by A1,Th28;
end;
begin :: Concept Lattices
definition
let C be FormalContext;
func B-carrier(C) -> non empty set equals
{ ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) is non empty & (ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E
};
coherence
proof
set M9 = { ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E };
M9 is non empty
proof
set CP = the FormalConcept of C;
consider O being Subset of the carrier of C such that
A1: O = the Extent of CP;
consider A being Subset of the carrier' of C such that
A2: A = the Intent of CP;
A3: (AttributeDerivation(C)).A = O by A1,A2,Def9;
A4: (ObjectDerivation(C)).O = A by A1,A2,Def9;
then ConceptStr(#O,A#) is non empty by Lm1;
then ConceptStr(#O,A#) in M9 by A4,A3;
hence thesis;
end;
then reconsider M9 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;
now
assume CP in M9;
then ex E being Subset of the carrier of C, I being Subset of the
carrier' of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non 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;
end;
hence thesis;
end;
hence thesis;
end;
end;
definition
let C be FormalContext;
redefine func B-carrier(C) -> Set-of-FormalConcepts of C; :: redefines B-carrier (CONLAT_1, definition)
coherence
proof
for X being set holds X in B-carrier(C) implies X is FormalConcept of C
proof
let X be set;
assume X in B-carrier(C);
then
ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st X = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & (
ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E;
hence thesis by Def9;
end;
hence thesis by Def14;
end;
end;
registration
let C be FormalContext;
cluster B-carrier(C) -> non empty;
coherence;
end;
theorem Th31:
for C being FormalContext for CP being object holds CP in B-carrier
(C) iff CP is strict FormalConcept of C
proof
let C be FormalContext;
let CP be object;
A1: CP is strict FormalConcept of C implies CP in B-carrier(C)
proof
assume
A2: CP is strict FormalConcept of C;
then reconsider CP as FormalConcept of C;
set I9 = the Intent of CP;
set E9 = the Extent of CP;
(ObjectDerivation(C)).E9 = I9 & (AttributeDerivation(C)).I9 = E9 by Def9;
hence thesis by A2;
end;
CP in B-carrier(C) implies CP is strict FormalConcept of C
proof
assume CP in B-carrier(C);
then ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st CP = ConceptStr(#E,I#) & ConceptStr(#E,I#) is non empty & (
ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E;
hence thesis by Def9;
end;
hence thesis by A1;
end;
definition
let C be FormalContext;
func B-meet(C) -> BinOp of B-carrier(C) means
:Def17:
for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, 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
proof
defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being
Subset of the carrier of C, 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 being Element of B-carrier(C), CP2 being Element of B-carrier(
C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP]
proof
let CP1 be Element of B-carrier(C);
let CP2 be Element of B-carrier(C);
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(#O,A#);
A2: (AttributeDerivation(C)).A = (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 Def9
.= (the Extent of CP1) /\ (the Extent of CP2) by Def9;
then
A3: (ObjectDerivation(C)).O = A by Th7;
then ConceptStr(#O,A#) is non empty by Lm1;
then
CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2,A3;
hence thesis;
end;
consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C)
such that
A4: for CP1 being Element of B-carrier(C), CP2 being Element of
B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1);
reconsider f as BinOp of B-carrier(C);
take f;
for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of
the carrier of C, 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;
CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31;
hence thesis by A4;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be BinOp of B-carrier(C);
assume
A5: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, 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)));
assume
A6: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, 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)));
A7: for X being object st X in [:B-carrier(C),B-carrier(C):]
holds F1.X = F2 .X
proof
let X be object;
assume X in [:B-carrier(C),B-carrier(C):];
then consider A,B being object 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 as strict FormalConcept of C by A9,Th31;
reconsider A as strict FormalConcept of C by A8,Th31;
(ex O being Subset of the carrier of C, 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,
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 thesis by A10;
end;
dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C),
B-carrier(C ):] by FUNCT_2:def 1;
hence thesis by A7,FUNCT_1:2;
end;
end;
definition
let C be FormalContext;
func B-join(C) -> BinOp of B-carrier(C) means
:Def18:
for CP1,CP2 being
strict FormalConcept of C holds ex O being Subset of the carrier of C, 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
proof
defpred P[FormalConcept of C, FormalConcept of C, set] means ex O being
Subset of the carrier of C, 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 being Element of B-carrier(C), CP2 being Element of B-carrier(
C) ex CP being Element of B-carrier(C) st P[CP1,CP2,CP]
proof
let CP1 be Element of B-carrier(C);
let CP2 be Element of B-carrier(C);
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(#O,A#);
A2: (ObjectDerivation(C)).O = (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 Def9
.= (the Intent of CP1) /\ (the Intent of CP2) by Def9;
then (AttributeDerivation(C)).A = O & ConceptStr(#O,A#) is non empty by
Lm1,Th7;
then
CP in {ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
Subset of the carrier' of C : ConceptStr(#E,I#) is non empty & (
ObjectDerivation(C)).E = I & (AttributeDerivation(C)).I = E } by A2;
hence thesis;
end;
consider f being Function of [:B-carrier(C),B-carrier(C):],B-carrier(C)
such that
A3: for CP1 being Element of B-carrier(C), CP2 being Element of
B-carrier(C) holds P[CP1,CP2,f.(CP1,CP2)] from BINOP_1:sch 3(A1);
reconsider f as BinOp of B-carrier(C);
take f;
for CP1,CP2 being strict FormalConcept of C holds ex O being Subset of
the carrier of C, 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;
CP1 is Element of B-carrier(C) & CP2 is Element of B-carrier(C) by Th31;
hence thesis by A3;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be BinOp of B-carrier(C);
assume
A4: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, 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);
assume
A5: for CP1,CP2 being strict FormalConcept of C holds ex O being
Subset of the carrier of C, 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);
A6: for X being object st X in [:B-carrier(C),B-carrier(C):]
holds F1.X = F2 .X
proof
let X be object;
assume X in [:B-carrier(C),B-carrier(C):];
then consider A,B being object 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 as strict FormalConcept of C by A8,Th31;
reconsider A as strict FormalConcept of C by A7,Th31;
(ex O being Subset of the carrier of C, 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,
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 thesis by A9;
end;
dom F1 = [:B-carrier(C),B-carrier(C):] & dom F2 = [:B-carrier(C),
B-carrier(C ):] by FUNCT_2:def 1;
hence thesis by A6,FUNCT_1:2;
end;
end;
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;
let CP1,CP2 be strict FormalConcept of 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 thesis by FUNCT_1:def 3;
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;
let CP1,CP2 be strict FormalConcept of 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 thesis by FUNCT_1:def 3;
end;
theorem Th32:
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;
let CP1,CP2 be strict FormalConcept of C;
(ex O being Subset of the carrier of C, 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, 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 Def17;
hence thesis;
end;
theorem Th33:
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;
let CP1,CP2 be strict FormalConcept of C;
(ex O being Subset of the carrier of C, 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, 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 Def18;
hence thesis;
end;
theorem Th34:
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;
let CP1,CP2,CP3 be strict FormalConcept of C;
(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, 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, 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 Def17;
(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, 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, 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 Def17;
(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 thesis by A1,A2,XBOOLE_1:16;
end;
theorem Th35:
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;
let CP1,CP2,CP3 be strict FormalConcept of C;
(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, 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, 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 Def18;
(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, 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, 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 Def18;
(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 thesis by A1,A2,XBOOLE_1:16;
end;
theorem Th36:
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;
let CP1,CP2 be strict FormalConcept of C;
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, 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, 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 Def17,Def18;
(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 Def9
.= the Extent of CP2 by Def9;
((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 Def9
.= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2)))
/\ (the Intent of CP2) by Def9
.= ((ObjectDerivation(C)). ((the Extent of CP1) /\ (the Extent of CP2)))
/\ ((ObjectDerivation(C)).(the Extent of CP2)) by Def9
.= (ObjectDerivation(C)).(the Extent of CP2) by A1,Th3,XBOOLE_1:28
.= the Intent of CP2 by Def9;
hence thesis by A2,A3;
end;
theorem Th37:
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;
let CP1,CP2 be strict FormalConcept of C;
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, 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, 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 Def17,Def18;
(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 Def9
.= the Intent of CP1 by Def9;
(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 Def9
.= (the Extent of CP1) /\ ((AttributeDerivation(C)). ((the Intent of CP1
) /\ (the Intent of CP2))) by Def9
.= ((AttributeDerivation(C)).(the Intent of CP1)) /\ ((
AttributeDerivation(C)). ((the Intent of CP1) /\ (the Intent of CP2))) by Def9
.= (AttributeDerivation(C)).(the Intent of CP1) by A1,Th4,XBOOLE_1:28
.= the Extent of CP1 by Def9;
hence thesis by A2,A3;
end;
theorem
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;
let CP be strict FormalConcept of 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-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 Def17;
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
,Def9
.= (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,Def9
.= (ObjectDerivation(C)).(the Extent of CP) by Th7
.= the Intent of CP by Def9;
hence thesis by A1,A4;
end;
theorem Th39:
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;
let CP be strict FormalConcept of 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 Def18;
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 Def9
.= the Extent of Concept-with-all-Objects(C) by Def9;
A = ((ObjectDerivation(C)).(the Extent of CP)) /\ (the Intent of
Concept-with-all-Objects(C)) by A3,Def9
.= ((ObjectDerivation(C)).(the Extent of CP)) /\ ((ObjectDerivation(C)).
(the Extent of Concept-with-all-Objects(C))) by Def9
.= (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 Def9;
hence thesis by A1,A4;
end;
theorem
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;
let CP be strict FormalConcept of 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-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 Def18;
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,Def9
.= (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,Def9
.= (AttributeDerivation(C)).(the Intent of CP) by Th8
.= the Extent of CP by Def9;
hence thesis by A1,A4;
end;
theorem
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;
let CP be strict FormalConcept of 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 Def17;
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 Def9
.= the Intent of Concept-with-all-Attributes(C) by Def9;
O = ((AttributeDerivation(C)).(the Intent of CP)) /\ (the Extent of
Concept-with-all-Attributes(C)) by A2,Def9
.= ((AttributeDerivation(C)).(the Intent of CP)) /\ ((
AttributeDerivation(C)). (the Intent of Concept-with-all-Attributes(C))) by
Def9
.= (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 Def9;
hence thesis by A1,A4;
end;
definition
let C be FormalContext;
func ConceptLattice(C) -> strict non empty LattStr equals
LattStr(#B-carrier
(C),B-join(C),B-meet(C)#);
coherence;
end;
theorem Th42:
for C being FormalContext holds ConceptLattice(C) is Lattice
proof
let C be FormalContext;
set L = LattStr(#B-carrier(C),B-join(C),B-meet(C)#);
reconsider L as strict non empty 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;
reconsider b,c as Element of B-carrier(C);
reconsider d = (B-join(C)).(b,c) as Element of L;
reconsider b,c as Element of L;
reconsider a,b as Element of B-carrier(C);
reconsider e = (B-join(C)).(a,b) as Element of L;
reconsider a,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,b,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 thesis by A2,A3;
end;
A4: for a,b being Element of L holds (a"/\"b)"\/"b = b
proof
let a,b be Element of L;
reconsider a,b as Element of B-carrier(C);
reconsider d = (B-meet(C)).(a,b) as Element of L;
reconsider a,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,b as strict FormalConcept of C by Th31;
(B-join(C)).((B-meet(C)).(a,b),b) = b by Th36;
hence thesis by A5;
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;
reconsider b,c as Element of B-carrier(C);
reconsider d = (B-meet(C)).(b,c) as Element of L;
reconsider b,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,b as Element of B-carrier(C);
reconsider e = (B-meet(C)).(a,b) as Element of L;
reconsider a,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,b,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 thesis by A7,A8;
end;
A9: for a,b being Element of L holds a"/\"b = b"/\"a
proof
let a,b be Element of L;
A10: b"/\"a = (B-meet(C)).(b,a) by LATTICES:def 2;
reconsider a,b as strict FormalConcept of C by Th31;
(B-meet(C)).(a,b) = (B-meet(C)).(b,a) by Th32;
hence thesis by A10,LATTICES:def 2;
end;
A11: for a,b being Element of L holds a"/\"(a"\/"b)=a
proof
let a,b be Element of L;
reconsider a,b as Element of B-carrier(C);
reconsider d = (B-join(C)).(a,b) as Element of L;
reconsider a,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,b as strict FormalConcept of C by Th31;
(B-meet(C)).(a,(B-join(C)).(a,b)) = a by Th37;
hence thesis by A12;
end;
for a,b being Element of L holds a"\/"b = b"\/"a
proof
let a,b be Element of L;
A13: b"\/"a = (B-join(C)).(b,a) by LATTICES:def 1;
reconsider a,b as strict FormalConcept of C by Th31;
(B-join(C)).(a,b) = (B-join(C)).(b,a) by Th33;
hence thesis by A13,LATTICES:def 1;
end;
then L is join-commutative join-associative meet-absorbing meet-commutative
meet-associative join-absorbing by A1,A4,A9,A6,A11,LATTICES:def 4,def 5,def 6
,def 7,def 8,def 9;
hence thesis;
end;
registration
let C be FormalContext;
cluster ConceptLattice(C) -> strict non empty Lattice-like;
coherence by Th42;
end;
definition
let C be FormalContext;
let S be non empty Subset of ConceptLattice(C);
redefine mode Element of S -> FormalConcept of C; :: redefines Element (SUBSET_1, definition)
coherence
proof
let s be Element of S;
s is Element of B-carrier(C);
hence thesis;
end;
end;
definition
let C be FormalContext;
let CP be Element of ConceptLattice(C);
func CP@ -> strict FormalConcept of C equals
CP;
coherence by Th31;
end;
theorem Th43:
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;
let CP1,CP2 be Element of ConceptLattice(C);
set CL = ConceptLattice(C);
A1: now
assume
A2: CP1@ is-SubConcept-of 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 Def18;
the Extent of CP1@ c= the Extent of CP2@ by A2;
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,Def9
.= the Extent of CP2@ by Def9;
then CP1 "\/" CP2 = CP2 by A3,A4,A6,LATTICES:def 1;
hence CP1 [= CP2 by LATTICES:def 3;
end;
now
assume CP1 [= CP2;
then CP1 "\/" CP2 = CP2 by LATTICES:def 3;
then
A7: (the L_join of CL).(CP1,CP2) = CP2 by LATTICES:def 1;
ex O being Subset of the carrier of C, 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 Def18;
then
for x being object holds x in the Intent of CP2@ implies x in the Intent
of CP1@ by A7,XBOOLE_0:def 4;
then the Intent of CP2@ c= the Intent of CP1@;
hence CP1@ is-SubConcept-of CP2@ by Th28;
end;
hence thesis by A1;
end;
theorem Th44:
for C being FormalContext holds ConceptLattice(C) is complete Lattice
proof
let C be FormalContext;
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);
per cases;
suppose
A1: X = {};
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);
assume b is_less_than X;
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);
reconsider CP as strict FormalConcept of C by Th31;
reconsider CO as strict FormalConcept of C;
(B-join(C)).(CO,CP) = (B-join(C)).(CP,CO) by Th33
.= CO by Th39;
hence thesis by LATTICES:def 1;
end;
hence thesis;
end;
then ConceptLattice(C) is upper-bounded by LATTICES:def 14;
then Top ConceptLattice(C) "\/" b = Top ConceptLattice(C);
hence thesis by LATTICES:def 3;
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 thesis by A2;
end;
suppose
X <> {};
then reconsider 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 ExX
proof
let x be Element of X;
x in X;
then reconsider x as Element of B-carrier(C);
the Extent of x in ExX;
hence thesis;
end;
then reconsider ExX as non empty set;
set E1 = meet ExX;
A4: for o being Object of C holds o in E1 iff for x being Element of X
holds o in the Extent of x
proof
let o be Object of C;
A5: (for x being Element of X holds o in the Extent of x) implies o in E1
proof
assume
A6: for x being Element of X holds o in the Extent of x;
for Y being set holds Y in ExX implies o in Y
proof
let Y be set;
assume Y in ExX;
then
ex Y9 being Element of B-carrier(C) st Y = the Extent of Y9 &
Y9 in X;
hence thesis by A6;
end;
hence thesis by SETFAM_1:def 1;
end;
o in E1 implies for x being Element of X holds o in the Extent of x
proof
assume
A7: o in E1;
let x be Element of X;
the Extent of x in ExX by A3;
hence thesis by A7,SETFAM_1:def 1;
end;
hence thesis by A5;
end;
E1 c= the carrier of C
proof
set Y = the Element of ExX;
let x be object;
Y in ExX;
then consider Y9 being Element of B-carrier(C) such that
A8: Y = the Extent of Y9 and
Y9 in X;
assume x in E1;
then x in the Extent of Y9 by A8,SETFAM_1:def 1;
hence thesis;
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 InX;
A10: for a being Attribute of C holds a in In iff ex x being Element of
X st a in the Intent of x
proof
let a be Attribute of C;
A11: (ex x being Element of X st a in the Intent of x) implies a in In
proof
assume
A12: ex x being Element of X st a in the Intent of x;
ex Y being set st a in Y & Y in InX
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 InX;
hence thesis by A13;
end;
hence thesis by TARSKI:def 4;
end;
a in In implies ex x being Element of X st a in the Intent of x
proof
assume a in In;
then consider Y being set such that
A14: a in Y and
A15: Y in InX by TARSKI:def 4;
ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9
in X by A15;
hence thesis by A14;
end;
hence thesis by A11;
end;
In c= the carrier' of C
proof
let x be object;
assume x in In;
then consider Y being set such that
A16: x in Y and
A17: Y in InX by TARSKI:def 4;
ex Y9 being Element of B-carrier(C) st Y = the Intent of Y9 & Y9
in X by A17;
hence thesis by A16;
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;
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);
for x being Element of X holds o in the Extent of x
proof
let x be Element of X;
o in (AttributeDerivation(C)).(the Intent of x) by A21;
hence thesis by Def9;
end;
hence thesis by A9;
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;
for x being Element of X holds o in (AttributeDerivation(C)).(
the Intent of x)
proof
let x be Element of X;
o in the Extent of x by A9,A22;
hence thesis by Def9;
end;
hence thesis;
end;
hence thesis by A20;
end;
A23: for x being object holds x in (AttributeDerivation(C)).A9 implies x in O
proof
let x be object;
assume x in (AttributeDerivation(C)).A9;
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 Def3;
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;
for a being Attribute of C st a in (the Intent of x) holds x9
is-connected-with a by A18,A25;
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 thesis by Def3;
end;
hence thesis by A19,A24;
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 object
holds x in O implies x in (AttributeDerivation(C)). A9
proof
let x9 be object;
assume
A27: x9 in O;
then reconsider 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;
assume a in A9;
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 Def3;
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 thesis by A28;
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 thesis by Def3;
end;
then O = (AttributeDerivation(C)).A9 by A23,TARSKI:2;
then p is FormalConcept of C by A26,Th21;
then reconsider p 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);
assume
A30: b is_less_than X;
the Extent of b@ c= the Extent of p@
proof
let x9 be object;
assume
A31: x9 in the Extent of b@;
then reconsider 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;
x in X;
then reconsider 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@;
hence thesis by A31;
end;
hence thesis by A9;
end;
then b@ is-SubConcept-of p@;
hence thesis by Th43;
end;
for q being Element of ConceptLattice(C) st q in X holds p [= q
proof
let q be Element of ConceptLattice(C);
assume
A32: q in X;
the Extent of p@ c= the Extent of q@
by A9,A32;
then p@ is-SubConcept-of q@;
hence thesis by Th43;
end;
then p is_less_than X by LATTICE3:def 16;
hence thesis by A29;
end;
end;
hence thesis by VECTSP_8:def 6;
end;
registration
let C be FormalContext;
cluster ConceptLattice(C) -> complete;
coherence by Th44;
end;