:: A Characterization of Concept Lattices; Dual Concept Lattices
:: by Christoph Schwarzweller
::
:: Received August 17, 1999
:: Copyright (c) 1999-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 CONLAT_1, STRUCT_0, QC_LANG1, SUBSET_1, LATTICES, XXREAL_2,
PBOOLE, EQREL_1, XBOOLE_0, SETFAM_1, FUNCT_1, TARSKI, CAT_1, LATTICE3,
ZFMISC_1, RELAT_1, FUNCT_3, LATTICE6, REWRITE1, GROUP_6, WELLORD1,
FUNCT_2, MCART_1, FILTER_1, XXREAL_0, ORDERS_2, CONLAT_2, LATTICE4;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, XTUPLE_0, MCART_1,
FUNCT_1, DOMAIN_1, RELSET_1, ORDERS_2, STRUCT_0, LATTICE2, LATTICE3,
LATTICE6, PARTFUN1, FUNCT_2, LATTICES, LATTICE4, CONLAT_1;
constructors DOMAIN_1, LATTICE2, LATTICE4, CONLAT_1, LATTICE6, RELSET_1,
XTUPLE_0;
registrations SUBSET_1, FUNCT_1, FUNCT_2, STRUCT_0, LATTICES, LATTICE2,
LATTICE3, CONLAT_1, RELSET_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, LATTICE3, VECTSP_8, LATTICE6, FUNCT_1, XBOOLE_0;
equalities LATTICE3, XBOOLE_0, SUBSET_1;
expansions LATTICE3, LATTICE6, FUNCT_1, XBOOLE_0;
theorems TARSKI, RELAT_1, FUNCT_1, ZFMISC_1, LATTICE4, LATTICES, LATTICE3,
SETFAM_1, FUNCT_2, FILTER_1, LATTICE2, ORDERS_2, CONLAT_1, XTUPLE_0;
schemes FUNCT_2;
begin
definition
let C be FormalContext;
let CP be strict FormalConcept of C;
func @CP -> Element of ConceptLattice(C) equals
CP;
coherence
proof
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
hence thesis by CONLAT_1:31;
end;
end;
registration
let C be FormalContext;
cluster ConceptLattice C -> bounded;
coherence
proof
A1: (@Concept-with-all-Objects(C))@ = Concept-with-all-Objects(C) by
CONLAT_1:def 21;
A2: for a being Element of ConceptLattice(C) holds a [= @
Concept-with-all-Objects(C)
proof
let a be Element of ConceptLattice(C);
a@ is-SubConcept-of (@Concept-with-all-Objects(C))@ by A1,CONLAT_1:30;
hence thesis by CONLAT_1:43;
end;
for a being Element of ConceptLattice(C) holds @
Concept-with-all-Objects(C) "\/" a = @Concept-with-all-Objects(C) & a "\/" @
Concept-with-all-Objects(C) = @Concept-with-all-Objects(C)
by A2,LATTICES:def 3;
then
A3: ConceptLattice C is upper-bounded by LATTICES:def 14;
A4: (@Concept-with-all-Attributes(C))@ = Concept-with-all-Attributes(C) by
CONLAT_1:def 21;
A5: for a being Element of ConceptLattice(C) holds @
Concept-with-all-Attributes(C) [= a
proof
let a be Element of ConceptLattice(C);
(@Concept-with-all-Attributes(C))@ is-SubConcept-of a@ by A4,CONLAT_1:30;
hence thesis by CONLAT_1:43;
end;
for a being Element of ConceptLattice(C) holds @
Concept-with-all-Attributes(C) "/\" a = @Concept-with-all-Attributes(C) & a
"/\" @Concept-with-all-Attributes(C) = @Concept-with-all-Attributes(C)
by A5,LATTICES:4;
then ConceptLattice C is lower-bounded by LATTICES:def 13;
hence thesis by A3;
end;
end;
theorem Th1:
for C being FormalContext holds Bottom (ConceptLattice(C)) =
Concept-with-all-Attributes(C) & Top (ConceptLattice(C)) =
Concept-with-all-Objects(C)
proof
let C be FormalContext;
A1: (@Concept-with-all-Objects(C))@ = Concept-with-all-Objects(C) by
CONLAT_1:def 21;
A2: for a being Element of ConceptLattice(C) holds a [= @
Concept-with-all-Objects(C)
proof
let a be Element of ConceptLattice(C);
a@ is-SubConcept-of (@Concept-with-all-Objects(C))@ by A1,CONLAT_1:30;
hence thesis by CONLAT_1:43;
end;
A3: for a being Element of ConceptLattice(C) holds @Concept-with-all-Objects
(C) "\/" a = @Concept-with-all-Objects(C) & a "\/" @Concept-with-all-Objects(C)
= @Concept-with-all-Objects(C) by A2,LATTICES:def 3;
A4: (@Concept-with-all-Attributes(C))@ = Concept-with-all-Attributes(C) by
CONLAT_1:def 21;
A5: for a being Element of ConceptLattice(C) holds @
Concept-with-all-Attributes(C) [= a
proof
let a be Element of ConceptLattice(C);
(@Concept-with-all-Attributes(C))@ is-SubConcept-of a@ by A4,CONLAT_1:30;
hence thesis by CONLAT_1:43;
end;
for a being Element of ConceptLattice(C) holds @
Concept-with-all-Attributes(C) "/\" a = @Concept-with-all-Attributes(C) & a
"/\" @Concept-with-all-Attributes(C) = @Concept-with-all-Attributes(C)
by A5,LATTICES:4;
hence thesis by A3,LATTICES:def 16,def 17;
end;
theorem Th2:
for C being FormalContext for D being non empty Subset-Family of
the carrier of C holds (ObjectDerivation(C)).(union D) = meet({(
ObjectDerivation(C)).O where O is Subset of the carrier of C : O in D})
proof
let C be FormalContext;
let D be non empty Subset-Family of(the carrier of C);
reconsider D9=D as non empty Subset-Family of the carrier of C;
set OU = (ObjectDerivation(C)).(union D);
set M = meet({(ObjectDerivation(C)).O where O is Subset of the carrier of C
: O in D});
per cases;
suppose
A1: {(ObjectDerivation(C)).O where O is Subset of the carrier of C : O
in D} <> {};
thus OU c= M
proof
let x be object;
assume x in OU;
then x in {a9 where a9 is Attribute of C : for o being Object of C st o
in union D9 holds o is-connected-with a9} by CONLAT_1:def 3;
then
A2: ex x9 being Attribute of C st x9 = x & for o being Object of C st o
in union D holds o is-connected-with x9;
then reconsider x as Attribute of C;
A3: for O being Subset of the carrier of C st O in D for o being Object
of C st o in O holds o is-connected-with x
proof
let O be Subset of the carrier of C;
assume
A4: O in D;
let o be Object of C;
assume o in O;
then o in union D by A4,TARSKI:def 4;
hence thesis by A2;
end;
A5: for O being Subset of the carrier of C st O in D holds x in (
ObjectDerivation(C)).O
proof
let O be Subset of the carrier of C;
assume O in D;
then for o being Object of C st o in O holds o is-connected-with x by
A3;
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 CONLAT_1:def 3;
end;
for Y being set holds Y in {(ObjectDerivation(C)).O where O is
Subset of the carrier of C : O in D} implies x in Y
proof
let Y be set;
assume Y in {(ObjectDerivation(C)).O where O is Subset of the
carrier of C : O in D};
then
ex O being Subset of the carrier of C st Y = ( ObjectDerivation(C)
).O & O in D;
hence thesis by A5;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
thus M c= OU
proof
set d = the Element of {(ObjectDerivation(C)).O where O is Subset of the
carrier of C : O in D};
let x be object;
assume
A6: x in M;
then
A7: x in d by A1,SETFAM_1:def 1;
d in {(ObjectDerivation(C)).O where O is Subset of the carrier of C
: O in D} by A1;
then
ex X being Subset of the carrier of C st d = ( ObjectDerivation(C)).
X & X in D;
then reconsider x as Attribute of C by A7;
A8: for O being Subset of the carrier of C st O in D holds x in (
ObjectDerivation(C)).O
proof
let O be Subset of the carrier of C;
assume O in D;
then (ObjectDerivation(C)).O in {(ObjectDerivation(C)).O9 where O9 is
Subset of the carrier of C : O9 in D};
hence thesis by A6,SETFAM_1:def 1;
end;
A9: for O being Subset of the carrier of C st O in D for o being Object
of C st o in O holds o is-connected-with x
proof
let O be Subset of the carrier of C;
assume O in D;
then x in (ObjectDerivation(C)).O by A8;
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} by CONLAT_1:def 3;
then
A10: 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;
let o be Object of C;
assume o in O;
hence thesis by A10;
end;
for o being Object of C st o in union D holds o is-connected-with x
proof
let o be Object of C;
assume o in union D;
then ex Y being set st o in Y & Y in D by TARSKI:def 4;
hence thesis by A9;
end;
then x in {a9 where a9 is Attribute of C : for o being Object of C st o
in union D9 holds o is-connected-with a9};
hence thesis by CONLAT_1:def 3;
end;
end;
suppose
A11: {(ObjectDerivation(C)).O where O is Subset of the carrier of C :
O in D} = {};
D = {}
proof
set x = the Element of D;
assume D <> {};
(ObjectDerivation(C)).x in {(ObjectDerivation(C)).O where O is
Subset of the carrier of C : O in D};
hence thesis by A11;
end;
hence thesis;
end;
end;
theorem Th3:
for C being FormalContext for D being non empty Subset-Family of(
the carrier' of C) holds (AttributeDerivation(C)).(union D) = meet({(
AttributeDerivation(C)).A where A is Subset of the carrier' of C : A in D})
proof
let C be FormalContext;
let D be non empty Subset-Family of(the carrier' of C);
reconsider D9=D as non empty Subset-Family of the carrier' of C;
set OU = (AttributeDerivation(C)).(union D);
set M = meet({(AttributeDerivation(C)).A where A is Subset of the carrier'
of C : A in D});
now
per cases;
case
A1: {(AttributeDerivation(C)).A where A is Subset of the carrier' of
C: A in D} <> {};
thus OU = M
proof
thus OU c= M
proof
let x be object;
assume x in OU;
then
x in {o9 where o9 is Object of C : for a being Attribute of C st
a in union D9 holds o9 is-connected-with a} by CONLAT_1:def 4;
then
A2: ex x9 being Object of C st x9 = x & for a being Attribute of C st
a in union D holds x9 is-connected-with a;
then reconsider x as Object of C;
A3: for A being Subset of the carrier' of C st A in D for a being
Attribute of C st a in A holds x is-connected-with a
proof
let A be Subset of the carrier' of C;
assume
A4: A in D;
let a be Attribute of C;
assume a in A;
then a in union D by A4,TARSKI:def 4;
hence thesis by A2;
end;
A5: for A being Subset of the carrier' of C st A in D holds x in (
AttributeDerivation(C)).A
proof
let A be Subset of the carrier' of C;
assume A in D;
then for a being Attribute of C st a in A holds x
is-connected-with a by A3;
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 CONLAT_1:def 4;
end;
for Y being set holds Y in {(AttributeDerivation(C)).A where A
is Subset of the carrier' of C : A in D} implies x in Y
proof
let Y be set;
assume Y in {(AttributeDerivation(C)).A where A is Subset of the
carrier' of C : A in D};
then ex A being Subset of the carrier' of C st Y = (
AttributeDerivation(C)).A & A in D;
hence thesis by A5;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
set d = the Element of {(AttributeDerivation(C)).A where A is Subset of the
carrier' of C : A in D};
let x be object;
assume
A6: x in M;
then
A7: x in d by A1,SETFAM_1:def 1;
d in {(AttributeDerivation(C)).A where A is Subset of the
carrier' of C : A in D} by A1;
then ex X being Subset of the carrier' of C st d = (
AttributeDerivation(C)).X & X in D;
then reconsider x as Object of C by A7;
A8: for A being Subset of the carrier' of C st A in D holds x in (
AttributeDerivation(C)).A
proof
let A be Subset of the carrier' of C;
assume A in D;
then (AttributeDerivation(C)).A in {(AttributeDerivation(C)).A9
where A9 is Subset of the carrier' of C : A9 in D};
hence thesis by A6,SETFAM_1:def 1;
end;
A9: for A being Subset of the carrier' of C st A in D for a being
Attribute of C st a in A holds x is-connected-with a
proof
let A be Subset of the carrier' of C;
assume A in D;
then x in (AttributeDerivation(C)).A by A8;
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} by CONLAT_1:def 4;
then
A10: 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;
let a be Attribute of C;
assume a in A;
hence thesis by A10;
end;
for a being Attribute of C st a in union D holds x is-connected-with a
proof
let a be Attribute of C;
assume a in union D;
then ex Y being set st a in Y & Y in D by TARSKI:def 4;
hence thesis by A9;
end;
then x in {o9 where o9 is Object of C : for a being Attribute of C st
a in union D9 holds o9 is-connected-with a};
hence thesis by CONLAT_1:def 4;
end;
end;
case
A11: {(AttributeDerivation(C)).A where A is Subset of the carrier'
of C : A in D} = {};
D = {}
proof
set x = the Element of D;
assume D <> {};
(AttributeDerivation(C)).x in {(AttributeDerivation(C)).A where A
is Subset of the carrier' of C : A in D};
hence thesis by A11;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th4:
for C being FormalContext for D being Subset of ConceptLattice(C)
holds "/\"(D,ConceptLattice(C)) is FormalConcept of C & "\/"(D,ConceptLattice(C
)) is FormalConcept of C
proof
let C be FormalContext;
let D be Subset of ConceptLattice(C);
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
hence thesis by CONLAT_1:31;
end;
definition
let C be FormalContext;
let D be Subset of ConceptLattice(C);
func "/\"(D,C) -> FormalConcept of C equals
"/\"(D,ConceptLattice(C));
coherence by Th4;
func "\/"(D,C) -> FormalConcept of C equals
"\/"(D,ConceptLattice(C));
coherence by Th4;
end;
theorem
for C being FormalContext holds "\/"({} ConceptLattice(C),C) =
Concept-with-all-Attributes(C) & "/\"({} ConceptLattice(C),C) =
Concept-with-all-Objects(C)
proof
let C be FormalContext;
A1: for b being Element of ConceptLattice(C) st b is_less_than {} holds b [=
@Concept-with-all-Objects(C)
proof
let b be Element of ConceptLattice(C);
assume b is_less_than {};
b@ is-SubConcept-of Concept-with-all-Objects(C) &
Concept-with-all-Objects(C ) = (@Concept-with-all-Objects(C))@ by CONLAT_1:30
,def 21;
hence thesis by CONLAT_1:43;
end;
"\/"({} ConceptLattice(C),C) = Bottom ConceptLattice(C) & @
Concept-with-all-Objects(C) is_less_than {} by LATTICE3:49;
hence thesis by A1,Th1,LATTICE3:34;
end;
theorem
for C being FormalContext holds "\/"([#] the carrier of ConceptLattice
(C),C) = Concept-with-all-Objects(C) & "/\"([#] the carrier of ConceptLattice(C
),C) = Concept-with-all-Attributes(C)
proof
let C be FormalContext;
A1: @Concept-with-all-Attributes(C) is_less_than [#] the carrier of
ConceptLattice(C)
proof
let q be Element of ConceptLattice(C);
assume q in [#] the carrier of ConceptLattice(C);
Concept-with-all-Attributes(C) is-SubConcept-of q@ &
Concept-with-all-Attributes(C) = (@Concept-with-all-Attributes(C))@ by
CONLAT_1:30,def 21;
hence thesis by CONLAT_1:43;
end;
"\/"(the carrier of ConceptLattice(C),ConceptLattice(C)) = Top
ConceptLattice (C) & for b being Element of ConceptLattice(C) st b is_less_than
[#] the carrier of ConceptLattice(C) holds b [= @Concept-with-all-Attributes(C)
by LATTICE3:50;
hence thesis by A1,Th1,LATTICE3:34;
end;
theorem
for C being FormalContext for D being non empty Subset of
ConceptLattice(C) holds the Extent of "\/"(D,C) = (AttributeDerivation(C)).((
ObjectDerivation(C)). union {the Extent of ConceptStr(#E,I#) where E is Subset
of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}
) & the Intent of "\/"(D,C) = meet {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D}
proof
let C be FormalContext;
let D be non empty Subset of ConceptLattice(C);
set O = (AttributeDerivation(C)).((ObjectDerivation(C)). union {the Extent
of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D});
set A9 = (ObjectDerivation(C)). union {the Extent of ConceptStr(#E,I#) where
E is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr
(#E,I#) in D};
set y = the Element of D;
{the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C,
I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= bool (the carrier
of C)
proof
let x be object;
assume x in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st x = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
hence thesis;
end;
then reconsider
OO = {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} as
Subset-Family of (the carrier of C);
O c= the carrier of C
proof
set u = union {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
u c= the carrier of C
proof
let x be object;
assume x in u;
then consider Y being set such that
A1: x in Y and
A2: Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by
TARSKI:def 4;
ex E being Subset of the carrier of C, I being Subset of the
carrier' of C st Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D
by A2;
hence thesis by A1;
end;
then reconsider u as Subset of the carrier of C;
let x be object;
A3: (AttributeDerivation(C)).((ObjectDerivation(C)).u) is Element of bool
(the carrier of C);
assume x in O;
hence thesis by A3;
end;
then reconsider o = O as Subset of the carrier of C;
A4: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
A5: for x being object
holds x in D implies x is strict FormalConcept of C & ex
E being Subset of the carrier of C, I being Subset of the carrier' of C st x =
ConceptStr(#E,I#)
proof
let x be object;
assume x in D;
then x is strict FormalConcept of C by A4,CONLAT_1:31;
hence thesis;
end;
then ex E9 being Subset of the carrier of C, I9 being Subset of the carrier'
of C st y = ConceptStr(#E9,I9#);
then
the Extent of y in {the Extent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then reconsider OO as non empty Subset-Family of (the carrier of C);
A6: {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C,
I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= {(
ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9 in {the
Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset
of the carrier' of C : ConceptStr(#E,I#) in D}}
proof
let x be object;
assume x in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the carrier of C, I being Subset of the
carrier' of C such that
A7: x = the Intent of ConceptStr(#E,I#) and
A8: ConceptStr(#E,I#) in D;
ConceptStr(#E,I#) is FormalConcept of C by A5,A8;
then
A9: x = (ObjectDerivation(C)).(the Extent of ConceptStr(#E,I#)) by A7,
CONLAT_1:def 10;
the Extent of ConceptStr(#E,I#) in {the Extent of ConceptStr(#EE,II
#) where EE is Subset of the carrier of C, II is Subset of the carrier' of C :
ConceptStr(#EE,II#) in D} by A8;
hence thesis by A9;
end;
{(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9
in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is
Subset of the carrier' of C : ConceptStr(#E,I#) in D}} c= {the Intent of
ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D}
proof
let x be object;
assume x in {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier
of C : O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier
of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}};
then consider O9 being Subset of the carrier of C such that
A10: x = (ObjectDerivation(C)).O9 and
A11: O9 in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
consider E being Subset of the carrier of C, I being Subset of the
carrier' of C such that
A12: O9 = the Extent of ConceptStr(#E,I#) and
A13: ConceptStr(#E,I#) in D by A11;
ConceptStr(#E,I#) is FormalConcept of C by A5,A13;
then x = the Intent of ConceptStr(#E,I#) by A10,A12,CONLAT_1:def 10;
hence thesis by A13;
end;
then
A14: {(ObjectDerivation(C)).O9 where O9 is Subset of the carrier of C : O9
in { the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I
is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} = {the Intent of
ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D} by A6;
A15: A9 = meet({(ObjectDerivation(C)).O9 where O9 is Subset of the carrier
of C : O9 in OO}) by Th2;
A9 c= the carrier' of C
proof
set y = the Element of D;
set Y = the Element of {the Intent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D};
let x be object;
ex E9 being Subset of the carrier of C, I9 being Subset of the
carrier' of C st y = ConceptStr(#E9,I9#) by A5;
then
A16: the Intent of y in {the Intent of ConceptStr(#E,I#) where E is Subset
of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}
;
then Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then
A17: ex E1 being Subset of the carrier of C, I1 being Subset of the
carrier' of C st Y = the Intent of ConceptStr(#E1,I1#) & ConceptStr(#E1, I1#)
in D;
assume x in A9;
then x in Y by A15,A14,A16,SETFAM_1:def 1;
hence thesis by A17;
end;
then reconsider a = A9 as Subset of the carrier' of C;
union {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier
of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= the carrier
of C
proof
let x be object;
assume x in union {the Extent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider Y being set such that
A18: x in Y and
A19: Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C,I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by
TARSKI:def 4;
ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st Y = the Extent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A19;
hence thesis by A18;
end;
then reconsider CP9 = ConceptStr(#o,a#) as strict FormalConcept of C by
CONLAT_1:19;
reconsider CP = CP9 as Element of ConceptLattice(C) by A4,CONLAT_1:31;
A20: the Intent of CP@ = meet {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D} by A15,A14,CONLAT_1:def 21;
A21: for r being Element of ConceptLattice(C) st D is_less_than r holds CP [= r
proof
let r be Element of ConceptLattice(C);
assume
A22: D is_less_than r;
A23: for q being Element of ConceptLattice(C) st q in D holds the Intent
of r@ c= the Intent of q@
proof
let q be Element of ConceptLattice(C);
assume q in D;
then q [= r by A22;
then q@ is-SubConcept-of r@ by CONLAT_1:43;
hence thesis by CONLAT_1:28;
end;
the Intent of r@ c= meet {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D}
proof
set y = the Element of D;
let x be object;
assume
A24: x in the Intent of r@;
A25: for Y being set holds Y in {the Intent of ConceptStr(#E,I#) where E
is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E
,I#) in D} implies x in Y
proof
let Y be set;
assume Y in {the Intent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider
Ey being Subset of the carrier of C, Iy being Subset of the
carrier' of C such that
A26: Y = the Intent of ConceptStr(#Ey,Iy#) and
A27: ConceptStr(#Ey,Iy#) in D;
reconsider C1 = ConceptStr(#Ey,Iy#) as Element of ConceptLattice(C) by
A27;
the Intent of r@ c= the Intent of C1@ by A23,A27;
then x in the Intent of C1@ by A24;
hence thesis by A26,CONLAT_1:def 21;
end;
ex E9 being Subset of the carrier of C, I9 being Subset of the
carrier' of C st y = ConceptStr(#E9,I9#) by A5;
then the Intent of y in {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D};
hence thesis by A25,SETFAM_1:def 1;
end;
then CP@ is-SubConcept-of r@ by A20,CONLAT_1:28;
hence thesis by CONLAT_1:43;
end;
D is_less_than CP
proof
let q be Element of ConceptLattice(C);
assume q in D;
then q@ in D by CONLAT_1:def 21;
then the Intent of q@ in {the Intent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D};
then the Intent of CP@ c= the Intent of q@ by A20,SETFAM_1:3;
then q@ is-SubConcept-of CP@ by CONLAT_1:28;
hence thesis by CONLAT_1:43;
end;
hence thesis by A15,A14,A21,LATTICE3:def 21;
end;
theorem
for C being FormalContext for D being non empty Subset of
ConceptLattice(C) holds the Extent of "/\"(D,C) = meet {the Extent of
ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D} & the Intent of "/\"(D,C) = (
ObjectDerivation(C)).((AttributeDerivation(C)). union {the Intent of ConceptStr
(#E,I#) where E is Subset of the carrier of C, I is Subset of the carrier' of C
: ConceptStr(#E,I#) in D})
proof
let C be FormalContext;
let D be non empty Subset of ConceptLattice(C);
set A = (ObjectDerivation(C)).((AttributeDerivation(C)). union {the Intent
of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D});
set O9 = (AttributeDerivation(C)). union {the Intent of ConceptStr(#E,I#)
where E is Subset of the carrier of C, I is Subset of the carrier' of C :
ConceptStr(#E,I#) in D};
set y = the Element of D;
{the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C,
I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= bool (the
carrier' of C)
proof
let x be object;
assume x in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st x = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D;
hence thesis;
end;
then reconsider
AA = {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} as
Subset-Family of (the carrier' of C);
A c= the carrier' of C
proof
set u = union {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
u c= the carrier' of C
proof
let x be object;
assume x in u;
then consider Y being set such that
A1: x in Y and
A2: Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by
TARSKI:def 4;
ex E being Subset of the carrier of C, I being Subset of the
carrier' of C st Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D
by A2;
hence thesis by A1;
end;
then reconsider u as Subset of the carrier' of C;
let x be object;
A3: (ObjectDerivation(C)).((AttributeDerivation(C)).u) is Element of bool
(the carrier' of C);
assume x in A;
hence thesis by A3;
end;
then reconsider a = A as Subset of the carrier' of C;
A4: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
A5: for x being object
holds x in D implies x is strict FormalConcept of C & ex
E being Subset of the carrier of C, I being Subset of the carrier' of C st x =
ConceptStr(#E,I#)
proof
let x be object;
assume x in D;
then x is strict FormalConcept of C by A4,CONLAT_1:31;
hence thesis;
end;
then ex E9 being Subset of the carrier of C, I9 being Subset of the carrier'
of C st y = ConceptStr(#E9,I9#);
then
the Intent of y in {the Intent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then reconsider AA as non empty Subset-Family of (the carrier' of C);
A6: {the Extent of ConceptStr(#E,I#) where E is Subset of the carrier of C,
I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= {(
AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C : A9 in {the
Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset
of the carrier' of C : ConceptStr(#E,I#) in D}}
proof
let x be object;
assume x in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider E being Subset of the carrier of C, I being Subset of the
carrier' of C such that
A7: x = the Extent of ConceptStr(#E,I#) and
A8: ConceptStr(#E,I#) in D;
ConceptStr(#E,I#) is FormalConcept of C by A5,A8;
then
A9: x = (AttributeDerivation(C)).(the Intent of ConceptStr(#E,I#)) by A7,
CONLAT_1:def 10;
the Intent of ConceptStr(#E,I#) in {the Intent of ConceptStr(#EE,II#)
where EE is Subset of the carrier of C, II is Subset of the carrier' of C :
ConceptStr(#EE,II#) in D} by A8;
hence thesis by A9;
end;
{(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C :
A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I
is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} c= {the Extent of
ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D}
proof
let x be object;
assume x in {(AttributeDerivation(C)).A9 where A9 is Subset of the
carrier' of C : A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}};
then consider A9 being Subset of the carrier' of C such that
A10: x = (AttributeDerivation(C)).A9 and
A11: A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
consider E being Subset of the carrier of C, I being Subset of the
carrier' of C such that
A12: A9 = the Intent of ConceptStr(#E,I#) and
A13: ConceptStr(#E,I#) in D by A11;
ConceptStr(#E,I#) is FormalConcept of C by A5,A13;
then x = the Extent of ConceptStr(#E,I#) by A10,A12,CONLAT_1:def 10;
hence thesis by A13;
end;
then
A14: {(AttributeDerivation(C)).A9 where A9 is Subset of the carrier' of C :
A9 in {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier of C, I
is Subset of the carrier' of C : ConceptStr(#E,I#) in D}} = {the Extent of
ConceptStr(#E,I#) where E is Subset of the carrier of C, I is Subset of the
carrier' of C : ConceptStr(#E,I#) in D} by A6;
A15: O9 = meet({(AttributeDerivation(C)).A9 where A9 is Subset of the
carrier' of C : A9 in AA}) by Th3;
O9 c= the carrier of C
proof
set y = the Element of D;
set Y = the Element of {the Extent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I #) in D};
let x be object;
ex E9 being Subset of the carrier of C, I9 being Subset of the
carrier' of C st y = ConceptStr(#E9,I9#) by A5;
then
A16: the Extent of y in {the Extent of ConceptStr(#E,I#) where E is Subset
of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D}
;
then Y in {the Extent of ConceptStr(#E,I#) where E is Subset of the
carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then
A17: ex E1 being Subset of the carrier of C, I1 being Subset of the
carrier' of C st Y = the Extent of ConceptStr(#E1,I1#) & ConceptStr(#E1, I1#)
in D;
assume x in O9;
then x in Y by A15,A14,A16,SETFAM_1:def 1;
hence thesis by A17;
end;
then reconsider o = O9 as Subset of the carrier of C;
union {the Intent of ConceptStr(#E,I#) where E is Subset of the carrier
of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} c= the
carrier' of C
proof
let x be object;
assume x in union {the Intent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider Y being set such that
A18: x in Y and
A19: Y in {the Intent of ConceptStr(#E,I#) where E is Subset of the
carrier of C,I is Subset of the carrier' of C : ConceptStr(#E,I#) in D} by
TARSKI:def 4;
ex E being Subset of the carrier of C, I being Subset of the carrier'
of C st Y = the Intent of ConceptStr(#E,I#) & ConceptStr(#E,I#) in D by A19;
hence thesis by A18;
end;
then reconsider CP9 = ConceptStr(#o,a#) as strict FormalConcept of C by
CONLAT_1:21;
reconsider CP = CP9 as Element of ConceptLattice(C) by A4,CONLAT_1:31;
A20: the Extent of CP@ = meet {the Extent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D} by A15,A14,CONLAT_1:def 21;
A21: for r being Element of ConceptLattice(C) st r is_less_than D holds r [= CP
proof
let r be Element of ConceptLattice(C);
assume
A22: r is_less_than D;
A23: for q being Element of ConceptLattice(C) st q in D holds the Extent
of r@ c= the Extent of q@
proof
let q be Element of ConceptLattice(C);
assume q in D;
then r [= q by A22;
then r@ is-SubConcept-of q@ by CONLAT_1:43;
hence thesis by CONLAT_1:def 16;
end;
the Extent of r@ c= meet {the Extent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D}
proof
set y = the Element of D;
let x be object;
assume
A24: x in the Extent of r@;
A25: for Y being set holds Y in {the Extent of ConceptStr(#E,I#) where E
is Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E
,I#) in D} implies x in Y
proof
let Y be set;
assume Y in {the Extent of ConceptStr(#E,I#) where E is Subset of
the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I#) in D};
then consider
Ey being Subset of the carrier of C, Iy being Subset of the
carrier' of C such that
A26: Y = the Extent of ConceptStr(#Ey,Iy#) and
A27: ConceptStr(#Ey,Iy#) in D;
reconsider C1 = ConceptStr(#Ey,Iy#) as Element of ConceptLattice(C) by
A27;
the Extent of r@ c= the Extent of C1@ by A23,A27;
then x in the Extent of C1@ by A24;
hence thesis by A26,CONLAT_1:def 21;
end;
ex E9 being Subset of the carrier of C, I9 being Subset of the
carrier' of C st y = ConceptStr(#E9,I9#) by A5;
then the Extent of y in {the Extent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D};
hence thesis by A25,SETFAM_1:def 1;
end;
then r@ is-SubConcept-of CP@ by A20,CONLAT_1:def 16;
hence thesis by CONLAT_1:43;
end;
CP is_less_than D
proof
let q be Element of ConceptLattice(C);
assume q in D;
then q@ in D by CONLAT_1:def 21;
then the Extent of q@ in {the Extent of ConceptStr(#E,I#) where E is
Subset of the carrier of C, I is Subset of the carrier' of C : ConceptStr(#E,I
#) in D};
then the Extent of CP@ c= the Extent of q@ by A20,SETFAM_1:3;
then CP@ is-SubConcept-of q@ by CONLAT_1:def 16;
hence thesis by CONLAT_1:43;
end;
hence thesis by A15,A14,A21,LATTICE3:34;
end;
theorem Th9:
for C being FormalContext for CP being strict FormalConcept of C
holds "\/"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex o being Object of C st o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o}}, ConceptLattice(C)) = CP
proof
let C be FormalContext;
let CP be strict FormalConcept of C;
set D = {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex o being Object of C st o in the Extent of CP &
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o}};
A1: for CP9 being Element of ConceptLattice(C) st D is_less_than CP9 holds
@CP [= CP9
proof
let CP9 be Element of ConceptLattice(C);
assume
A2: D is_less_than CP9;
A3: the Extent of CP c= the Extent of (CP9)@
proof
let x be object;
assume
A4: x in the Extent of CP;
then reconsider x as Element of C;
set Ax = (ObjectDerivation(C)).{x};
set Ox = (AttributeDerivation(C)).((ObjectDerivation(C)).{x});
reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C by
CONLAT_1:19;
Cx in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A
is Subset of the carrier' of C : ex o being Object of C st o in the Extent of
CP & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o}} by A4;
then @Cx [= CP9 by A2;
then
A5: (@Cx)@ is-SubConcept-of (CP9)@ by CONLAT_1:43;
{x} c= Ox by CONLAT_1:5;
then
A6: x in the Extent of Cx by ZFMISC_1:31;
Cx = (@Cx)@ by CONLAT_1:def 21;
then the Extent of Cx c= the Extent of (CP9)@ by A5,CONLAT_1:def 16;
hence thesis by A6;
end;
CP = (@CP)@ by CONLAT_1:def 21;
then (@CP)@ is-SubConcept-of (CP9)@ by A3,CONLAT_1:def 16;
hence thesis by CONLAT_1:43;
end;
D is_less_than @CP
proof
let q be Element of ConceptLattice(C);
assume q in D;
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A7: q = ConceptStr(#O,A#) and
A8: ex o being Object of C st o in the Extent of CP & O = (
AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C))
.{o};
consider o being Object of C such that
A9: o in the Extent of CP and
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and
A10: A = (ObjectDerivation(C)).{o} by A8;
A11: {o} c= the Extent of CP by A9,ZFMISC_1:31;
(ObjectDerivation(C)).(the Extent of CP) = the Intent of CP & the
Intent of q@ = (ObjectDerivation(C)).{o} by A7,A10,CONLAT_1:def 10,def 21;
then the Intent of CP c= the Intent of q@ by A11,CONLAT_1:3;
then
A12: q@ is-SubConcept-of CP by CONLAT_1:28;
CP = (@CP)@ by CONLAT_1:def 21;
hence thesis by A12,CONLAT_1:43;
end;
hence thesis by A1,LATTICE3:def 21;
end;
theorem Th10:
for C being FormalContext for CP being strict FormalConcept of C
holds "/\"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of
CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a})}, ConceptLattice(C)) = CP
proof
let C be FormalContext;
let CP be strict FormalConcept of C;
set D = {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of
CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a})};
A1: for CP9 being Element of ConceptLattice(C) st CP9 is_less_than D holds
CP9 [= @CP
proof
let CP9 be Element of ConceptLattice(C);
assume
A2: CP9 is_less_than D;
A3: the Intent of CP c= the Intent of (CP9)@
proof
let x be object;
assume
A4: x in the Intent of CP;
then reconsider x as Element of the carrier' of C;
set Ax = (ObjectDerivation(C)).((AttributeDerivation(C)).{x});
set Ox = (AttributeDerivation(C)).{x};
reconsider Cx = ConceptStr(#Ox,Ax#) as strict FormalConcept of C by
CONLAT_1:21;
Cx in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A
is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent
of CP & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a}) } by A4;
then CP9 [= @Cx by A2;
then
A5: (CP9)@ is-SubConcept-of (@Cx)@ by CONLAT_1:43;
{x} c= Ax by CONLAT_1:6;
then
A6: x in the Intent of Cx by ZFMISC_1:31;
Cx = (@Cx)@ by CONLAT_1:def 21;
then the Intent of Cx c= the Intent of (CP9)@ by A5,CONLAT_1:28;
hence thesis by A6;
end;
CP = (@CP)@ by CONLAT_1:def 21;
then (CP9)@ is-SubConcept-of (@CP)@ by A3,CONLAT_1:28;
hence thesis by CONLAT_1:43;
end;
@CP is_less_than D
proof
let q be Element of ConceptLattice(C);
assume q in D;
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A7: q = ConceptStr(#O,A#) and
A8: ex a being Attribute of C st a in the Intent of CP & O = (
AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C
)).{a});
consider a being Attribute of C such that
A9: a in the Intent of CP and
A10: O = (AttributeDerivation(C)).{a} and
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A8;
A11: {a} c= the Intent of CP by A9,ZFMISC_1:31;
(AttributeDerivation(C)).(the Intent of CP) = the Extent of CP & the
Extent of q@ = (AttributeDerivation(C)).{a} by A7,A10,CONLAT_1:def 10,def 21;
then the Extent of CP c= the Extent of q@ by A11,CONLAT_1:4;
then
A12: CP is-SubConcept-of q@ by CONLAT_1:def 16;
CP = (@CP)@ by CONLAT_1:def 21;
hence thesis by A12,CONLAT_1:43;
end;
hence thesis by A1,LATTICE3:34;
end;
definition
let C be FormalContext;
func gamma(C) -> Function of the carrier of C, the carrier of ConceptLattice
(C) means
:Def4:
for o being Element of C holds ex O being
Subset of the carrier of C, A being Subset of the carrier' of C st it.o =
ConceptStr(#O,A#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) &
A = (ObjectDerivation(C)).{o};
existence
proof
defpred P[object, object] means
ex O being Subset of the carrier of C, A being
Subset of the carrier' of C st $2 = ConceptStr(#O,A#) & O = (
AttributeDerivation(C)).((ObjectDerivation(C)).{$1}) & A = (ObjectDerivation(C)
).{$1};
A1: for e being object st e in the carrier of C
ex u being object st u in the carrier of ConceptLattice(C) & P[e,u]
proof
let e be object;
assume e in the carrier of C;
then reconsider se = {e} as Subset of the carrier of C by ZFMISC_1:31;
set A = (ObjectDerivation(C)).se;
set O = (AttributeDerivation(C)).((ObjectDerivation(C)).se);
take ConceptStr(#O,A#);
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) &
ConceptStr (#O,A#) is FormalConcept of C by CONLAT_1:19,def 20;
hence thesis by CONLAT_1:31;
end;
consider f being Function of the carrier of C, the carrier of
ConceptLattice(C) such that
A2: for e being object st e in the carrier of C holds P[e,f.e] from
FUNCT_2:sch 1(A1);
take f;
let o be Element of C;
thus thesis by A2;
end;
uniqueness
proof
let F1,F2 be Function of the carrier of C,the carrier of ConceptLattice(C);
assume
A3: for o being Element of C holds ex O being Subset of
the carrier of C, A being Subset of the carrier' of C st F1.o = ConceptStr(#O,A
#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o};
assume
A4: for o being Element of C holds ex O being Subset of
the carrier of C, A being Subset of the carrier' of C st F2.o = ConceptStr(#O,A
#) & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o};
A5: for o being object st o in the carrier of C holds F1.o = F2.o
proof
let o be object;
assume o in the carrier of C;
then reconsider o as Element of C;
(ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st F1.o = ConceptStr(#O,A#) & O = (AttributeDerivation(C)) .((
ObjectDerivation(C) ).{o}) & A = (ObjectDerivation(C)).{o} )& ex O9 being
Subset of the carrier of C, A9 being Subset of the carrier' of C st F2.o =
ConceptStr(#O9,A9#) & O9 = (AttributeDerivation( C)).((ObjectDerivation(C)).{o}
) & A9 = (ObjectDerivation (C)).{o} by A3,A4;
hence thesis;
end;
dom F1 = the carrier of C & dom F2 = the carrier of C by FUNCT_2:def 1;
hence thesis by A5;
end;
end;
definition
let C be FormalContext;
func delta(C) -> Function of the carrier' of C, the carrier of
ConceptLattice(C) means
:Def5:
for a being Element of the carrier' of C holds
ex O being Subset of the carrier of C, A being Subset of the carrier' of C st
it.a = ConceptStr(#O,A#) & O = (AttributeDerivation(C)).{a} & A = (
ObjectDerivation(C)).((AttributeDerivation(C)).{a});
existence
proof
defpred P[object, object] means
ex O being Subset of the carrier of C, A being
Subset of the carrier' of C st $2 = ConceptStr(#O,A#) & O = (
AttributeDerivation(C)).{$1} & A = (ObjectDerivation(C)).((AttributeDerivation(
C)).{$1});
A1: for e being object st e in the carrier' of C
ex u being object st u in the carrier of ConceptLattice(C) & P[e,u]
proof
let e be object;
assume e in the carrier' of C;
then reconsider se = {e} as Subset of the carrier' of C by ZFMISC_1:31;
set A = (ObjectDerivation(C)).((AttributeDerivation(C)).se);
set O = (AttributeDerivation(C)).se;
take ConceptStr(#O,A#);
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) &
ConceptStr (#O,A#) is FormalConcept of C by CONLAT_1:21,def 20;
hence thesis by CONLAT_1:31;
end;
consider f being Function of the carrier' of C, the carrier of
ConceptLattice(C) such that
A2: for e being object st e in the carrier' of C holds P[e,f.e] from
FUNCT_2:sch 1(A1);
take f;
let o be Element of the carrier' of C;
thus thesis by A2;
end;
uniqueness
proof
let F1,F2 be Function of the carrier' of C,the carrier of ConceptLattice(C
);
assume
A3: for a being Element of the carrier' of C holds ex O being Subset
of the carrier of C, A being Subset of the carrier' of C st F1.a = ConceptStr(#
O,A#) & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a});
assume
A4: for a being Element of the carrier' of C holds ex O being Subset
of the carrier of C, A being Subset of the carrier' of C st F2.a = ConceptStr(#
O,A#) & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a});
A5: for a being object st a in the carrier' of C holds F1.a = F2.a
proof
let a be object;
assume a in the carrier' of C;
then reconsider a as Element of the carrier' of C;
(ex O being Subset of the carrier of C, A being Subset of the
carrier' of C st F1.a = ConceptStr(#O,A#) & O = (AttributeDerivation(C)) .{a} &
A = ( ObjectDerivation(C)).((AttributeDerivation(C)).{a}) )& ex O9 being Subset
of the carrier of C, A9 being Subset of the carrier' of C st F2.a = ConceptStr
(# O9,A9#) & O9 = (AttributeDerivation( C)).{a} & A9 = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a}) by A3,A4;
hence thesis;
end;
dom F1 = the carrier' of C & dom F2 = the carrier' of C by FUNCT_2:def 1;
hence thesis by A5;
end;
end;
theorem
for C being FormalContext for o being Object of C for a being
Attribute of C holds (gamma(C)).o is FormalConcept of C & (delta(C)).a is
FormalConcept of C
proof
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
hence thesis by CONLAT_1:def 15;
end;
theorem Th12:
for C being FormalContext holds rng(gamma(C)) is supremum-dense
& rng(delta(C)) is infimum-dense
proof
let C be FormalContext;
set G = rng(gamma(C));
thus G is supremum-dense
proof
let a be Element of ConceptLattice(C);
A1: {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset
of the carrier' of C : ex o being Object of C st o in the Extent of a@ & O = (
AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C))
.{o}} c= G
proof
let x be object;
assume x in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A
is Subset of the carrier' of C : ex o being Object of C st o in the Extent of a
@ & O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)).{o}};
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A2: x = ConceptStr(#O,A#) and
A3: ex o being Object of C st o in the Extent of a@ & O = (
AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (ObjectDerivation(C))
.{o};
consider o being Object of C such that
o in the Extent of a@ and
O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and
A4: A = (ObjectDerivation(C)).{o} by A3;
consider y being Element of ConceptLattice(C) such that
A5: (gamma(C)).o = y;
dom(gamma(C)) = the carrier of C & ex O9 being Subset of the carrier
of C, A9 being Subset of the carrier' of C st y = ConceptStr(#O9,A9#) & O9 = (
AttributeDerivation(C)) .((ObjectDerivation(C)).{o}) & A9 = (ObjectDerivation(
C)).{o} by A5,Def4,FUNCT_2:def 1;
hence thesis by A2,A3,A4,A5,FUNCT_1:def 3;
end;
"\/"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex o being Object of C st o in the Extent of a@ &
O = ( AttributeDerivation(C)).((ObjectDerivation(C)).{o}) & A = (
ObjectDerivation(C)) .{o}}, ConceptLattice(C)) = a@ & a = a@ by Th9,
CONLAT_1:def 21;
hence thesis by A1;
end;
let b be Element of ConceptLattice(C);
set G = rng(delta(C));
A6: {ConceptStr(#O,A#) where O is Subset of the carrier of C, A is Subset of
the carrier' of C : ex a being Attribute of C st a in the Intent of b@ & O = (
AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C
)).{a})} c= G
proof
let x be object;
assume x in {ConceptStr(#O,A#) where O is Subset of the carrier of C, A
is Subset of the carrier' of C : ex a being Attribute of C st a in the Intent
of b@ & O = (AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a})};
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A7: x = ConceptStr(#O,A#) and
A8: ex a being Attribute of C st a in the Intent of b@ & O = (
AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((AttributeDerivation(C
)).{a});
consider a being Attribute of C such that
a in the Intent of b@ and
A9: O = (AttributeDerivation(C)).{a} and
A = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by A8;
consider y being Element of ConceptLattice(C) such that
A10: (delta(C)).a = y;
dom(delta(C)) = the carrier' of C & ex O9 being Subset of the carrier
of C, A9 being Subset of the carrier' of C st y = ConceptStr(#O9,A9#) & O9 = (
AttributeDerivation(C)) .{a} & A9 = (ObjectDerivation(C)).((
AttributeDerivation(C)).{a}) by A10,Def5,FUNCT_2:def 1;
hence thesis by A7,A8,A9,A10,FUNCT_1:def 3;
end;
"/\"({ConceptStr(#O,A#) where O is Subset of the carrier of C, A is
Subset of the carrier' of C : ex a being Attribute of C st a in the Intent of b
@ & O = ( AttributeDerivation(C)).{a} & A = (ObjectDerivation(C)).((
AttributeDerivation(C )).{a})}, ConceptLattice(C)) = b@ & b = b@ by Th10,
CONLAT_1:def 21;
hence thesis by A6;
end;
theorem Th13:
for C being FormalContext for o being Object of C for a being
Attribute of C holds o is-connected-with a iff (gamma(C)).o [= (delta(C)).a
proof
let C be FormalContext;
let o be Object of C;
let a be Attribute of C;
set aa = {a};
set o9 = {o};
set oo = (AttributeDerivation(C)).((ObjectDerivation(C)).{o});
consider O being Subset of the carrier of C, A being Subset of the carrier'
of C such that
A1: (gamma(C)).o = ConceptStr(#O,A#) and
A2: O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and
A = (ObjectDerivation(C)).{o} by Def4;
hereby
assume o is-connected-with a;
then a in {a9 where a9 is Attribute of C : o is-connected-with a9};
then a in (ObjectDerivation(C)).({o}) by CONLAT_1:1;
then
A3: {a} c= (ObjectDerivation(C)).({o}) by ZFMISC_1:31;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A4: (gamma(C)).o = ConceptStr(#O,A#) and
A5: O = (AttributeDerivation(C)).((ObjectDerivation(C)).{o}) and
A = (ObjectDerivation(C)).{o} by Def4;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A6: (delta(C)).a = ConceptStr(#O9,A9#) and
A7: O9 = (AttributeDerivation(C)).{a} and
A9 = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5;
A8: the Extent of ((delta(C)).a)@ = O9 by A6,CONLAT_1:def 21;
the Extent of ((gamma(C)).o)@ = O by A4,CONLAT_1:def 21;
then
the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@ by A3,A5,A7
,A8,CONLAT_1:4;
then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:def 16;
hence ((gamma(C)).o) [= ((delta(C)).a) by CONLAT_1:43;
end;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A9: (delta(C)).a = ConceptStr(#O9,A9#) and
A10: O9 = (AttributeDerivation(C)).{a} and
A9 = (ObjectDerivation(C)).((AttributeDerivation(C)).{a}) by Def5;
assume ((gamma(C)).o) [= ((delta(C)).a);
then ((gamma(C)).o)@ is-SubConcept-of ((delta(C)).a)@ by CONLAT_1:43;
then
A11: the Extent of ((gamma(C)).o)@ c= the Extent of ((delta(C)).a)@ by
CONLAT_1:def 16;
the Extent of ((delta(C)).a)@ = O9 by A9,CONLAT_1:def 21;
then O c= O9 by A11,A1,CONLAT_1:def 21;
then aa c= (ObjectDerivation(C)).oo by A2,A10,CONLAT_1:11;
then {a} c= (ObjectDerivation(C)).o9 by CONLAT_1:7;
then a in (ObjectDerivation(C)).({o}) by ZFMISC_1:31;
then a in {a9 where a9 is Attribute of C : o is-connected-with a9} by
CONLAT_1:1;
then ex b being Attribute of C st b = a & o is-connected-with b;
hence thesis;
end;
begin :: The Characterization
Lm1: for L1,L2 being Lattice for f being Function of the carrier of L1, the
carrier of L2 holds (for a,b being Element of L1 holds f.a [= f.b implies a [=
b) implies f is one-to-one
proof
let L1,L2 be Lattice;
let f be Function of the carrier of L1, the carrier of L2;
assume
A1: for a,b being Element of L1 holds f.a [= f.b implies a [= b;
let x,y be object;
assume that
A2: x in dom f and
A3: y in dom f and
A4: f.x = f.y;
reconsider y as Element of L1 by A3;
reconsider x as Element of L1 by A2;
x [= y & y [= x by A1,A4;
hence thesis by LATTICES:8;
end;
Lm2: for L1,L2 being complete Lattice for f being Function of the carrier of
L1, the carrier of L2 st f is one-to-one & rng f = the carrier of L2 holds (for
a,b being Element of L1 holds a [= b iff f.a [= f.b) implies f is Homomorphism
of L1,L2
proof
let L1,L2 be complete Lattice;
let f be Function of the carrier of L1, the carrier of L2;
assume
A1: f is one-to-one & rng f = the carrier of L2;
assume
A2: for a,b being Element of L1 holds a [= b iff f.a [= f.b;
A3: for a,b being Element of L1 holds f.(a "/\" b) = f.a "/\" f.b
proof
let a,b be Element of L1;
a "/\" b [= b by LATTICES:6;
then
A4: f.(a "/\" b) [= f.b by A2;
A5: for r being Element of L2 st r is_less_than {f.a,f.b} holds r [= f.(a
"/\" b)
proof
reconsider g = f" as Function of the carrier of L2, the carrier of L1 by
A1,FUNCT_2:25;
let r be Element of L2;
assume
A6: r is_less_than {f.a,f.b};
A7: f.(g.r) = r by A1,FUNCT_1:35;
f.b in {f.a,f.b} by TARSKI:def 2;
then r [= f.b by A6;
then
A8: g.r [= b by A2,A7;
f.a in {f.a,f.b} by TARSKI:def 2;
then r [= f.a by A6;
then g.r [= a by A2,A7;
then for q being Element of L1 st q in {a,b} holds g.r [= q by A8,
TARSKI:def 2;
then
A9: g.r is_less_than {a,b};
a "/\" b = "/\"{a,b} by LATTICE3:43;
then g.r [= a "/\" b by A9,LATTICE3:34;
hence thesis by A2,A7;
end;
a "/\" b [= a by LATTICES:6;
then f.(a "/\" b) [= f.a by A2;
then for q being Element of L2 st q in {f.a,f.b} holds f.(a "/\" b) [= q
by A4,TARSKI:def 2;
then f.(a "/\" b) is_less_than {f.a,f.b};
then f.(a "/\" b) = "/\"({f.a,f.b},L2) by A5,LATTICE3:34;
hence thesis by LATTICE3:43;
end;
for a,b being Element of L1 holds f.(a "\/" b) = f.a "\/" f.b
proof
let a,b be Element of L1;
b [= a "\/" b by LATTICES:5;
then
A10: f.b [= f.(a "\/" b) by A2;
A11: for r being Element of L2 st {f.a,f.b} is_less_than r holds f.(a "\/"
b) [= r
proof
reconsider g = f" as Function of the carrier of L2, the carrier of L1 by
A1,FUNCT_2:25;
let r be Element of L2;
assume
A12: {f.a,f.b} is_less_than r;
A13: f.(g.r) = r by A1,FUNCT_1:35;
f.b in {f.a,f.b} by TARSKI:def 2;
then f.b [= r by A12;
then
A14: b [= g.r by A2,A13;
f.a in {f.a,f.b} by TARSKI:def 2;
then f.a [= r by A12;
then a [= g.r by A2,A13;
then for q being Element of L1 st q in {a,b} holds q [= g.r by A14,
TARSKI:def 2;
then
A15: {a,b} is_less_than g.r;
a "\/" b = "\/"{a,b} by LATTICE3:43;
then a "\/" b [= g.r by A15,LATTICE3:def 21;
hence thesis by A2,A13;
end;
a [= a "\/" b by LATTICES:5;
then f.a [= f.(a "\/" b) by A2;
then
for q being Element of L2 st q in {f.a,f.b} holds q [= f.(a "\/" b) by A10,
TARSKI:def 2;
then {f.a,f.b} is_less_than f.(a "\/" b);
then f.(a "\/" b) = "\/"({f.a,f.b},L2) by A11,LATTICE3:def 21;
hence thesis by LATTICE3:43;
end;
then f is "\/"-preserving "/\"-preserving by A3,LATTICE4:def 1,def 2;
hence thesis;
end;
Lm3: 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;
per cases;
suppose
the Extent of CS is empty;
then the Intent of CS = the carrier' of C by A1,CONLAT_1:17;
hence thesis by CONLAT_1:def 8;
end;
suppose
the Extent of CS is non empty;
hence thesis by CONLAT_1:def 8;
end;
end;
theorem Th14:
for L being complete Lattice for C being FormalContext holds
ConceptLattice(C),L are_isomorphic iff ex g being Function of the carrier of C,
the carrier of L, d being Function of the carrier' of C, the carrier of L st
rng(g) is supremum-dense & rng(d) is infimum-dense & for o being Object of C, a
being Attribute of C holds o is-connected-with a iff g.o [= d.a
proof
let L be complete Lattice;
let C be FormalContext;
hereby
assume ConceptLattice(C),L are_isomorphic;
then consider f being Homomorphism of ConceptLattice(C),L such that
A1: f is bijective by LATTICE4:def 3;
take g = f * gamma(C), d = f * delta(C);
thus rng(g) is supremum-dense
proof
let a be Element of L;
consider b being Element of ConceptLattice(C) such that
A2: a = f.b by A1,LATTICE4:6;
rng(gamma(C)) is supremum-dense by Th12;
then consider D9 being Subset of rng(gamma(C)) such that
A3: b = "\/"(D9,ConceptLattice(C));
set D = {f.x where x is Element of ConceptLattice(C) : x in D9};
A4: for r being Element of L st D is_less_than r holds a [= r
proof
let r be Element of L;
consider r9 being Element of ConceptLattice(C) such that
A5: r = f.r9 by A1,LATTICE4:6;
reconsider r9 as Element of ConceptLattice(C);
assume
A6: D is_less_than r;
for q being Element of ConceptLattice(C) st q in D9 holds q [= r9
proof
let q be Element of ConceptLattice(C);
assume q in D9;
then f.q in {f.x where x is Element of ConceptLattice(C) : x in D9};
then f.q [= f.r9 by A6,A5;
hence thesis by A1,LATTICE4:5;
end;
then D9 is_less_than r9;
then b [= r9 by A3,LATTICE3:def 21;
hence thesis by A1,A2,A5,LATTICE4:5;
end;
A7: D c= rng(g)
proof
let x be object;
assume x in D;
then consider x9 being Element of ConceptLattice(C) such that
A8: x = f.x9 and
A9: x9 in D9;
consider y being object such that
A10: y in dom(gamma(C)) & (gamma(C)).y = x9 by A9,FUNCT_1:def 3;
dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
then
A11: y in dom(f * (gamma(C))) by A10,FUNCT_1:11;
x = (f * (gamma(C))).y by A8,A10,FUNCT_1:13;
hence thesis by A11,FUNCT_1:def 3;
end;
A12: D9 is_less_than b by A3,LATTICE3:def 21;
D is_less_than a
proof
let q be Element of L;
assume q in D;
then consider q9 being Element of ConceptLattice(C) such that
A13: q = f.q9 and
A14: q9 in D9;
q9 [= b by A12,A14;
hence thesis by A1,A2,A13,LATTICE4:5;
end;
then a = "\/"(D,L) by A4,LATTICE3:def 21;
hence thesis by A7;
end;
thus rng(d) is infimum-dense
proof
let a be Element of L;
consider b being Element of ConceptLattice(C) such that
A15: a = f.b by A1,LATTICE4:6;
rng(delta(C)) is infimum-dense by Th12;
then consider D9 being Subset of rng(delta(C)) such that
A16: b = "/\"(D9,ConceptLattice(C));
set D = {f.x where x is Element of ConceptLattice(C) : x in D9};
A17: for r being Element of L st r is_less_than D holds r [= a
proof
let r be Element of L;
consider r9 being Element of ConceptLattice(C) such that
A18: r = f.r9 by A1,LATTICE4:6;
reconsider r9 as Element of ConceptLattice(C);
assume
A19: r is_less_than D;
r9 is_less_than D9
proof
let q be Element of ConceptLattice(C);
assume q in D9;
then f.q in {f.x where x is Element of ConceptLattice(C) : x in D9};
then f.r9 [= f.q by A19,A18;
hence thesis by A1,LATTICE4:5;
end;
then r9 [= b by A16,LATTICE3:34;
hence thesis by A1,A15,A18,LATTICE4:5;
end;
A20: D c= rng(d)
proof
let x be object;
assume x in D;
then consider x9 being Element of ConceptLattice(C) such that
A21: x = f.x9 and
A22: x9 in D9;
consider y being object such that
A23: y in dom(delta(C)) & (delta(C)).y = x9 by A22,FUNCT_1:def 3;
dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
then
A24: y in dom(f * (delta(C))) by A23,FUNCT_1:11;
x = (f * (delta(C))).y by A21,A23,FUNCT_1:13;
hence thesis by A24,FUNCT_1:def 3;
end;
A25: b is_less_than D9 by A16,LATTICE3:34;
a is_less_than D
proof
let q be Element of L;
assume q in D;
then consider q9 being Element of ConceptLattice(C) such that
A26: q = f.q9 and
A27: q9 in D9;
b [= q9 by A25,A27;
hence thesis by A1,A15,A26,LATTICE4:5;
end;
then a = "/\"(D,L) by A17,LATTICE3:34;
hence thesis by A20;
end;
let o be Object of C, a be Attribute of C;
A28: o is-connected-with a iff (gamma(C)).o [= (delta(C)).a by Th13;
hereby
dom(delta(C)) = the carrier' of C by FUNCT_2:def 1;
then
A29: f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:13;
dom(gamma(C)) = the carrier of C by FUNCT_2:def 1;
then
A30: f.((gamma(C)).o) = (f * (gamma(C))).o by FUNCT_1:13;
assume o is-connected-with a;
hence g.o [= d.a by A1,A28,A30,A29,LATTICE4:5;
end;
dom(gamma(C)) = the carrier of C by FUNCT_2:def 1;
then
A31: f.((gamma(C)).o) = (f * (gamma(C))).o by FUNCT_1:13;
dom(delta(C)) = the carrier' of C by FUNCT_2:def 1;
then
A32: f.((delta(C)).a) = (f * (delta(C))).a by FUNCT_1:13;
assume g.o [= d.a;
then (gamma(C)).o [= (delta(C)).a by A1,A31,A32,LATTICE4:5;
hence o is-connected-with a by Th13;
end;
given g being Function of the carrier of C, the carrier of L, d being
Function of the carrier' of C, the carrier of L such that
A33: rng(g) is supremum-dense and
A34: rng(d) is infimum-dense and
A35: for o being Object of C, a being Attribute of C holds o
is-connected-with a iff g.o [= d.a;
set fi = {[x,ConceptStr(#O,A#)] where x is Element of L, O is Subset of the
carrier of C, A is Subset of the carrier' of C : O = {o where o is Object of C
: g.o [= x} & A = {a where a is Attribute of C : x [= d.a} };
set f = {[ConceptStr(#O,A#),x] where O is Subset of the carrier of C, A is
Subset of the carrier' of C, x is Element of L : ConceptStr(#O,A#) is
FormalConcept of C & x = "\/"({g.o where o is Object of C : o in O},L) };
A36: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
A37: f c= [:the carrier of ConceptLattice(C), the carrier of L:]
proof
let y be object;
assume y in f;
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C, x being Element of L such that
A38: y = [ConceptStr(#O,A#),x] and
A39: ConceptStr(#O,A#) is FormalConcept of C and
x = "\/"({g.o where o is Object of C : o in O},L);
ConceptStr(#O,A#) in the carrier of ConceptLattice(C) by A36,A39,
CONLAT_1:31;
hence thesis by A38,ZFMISC_1:def 2;
end;
fi c= [:the carrier of L, the carrier of ConceptLattice(C):]
proof
let y be object;
assume y in fi;
then consider
x being Element of L, O being Subset of the carrier of C, A being
Subset of the carrier' of C such that
A40: y = [x,ConceptStr(#O,A#)] and
A41: O = {o where o is Object of C : g.o [= x} and
A42: A = {a where a is Attribute of C : x [= d.a};
A43: (AttributeDerivation(C)).(the Intent of ConceptStr(#O,A#)) = the
Extent of ConceptStr(#O,A#)
proof
thus (AttributeDerivation(C)). (the Intent of ConceptStr(#O,A#)) c= the
Extent of ConceptStr(#O,A#)
proof
let u be object;
A44: "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) = x
proof
consider D being Subset of rng(d) such that
A45: "/\"(D,L) = x by A34;
A46: x is_less_than D by A45,LATTICE3:34;
D c= {d.a9 where a9 is Attribute of C : x [= d.a9}
proof
let u be object;
assume
A47: u in D;
then consider v being object such that
A48: v in dom d and
A49: u = d.v by FUNCT_1:def 3;
reconsider v as Attribute of C by A48;
x [= d.v by A46,A47,A49;
hence thesis by A49;
end;
then
A50: "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) [= x by A45,
LATTICE3:45;
x is_less_than {d.a9 where a9 is Attribute of C : x [= d.a9}
proof
let u be Element of L;
assume u in {d.a9 where a9 is Attribute of C : x [= d.a9};
then ex v being Attribute of C st u = d.v & x [= d.v;
hence thesis;
end;
then x [= "/\"({d.a9 where a9 is Attribute of C : x [= d.a9},L) by
LATTICE3:39;
hence thesis by A50,LATTICES:8;
end;
assume
u in (AttributeDerivation(C)).(the Intent of ConceptStr(#O,A #));
then u in { o where o is Object of C : for a being Attribute of C st
a in the Intent of ConceptStr(#O,A#) holds o is-connected-with a } by
CONLAT_1:def 4;
then consider u9 being Object of C such that
A51: u9 = u and
A52: for a being Attribute of C st a in the Intent of ConceptStr
(#O,A#) holds u9 is-connected-with a;
A53: for v being Attribute of C st v in {a where a is Attribute of C:
x [= d.a} holds g.u9 [= d.v by A35,A42,A52;
g.u9 is_less_than {d.a where a is Attribute of C: x [= d.a}
proof
let q be Element of L;
assume q in {d.a where a is Attribute of C: x [= d.a};
then consider b being Attribute of C such that
A54: q = d.b and
A55: x [= d.b;
b in {a where a is Attribute of C: x [= d.a} by A55;
hence thesis by A53,A54;
end;
then g.u9 [= x by A44,LATTICE3:34;
hence thesis by A41,A51;
end;
let u be object;
assume u in the Extent of ConceptStr(#O,A#);
then consider u9 being Object of C such that
A56: u9 = u and
A57: g.u9 [= x by A41;
A58: for v being Attribute of C st v in {a where a is Attribute of C: x
[= d.a} holds g.u9 [= d.v
proof
let v be Attribute of C;
assume v in {a where a is Attribute of C : x [= d.a};
then ex v9 being Attribute of C st v9 = v & x [= d.v9;
hence thesis by A57,LATTICES:7;
end;
for v being Attribute of C st v in {a where a is Attribute of C: x
[= d.a} holds u9 is-connected-with v
proof
let v be Attribute of C;
assume v in {a where a is Attribute of C : x [= d.a};
then g.u9 [= d.v by A58;
hence thesis by A35;
end;
then u9 in {o where o is Object of C : for a being Attribute of C st a
in the Intent of ConceptStr(#O,A#) holds o is-connected-with a } by A42;
hence thesis by A56,CONLAT_1:def 4;
end;
(ObjectDerivation(C)).(the Extent of ConceptStr(#O,A#)) = the Intent
of ConceptStr(#O,A#)
proof
thus (ObjectDerivation(C)). (the Extent of ConceptStr(#O,A#)) c= the
Intent of ConceptStr(#O,A#)
proof
let u be object;
A59: "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L) = x
proof
consider D being Subset of rng(g) such that
A60: "\/"(D,L) = x by A33;
A61: D is_less_than x by A60,LATTICE3:def 21;
D c= {g.a9 where a9 is Object of C : g.a9 [= x}
proof
let u be object;
assume
A62: u in D;
then consider v being object such that
A63: v in dom g and
A64: u = g.v by FUNCT_1:def 3;
reconsider v as Object of C by A63;
g.v [= x by A61,A62,A64;
hence thesis by A64;
end;
then
A65: x [= "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L ) by A60,
LATTICE3:45;
{g.a9 where a9 is Object of C : g.a9 [= x} is_less_than x
proof
let u be Element of L;
assume u in {g.a9 where a9 is Object of C : g.a9 [= x};
then ex v being Object of C st u = g.v & g.v [= x;
hence thesis;
end;
then "\/"({g.a9 where a9 is Object of C : g.a9 [= x},L) [= x by
LATTICE3:def 21;
hence thesis by A65,LATTICES:8;
end;
assume u in (ObjectDerivation(C)).(the Extent of ConceptStr(#O,A#));
then u in { o where o is Attribute of C : for a being Object of C st
a in the Extent of ConceptStr(#O,A#) holds a is-connected-with o } by
CONLAT_1:def 3;
then consider u9 being Attribute of C such that
A66: u9 = u and
A67: for a being Object of C st a in the Extent of ConceptStr(#O,
A#) holds a is-connected-with u9;
A68: for v being Object of C st v in {a where a is Object of C: g.a
[= x} holds g.v [= d.u9 by A35,A41,A67;
{g.a where a is Object of C: g.a [= x} is_less_than d.u9
proof
let q be Element of L;
assume q in {g.a where a is Object of C: g.a [= x};
then consider b being Object of C such that
A69: q = g.b and
A70: g.b [= x;
b in {a where a is Object of C: g.a [= x} by A70;
hence thesis by A68,A69;
end;
then x [= d.u9 by A59,LATTICE3:def 21;
hence thesis by A42,A66;
end;
let u be object;
assume u in the Intent of ConceptStr(#O,A#);
then consider u9 being Attribute of C such that
A71: u9 = u and
A72: x [= d.u9 by A42;
A73: for v being Object of C st v in {a where a is Object of C: g.a [=
x} holds g.v [= d.u9
proof
let v be Object of C;
assume v in {a where a is Object of C : g.a [= x};
then ex v9 being Object of C st v9 = v & g.v9 [= x;
hence thesis by A72,LATTICES:7;
end;
for v being Object of C st v in {a where a is Object of C : g.a [=
x} holds v is-connected-with u9
proof
let v be Object of C;
assume v in {a where a is Object of C : g.a [= x};
then g.v [= d.u9 by A73;
hence thesis by A35;
end;
then u9 in {o where o is Attribute of C : for a being Object of C st a
in the Extent of ConceptStr(#O,A#) holds a is-connected-with o } by A41;
hence thesis by A71,CONLAT_1:def 3;
end;
then ConceptStr(#O,A#) is FormalConcept of C by A43,Lm3,CONLAT_1:def 10;
then ConceptStr(#O,A#) in the carrier of ConceptLattice(C) by A36,
CONLAT_1:31;
hence thesis by A40,ZFMISC_1:def 2;
end;
then reconsider
fi as Relation of the carrier of L, the carrier of ConceptLattice
(C);
A74: for x,y1,y2 being object st [x,y1] in fi & [x,y2] in fi holds y1 = y2
proof
let x,y1,y2 be object;
assume that
A75: [x,y1] in fi and
A76: [x,y2] in fi;
consider z being Element of L, O being Subset of the carrier of C, A being
Subset of the carrier' of C such that
A77: [x,y1] = [z,ConceptStr(#O,A#)] and
A78: O = {o where o is Object of C : g.o [= z} & A = {a where a is
Attribute of C : z [= d.a} by A75;
consider z9 being Element of L, O9 being Subset of the carrier of C, A9
being Subset of the carrier' of C such that
A79: [x,y2] = [z9,ConceptStr(#O9,A9#)] and
A80: O9 = {o where o is Object of C : g.o [= z9} & A9 = {a where a is
Attribute of C : z9 [= d.a} by A76;
A81: z = x by A77,XTUPLE_0:1
.= z9 by A79,XTUPLE_0:1;
thus y1 = [x,y1]`2
.= [x,y2]`2 by A77,A78,A79,A80,A81
.= y2;
end;
the carrier of L c= dom fi
proof
let y be object;
assume y in the carrier of L;
then reconsider y as Element of L;
set A = {a where a is Attribute of C : y [= d.a};
A c= the carrier' of C
proof
let u be object;
assume u in A;
then ex u9 being Attribute of C st u9 = u & y [= d.u9;
hence thesis;
end;
then reconsider A as Subset of the carrier' of C;
set O = {o where o is Object of C : g.o [= y};
O c= the carrier of C
proof
let u be object;
assume u in O;
then ex u9 being Object of C st u9 = u & g.u9 [= y;
hence thesis;
end;
then reconsider O as Subset of the carrier of C;
[y,ConceptStr(#O,A#)] in fi;
hence thesis by XTUPLE_0:def 12;
end;
then
A82: the carrier of L = dom fi;
reconsider f as Relation of the carrier of ConceptLattice(C), the carrier of
L by A37;
the carrier of ConceptLattice(C) c= dom f
proof
let y be object;
assume y in the carrier of ConceptLattice(C);
then
A83: y is strict FormalConcept of C by A36,CONLAT_1:31;
then consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A84: y = ConceptStr(#O9,A9#);
reconsider z = "\/"({g.o where o is Object of C : o in O9},L) as Element
of L;
[y,z] in f by A83,A84;
hence thesis by XTUPLE_0:def 12;
end;
then
A85: the carrier of ConceptLattice(C) = dom f;
reconsider fi as Function of the carrier of L, the carrier of ConceptLattice
(C) by A82,A74,FUNCT_1:def 1,FUNCT_2:def 1;
for x,y1,y2 being object st [x,y1] in f & [x,y2] in f holds y1 = y2
proof
let x,y1,y2 be object;
assume that
A86: [x,y1] in f and
A87: [x,y2] in f;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C, z being Element of L such that
A88: [x,y1] = [ConceptStr(#O,A#),z] and
ConceptStr(#O,A#) is FormalConcept of C and
A89: z = "\/"({g.o where o is Object of C : o in O},L) by A86;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C, z9 being Element of L such that
A90: [x,y2] = [ConceptStr(#O9,A9#),z9] and
ConceptStr(#O9,A9#) is FormalConcept of C and
A91: z9 = "\/"({g.o where o is Object of C : o in O9},L) by A87;
A92: ConceptStr(#O,A#) = [ConceptStr(#O,A#),z]`1
.= [x,y1]`1 by A88
.= x
.= [x,y2]`1
.= [ConceptStr(#O9,A9#),z9]`1 by A90
.= ConceptStr(#O9,A9#);
thus y1 = [x,y1]`2
.= [x,y2]`2 by A88,A89,A90,A91,A92
.= y2;
end;
then reconsider
f as Function of the carrier of ConceptLattice(C), the carrier of
L by A85,FUNCT_1:def 1,FUNCT_2:def 1;
A93: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
A94: for a being Element of L holds f.(fi.a) = a
proof
let a be Element of L;
reconsider a as Element of L;
set A = {a9 where a9 is Attribute of C : a [= d.a9};
A c= the carrier' of C
proof
let u be object;
assume u in A;
then ex u9 being Attribute of C st u9 = u & a [= d.u9;
hence thesis;
end;
then reconsider A as Subset of the carrier' of C;
set O = {o where o is Object of C : g.o [= a};
O c= the carrier of C
proof
let u be object;
assume u in O;
then ex u9 being Object of C st u9 = u & g.u9 [= a;
hence thesis;
end;
then reconsider O as Subset of the carrier of C;
set b = "\/"({g.o where o is Object of C : o in the Extent of ConceptStr(#
O,A#)},L);
A95: "\/"({g.o where o is Object of C : o in {o9 where o9 is Object of C
: g.o9 [= a}},L) = a
proof
consider D being Subset of rng(g) such that
A96: "\/"(D,L) = a by A33;
A97: D is_less_than a by A96,LATTICE3:def 21;
D c= {g.o where o is Object of C : o in {o9 where o9 is Object of
C: g.o9 [= a}}
proof
let u be object;
assume
A98: u in D;
then consider v being object such that
A99: v in dom g and
A100: u = g.v by FUNCT_1:def 3;
reconsider v as Object of C by A99;
g.v [= a by A97,A98,A100;
then v in {o9 where o9 is Object of C : g.o9 [= a};
hence thesis by A100;
end;
then
A101: a [= "\/"({g.o where o is Object of C : o in {o9 where o9 is
Object of C : g.o9 [= a}},L) by A96,LATTICE3:45;
{g.o where o is Object of C : o in {o9 where o9 is Object of C : g
.o9 [= a}} is_less_than a
proof
let u be Element of L;
assume u in {g.o where o is Object of C : o in {o9 where o9 is
Object of C : g.o9 [= a}};
then consider v being Object of C such that
A102: u = g.v and
A103: v in {o9 where o9 is Object of C : g.o9 [= a};
ex ov being Object of C st ov = v & g.ov [= a by A103;
hence thesis by A102;
end;
then "\/"({g.o where o is Object of C : o in {o9 where o9 is Object of
C: g.o9 [= a}},L) [= a by LATTICE3:def 21;
hence thesis by A101,LATTICES:8;
end;
A104: [a,ConceptStr(#O,A#)] in fi;
then ConceptStr(#O,A#) in rng(fi) by XTUPLE_0:def 13;
then ConceptStr(#O,A#) is FormalConcept of C by A93,CONLAT_1:31;
then [ConceptStr(#O,A#),b] in f;
then f.ConceptStr(#O,A#) = b by FUNCT_1:1;
hence thesis by A104,A95,FUNCT_1:1;
end;
the carrier of L c= rng f
proof
let u be object;
A105: dom f = the carrier of ConceptLattice(C) by FUNCT_2:def 1;
assume
A106: u in the carrier of L;
then u in dom fi by FUNCT_2:def 1;
then consider v being object such that
A107: [u,v] in fi by XTUPLE_0:def 12;
reconsider u as Element of L by A106;
v in rng fi by A107,XTUPLE_0:def 13;
then reconsider v as Element of ConceptLattice(C);
f.v = f.(fi.u) by A107,FUNCT_1:1
.= u by A94;
hence thesis by A105,FUNCT_1:def 3;
end;
then
A108: rng f = the carrier of L;
A109: for x being Element of ConceptLattice(C) holds f.x = "/\"({d.a where a
is Attribute of C : a in the Intent of x@},L)
proof
let x be Element of ConceptLattice(C);
set y = "\/"({g.o where o is Object of C : o in the Extent of x@},L);
A110: [x@, y] in f;
A111: for o being object holds o in {d.a9 where a9 is Attribute of C : y [= d
.a9} implies o in {d.a where a is Attribute of C : a in the Intent of x@}
proof
let o be object;
assume o in {d.a9 where a9 is Attribute of C : y [= d.a9};
then consider u being Attribute of C such that
A112: o = d.u and
A113: y [= d.u;
A114: for o being Object of C st o in the Extent of x@ holds g.o [= d.u
proof
let o be Object of C;
assume o in the Extent of x@;
then g.o in {g.o9 where o9 is Object of C : o9 in the Extent of x @};
then g.o [= y by LATTICE3:38;
hence thesis by A113,LATTICES:7;
end;
for o being Object of C st o in the Extent of x@ holds o
is-connected-with u
proof
let o be Object of C;
assume o in the Extent of x@;
then g.o [= d.u by A114;
hence thesis by A35;
end;
then u in {a9 where a9 is Attribute of C : for o9 being Object of C st
o9 in the Extent of x@ holds o9 is-connected-with a9};
then u in (ObjectDerivation(C)).(the Extent of x@) by CONLAT_1:def 3;
then u in the Intent of x@ by CONLAT_1:def 10;
hence thesis by A112;
end;
A115: for o9 being Object of C st o9 in the Extent of x@ for a9 being
Attribute of C st a9 in the Intent of x@ holds g.o9 [= d.a9
proof
let o9 be Object of C;
assume
A116: o9 in the Extent of x@;
let a9 be Attribute of C;
assume a9 in the Intent of x@;
then a9 in (ObjectDerivation(C)).(the Extent of x@) by CONLAT_1:def 10;
then a9 in {a where a is Attribute of C : for o being Object of C st o
in the Extent of x@ holds o is-connected-with a } by CONLAT_1:def 3;
then ex aa being Attribute of C st aa = a9 & for o being Object of C st
o in the Extent of x@ holds o is-connected-with aa;
then o9 is-connected-with a9 by A116;
hence thesis by A35;
end;
A117: for o being object holds o in {d.a where a is Attribute of C : a in the
Intent of x@} implies o in {d.a9 where a9 is Attribute of C : y [= d.a9}
proof
let o be object;
assume o in {d.a where a is Attribute of C : a in the Intent of x@};
then consider b being Attribute of C such that
A118: o = d.b and
A119: b in the Intent of x@;
{g.o9 where o9 is Object of C : o9 in the Extent of x@} is_less_than d.b
proof
let q be Element of L;
assume q in {g.o9 where o9 is Object of C : o9 in the Extent of x@};
then ex u being Object of C st q = g.u & u in the Extent of x @;
hence thesis by A115,A119;
end;
then y [= d.b by LATTICE3:def 21;
hence thesis by A118;
end;
A120: "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) = y
proof
consider D being Subset of rng(d) such that
A121: "/\"(D,L) = y by A34;
A122: y is_less_than D by A121,LATTICE3:34;
D c= {d.a9 where a9 is Attribute of C : y [= d.a9}
proof
let u be object;
assume
A123: u in D;
then consider v being object such that
A124: v in dom d and
A125: u = d.v by FUNCT_1:def 3;
reconsider v as Attribute of C by A124;
y [= d.v by A122,A123,A125;
hence thesis by A125;
end;
then
A126: "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) [= y by A121,
LATTICE3:45;
y is_less_than {d.a9 where a9 is Attribute of C : y [= d.a9}
proof
let u be Element of L;
assume u in {d.a9 where a9 is Attribute of C : y [= d.a9};
then ex v being Attribute of C st u = d.v & y [= d.v;
hence thesis;
end;
then
y [= "/\"({d.a9 where a9 is Attribute of C : y [= d.a9},L) by LATTICE3:39;
hence thesis by A126,LATTICES:8;
end;
f.x = f.x@ by CONLAT_1:def 21
.= y by A110,FUNCT_1:1;
hence thesis by A111,A117,A120,TARSKI:2;
end;
A127: for a being Element of ConceptLattice(C) holds fi.(f.a) = a
proof
let a be Element of ConceptLattice(C);
set x = "/\"({d.u where u is Attribute of C : u in the Intent of a@},L);
set A = {a9 where a9 is Attribute of C : x [= d.a9};
A c= the carrier' of C
proof
let u be object;
assume u in A;
then ex u9 being Attribute of C st u9 = u & x [= d.u9;
hence thesis;
end;
then reconsider A as Subset of the carrier' of C;
set O = {o where o is Object of C : g.o [= x};
O c= the carrier of C
proof
let u be object;
assume u in O;
then ex u9 being Object of C st u9 = u & g.u9 [= x;
hence thesis;
end;
then reconsider O as Subset of the carrier of C;
A128: O = {o where o is Object of C : for a9 being Attribute of C st a9 in
the Intent of a@ holds g.o [= d.a9 }
proof
thus O c= {o where o is Object of C: for a9 being Attribute of C st a9
in the Intent of a@ holds g.o [= d.a9 }
proof
let u be object;
assume u in O;
then consider o9 being Object of C such that
A129: u = o9 and
A130: g.o9 [= x;
for a9 being Attribute of C st a9 in the Intent of a@ holds g.o9
[= d.a9
proof
let a9 be Attribute of C;
assume a9 in the Intent of a@;
then d.a9 in {d.y where y is Attribute of C : y in the Intent of a
@};
then x [= d.a9 by LATTICE3:38;
hence thesis by A130,LATTICES:7;
end;
hence thesis by A129;
end;
let u be object;
assume u in {o where o is Object of C : for a9 being Attribute of C
st a9 in the Intent of a@ holds g.o [= d.a9 };
then consider o9 being Object of C such that
A131: o9 = u and
A132: for a9 being Attribute of C st a9 in the Intent of a@ holds g.
o9 [= d.a9;
g.o9 is_less_than {d.y where y is Attribute of C : y in the Intent of a@}
proof
let q be Element of L;
assume q in {d.y where y is Attribute of C : y in the Intent of a@};
then ex qa being Attribute of C st q = d.qa & qa in the Intent of a@;
hence thesis by A132;
end;
then g.o9 [= x by LATTICE3:34;
hence thesis by A131;
end;
{o where o is Object of C : for a9 being Attribute of C st a9 in the
Intent of a@ holds g.o [= d.a9 } = {o where o is Object of C : for a9 being
Attribute of C st a9 in the Intent of a@ holds o is-connected-with a9 }
proof
thus {o where o is Object of C : for a9 being Attribute of C st a9 in
the Intent of a@ holds g.o [= d.a9 } c= {o where o is Object of C : for a9
being Attribute of C st a9 in the Intent of a@ holds o is-connected-with a9 }
proof
let u be object;
assume u in {o where o is Object of C : for a9 being Attribute of C
st a9 in the Intent of a@ holds g.o [= d.a9 };
then consider u9 being Object of C such that
A133: u = u9 and
A134: for a9 being Attribute of C st a9 in the Intent of a@ holds
g.u9 [= d.a9;
for a9 being Attribute of C st a9 in the Intent of a@ holds u9
is-connected-with a9
proof
let a9 be Attribute of C;
assume a9 in the Intent of a@;
then g.u9 [= d.a9 by A134;
hence thesis by A35;
end;
hence thesis by A133;
end;
let u be object;
assume u in {o where o is Object of C : for a9 being Attribute of C
st a9 in the Intent of a@ holds o is-connected-with a9 };
then consider u9 being Object of C such that
A135: u = u9 and
A136: for a9 being Attribute of C st a9 in the Intent of a@ holds u9
is-connected-with a9;
for a9 being Attribute of C st a9 in the Intent of a@ holds g.u9 [= d.a9
by A35,A136;
hence thesis by A135;
end;
then
A137: O = (AttributeDerivation(C)).(the Intent of a@) by A128,CONLAT_1:def 4
.= the Extent of a@ by CONLAT_1:def 10;
A138: fi.("/\"({d.u where u is Attribute of C : u in the Intent of a@},L))
= fi.(f.a) by A109;
[x,ConceptStr(#O,A#)] in fi;
then
A139: fi.x = ConceptStr(#O,A#) by FUNCT_1:1;
then ConceptStr(#O,A#) is FormalConcept of C by A93,CONLAT_1:31;
then A = (ObjectDerivation(C)).(the Extent of a@) by A137,CONLAT_1:def 10
.= the Intent of a@ by CONLAT_1:def 10;
hence thesis by A138,A139,A137,CONLAT_1:def 21;
end;
A140: for a,b being Element of L holds a [= b implies fi.a [= fi.b
proof
let a,b be Element of L;
set ca = fi.a, cb = fi.b;
assume
A141: a [= b;
A142: {o where o is Object of C : g.o [= a} c= {o where o is Object of C :
g.o [= b}
proof
let x be object;
assume x in {o where o is Object of C : g.o [= a};
then consider x9 being Object of C such that
A143: x9 = x and
A144: g.x9 [= a;
g.x9 [= b by A141,A144,LATTICES:7;
hence thesis by A143;
end;
A145: dom fi = the carrier of L by FUNCT_2:def 1;
then consider ya being object such that
A146: [a,ya] in fi by XTUPLE_0:def 12;
consider yb being object such that
A147: [b,yb] in fi by A145,XTUPLE_0:def 12;
consider xb being Element of L, Ob being Subset of the carrier of C, Ab
being Subset of the carrier' of C such that
A148: [b,yb] = [xb,ConceptStr(#Ob,Ab#)] and
A149: Ob = {o where o is Object of C : g.o [= xb} and
Ab = {a9 where a9 is Attribute of C : xb [= d.a9} by A147;
A150: b = [b,yb]`1
.= [xb,ConceptStr(#Ob,Ab#)]`1 by A148
.= xb;
then fi.b = ConceptStr(#Ob,Ab#) by A147,A148,FUNCT_1:1;
then
A151: the Extent of cb@ = Ob by CONLAT_1:def 21;
consider xa being Element of L, Oa being Subset of the carrier of C, Aa
being Subset of the carrier' of C such that
A152: [a,ya] = [xa,ConceptStr(#Oa,Aa#)] and
A153: Oa = {o where o is Object of C : g.o [= xa} and
Aa = {a9 where a9 is Attribute of C : xa [= d.a9} by A146;
A154: a = [a,ya]`1
.= [xa,ConceptStr(#Oa,Aa#)]`1 by A152
.= xa;
then fi.a = ConceptStr(#Oa,Aa#) by A146,A152,FUNCT_1:1;
then the Extent of ca@ = Oa by CONLAT_1:def 21;
then ca@ is-SubConcept-of cb@ by A142,A153,A149,A154,A150,A151,
CONLAT_1:def 16;
hence thesis by CONLAT_1:43;
end;
A155: for a,b being Element of ConceptLattice(C) holds f.a [= f.b implies a
[= b
proof
let a,b be Element of ConceptLattice(C);
assume
A156: f.a [= f.b;
fi.(f.a) = a & fi.(f.b) = b by A127;
hence thesis by A140,A156;
end;
for a,b being Element of ConceptLattice(C) holds a [= b implies f.a [= f.b
proof
let a,b be Element of ConceptLattice(C);
reconsider xa = "\/"({g.o where o is Object of C : o in the Extent of a@},
L), xb = "\/"({g.o where o is Object of C : o in the Extent of b@},L) as
Element of L;
[a@,xa] in f;
then
A157: f.(a@) = xa by FUNCT_1:1;
[b@,xb] in f;
then
A158: f.(b@) = xb by FUNCT_1:1;
assume a [= b;
then a@ is-SubConcept-of b@ by CONLAT_1:43;
then
A159: the Extent of a@ c= the Extent of b@ by CONLAT_1:def 16;
A160: {g.o where o is Object of C : o in the Extent of a@} c= {g.o where o
is Object of C : o in the Extent of b@}
proof
let x be object;
assume x in {g.o where o is Object of C : o in the Extent of a@};
then ex o being Object of C st x = g.o & o in the Extent of a @;
hence thesis by A159;
end;
a@ = a & b@ = b by CONLAT_1:def 21;
hence thesis by A160,A157,A158,LATTICE3:45;
end;
then reconsider f as Homomorphism of ConceptLattice(C),L by A155,A108,Lm1,Lm2
;
A161: f is onto by A108,FUNCT_2:def 3;
f is one-to-one by A155,Lm1;
hence thesis by A161,LATTICE4:def 3;
end;
definition
let L be Lattice;
func Context(L) -> strict non empty non void ContextStr equals
ContextStr(#the
carrier of L, the carrier of L, LattRel L#);
coherence;
end;
theorem Th15:
for L being complete Lattice holds ConceptLattice(Context(L)),L
are_isomorphic
proof
let L be complete Lattice;
reconsider g = id the carrier of L as Function of the carrier of Context(L),
the carrier of L;
reconsider d = id the carrier of L as Function of the carrier' of Context(L)
, the carrier of L;
A1: for o being Object of Context(L), a being Attribute of Context(L) holds
o is-connected-with a iff g.o [= d.a
proof
let o be Object of Context(L), a be Attribute of Context(L);
reconsider o9 = o, a9 = a as Element of L;
o is-connected-with a iff [o,a] in the Information of Context(L) by
CONLAT_1:def 2;
hence thesis by FILTER_1:31;
end;
for a being Element of L holds ex D9 being Subset of rng(d) st a = "/\"(
D9,L)
proof
let a be Element of L;
"/\"({a},L) = a & rng(d) = the carrier of L by LATTICE3:42,RELAT_1:45;
hence thesis;
end;
then
A2: rng(d) is infimum-dense;
rng(g) is supremum-dense
proof
let a be Element of L;
"\/"({a},L) = a & rng(g) = the carrier of L by LATTICE3:42,RELAT_1:45;
hence thesis;
end;
hence thesis by A2,A1,Th14;
end;
theorem
for L being Lattice holds L is complete iff ex C being FormalContext
st ConceptLattice(C),L are_isomorphic
proof
let L be Lattice;
hereby
assume L is complete;
then ConceptLattice(Context(L)),L are_isomorphic by Th15;
hence ex C being FormalContext st ConceptLattice(C),L are_isomorphic;
end;
given C being FormalContext such that
A1: ConceptLattice(C),L are_isomorphic;
let X be Subset of L;
consider f being Homomorphism of L,ConceptLattice(C) such that
A2: f is bijective by A1,LATTICE4:def 3;
set FX = { f.x where x is Element of L : x in X };
FX c= the carrier of ConceptLattice(C)
proof
let x be object;
assume x in FX;
then ex y being Element of L st x = f.y & y in X;
hence thesis;
end;
then reconsider FX as Subset of ConceptLattice(C);
set Fa = "/\"(FX,ConceptLattice(C));
consider a being Element of L such that
A3: Fa = f.a by A2,LATTICE4:6;
A4: for b being Element of L st b is_less_than X holds b [= a
proof
let b be Element of L;
assume
A5: b is_less_than X;
f.b is_less_than FX
proof
let q be Element of ConceptLattice(C);
assume q in FX;
then consider y being Element of L such that
A6: q = f.y and
A7: y in X;
b [= y by A5,A7;
hence thesis by A2,A6,LATTICE4:5;
end;
then f.b [= f.a by A3,LATTICE3:34;
hence thesis by A2,LATTICE4:5;
end;
A8: Fa is_less_than FX by LATTICE3:34;
a is_less_than X
proof
let q be Element of L;
assume q in X;
then f.q in FX;
then Fa [= f.q by A8;
hence thesis by A2,A3,LATTICE4:5;
end;
hence thesis by A4;
end;
begin :: Dual Concept Lattices
registration
let L be complete Lattice;
cluster L.: -> complete;
coherence
proof
let X be Subset of L.:;
A1: L.: = LattStr(#the carrier of L,the L_meet of L, the L_join of L#) by
LATTICE2:def 2;
then reconsider X9 = X as Subset of L;
set a9 = "\/"(X9,L);
reconsider a = a9 as Element of L.: by A1;
LattRel (L.:) = (LattRel L)~ by LATTICE3:20;
then
A2: LattRel (L .: .:) = ((LattRel L)~)~ by LATTICE3:20;
A3: for b being Element of L.: st b is_less_than X holds b [= a
proof
let b be Element of L.:;
reconsider b9 = b as Element of L by A1;
assume
A4: b is_less_than X;
X9 is_less_than b9
proof
let q be Element of L;
reconsider q9 = q as Element of L.: by A1;
assume q in X9;
then b [= q9 by A4;
then b% <= (q9)% by LATTICE3:7;
then [b%,(q9)%] in the InternalRel of LattPOSet L.: by ORDERS_2:def 5;
then [(q9)%,b%] in (the InternalRel of LattPOSet L.:)~ by RELAT_1:def 7
;
then [(q9)%,b%] in the InternalRel of LattPOSet (L .: .:) by
LATTICE3:20;
then q% <= (b9)% by A2,ORDERS_2:def 5;
hence thesis by LATTICE3:7;
end;
then a9 [= b9 by LATTICE3:def 21;
then (a9)% <= (b9)% by LATTICE3:7;
then [(a9)%,(b9)%] in the InternalRel of LattPOSet L by ORDERS_2:def 5;
then [(b9)%,(a9)%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7;
then [(b9)%,(a9)%] in the InternalRel of LattPOSet (L.:) by LATTICE3:20;
then b% <= a% by ORDERS_2:def 5;
hence thesis by LATTICE3:7;
end;
A5: X9 is_less_than a9 by LATTICE3:def 21;
a is_less_than X
proof
let q9 be Element of L.:;
reconsider q = q9 as Element of L by A1;
assume q9 in X;
then q [= a9 by A5;
then q% <= (a9)% by LATTICE3:7;
then [q%,(a9)%] in the InternalRel of LattPOSet L by ORDERS_2:def 5;
then [(a9)%,q%] in (the InternalRel of LattPOSet L)~ by RELAT_1:def 7;
then [(a9)%,q%] in the InternalRel of LattPOSet (L.:) by LATTICE3:20;
then a% <= (q9)% by ORDERS_2:def 5;
hence thesis by LATTICE3:7;
end;
hence thesis by A3;
end;
end;
definition
let C be FormalContext;
func C.: -> strict non empty non void ContextStr equals
ContextStr(#the
carrier' of C, the carrier of C, (the Information of C)~ #);
coherence;
end;
theorem
for C being strict FormalContext holds (C.:).: = C;
theorem Th18:
for C being FormalContext for O being Subset of the carrier of C
holds (ObjectDerivation(C)).O = (AttributeDerivation(C.:)).O
proof
let C be FormalContext;
let O be Subset of the carrier of C;
reconsider O9 = O as Subset of(the carrier' of C.:);
set A1 = {a where a is Attribute of C : for o being Object of C st o in O
holds o is-connected-with a };
set A2 = {a where a is Object of C.: : for o being Attribute of C.: st o in
O9 holds a is-connected-with o };
A1: A1 c= A2
proof
let u be object;
assume u in A1;
then consider a being Attribute of C such that
A2: a = u and
A3: for o being Object of C st o in O holds o is-connected-with a;
reconsider u9 = u as Object of C.: by A2;
for o9 being Attribute of C.: st o9 in O9 holds u9 is-connected-with o9
proof
let o9 be Attribute of C.:;
reconsider o = o9 as Object of C;
assume o9 in O9;
then o is-connected-with a by A3;
then [o,a] in the Information of C by CONLAT_1:def 2;
then [a,o] in the Information of C.: by RELAT_1:def 7;
hence thesis by A2,CONLAT_1:def 2;
end;
hence thesis;
end;
A4: A2 c= A1
proof
let u be object;
assume u in A2;
then consider a being Object of C.: such that
A5: a = u and
A6: for o being Attribute of C.: st o in O9 holds a is-connected-with o;
reconsider u9 = u as Attribute of C by A5;
for o being Object of C st o in O holds o is-connected-with u9
proof
let o9 be Object of C;
reconsider o = o9 as Attribute of C.:;
assume o9 in O;
then a is-connected-with o by A6;
then [a,o] in the Information of C.: by CONLAT_1:def 2;
then [o9,u9] in the Information of C by A5,RELAT_1:def 7;
hence thesis by CONLAT_1:def 2;
end;
hence thesis;
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 } & (AttributeDerivation(C.:)
).O9 = {a where a is Object of C.: : for o being Attribute of C.: st o in O9
holds a is-connected-with o } by CONLAT_1:def 3,def 4;
hence thesis by A1,A4;
end;
theorem Th19:
for C being FormalContext for A being Subset of the carrier' of
C holds (AttributeDerivation(C)).A = (ObjectDerivation(C.:)).A
proof
let C be FormalContext;
let O be Subset of the carrier' of C;
reconsider O9 = O as Subset of(the carrier of C.:);
set A1 = {a where a is Object of C : for o being Attribute of C st o in O
holds a is-connected-with o };
set A2 = {a where a is Attribute of C.: : for o being Object of C.: st o in
O9 holds o is-connected-with a };
A1: A1 c= A2
proof
let u be object;
assume u in A1;
then consider a being Object of C such that
A2: a = u and
A3: for o being Attribute of C st o in O holds a is-connected-with o;
reconsider u9 = u as Attribute of C.: by A2;
for o being Object of C.: st o in O9 holds o is-connected-with u9
proof
let o9 be Object of C.:;
reconsider o = o9 as Attribute of C;
assume o9 in O9;
then a is-connected-with o by A3;
then [a,o] in the Information of C by CONLAT_1:def 2;
then [o9,u9] in the Information of C.: by A2,RELAT_1:def 7;
hence thesis by CONLAT_1:def 2;
end;
hence thesis;
end;
A4: A2 c= A1
proof
let u be object;
assume u in A2;
then consider a being Attribute of C.: such that
A5: a = u and
A6: for o being Object of C.: st o in O9 holds o is-connected-with a;
reconsider u9 = u as Object of C by A5;
for o being Attribute of C st o in O holds u9 is-connected-with o
proof
let o9 be Attribute of C;
reconsider o = o9 as Object of C.:;
assume o9 in O;
then o is-connected-with a by A6;
then [o,a] in the Information of C.: by CONLAT_1:def 2;
then [u9,o9] in the Information of C by A5,RELAT_1:def 7;
hence thesis by CONLAT_1:def 2;
end;
hence thesis;
end;
(AttributeDerivation(C)).O = {a where a is Object of C : for o being
Attribute of C st o in O holds a is-connected-with o } & (ObjectDerivation(C.:
)).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 CONLAT_1:def 3,def 4;
hence thesis by A1,A4;
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
func CP.: -> strict ConceptStr over C.: means
:Def8:
the Extent of it = the Intent of CP & the Intent of it = the Extent of CP;
existence
proof
reconsider O = the Intent of CP as Subset of the carrier of C.:;
reconsider A = the Extent of CP as Subset of the carrier' of C.:;
take ConceptStr(# O,A#);
thus thesis;
end;
uniqueness;
end;
registration
let C be FormalContext;
let CP be FormalConcept of C;
cluster CP.: -> non empty concept-like;
coherence
proof
reconsider O = the Intent of CP as Subset of the carrier of C.:;
reconsider A = the Extent of CP as Subset of the carrier' of C.:;
set CPD = ConceptStr(# O,A#);
A1: (AttributeDerivation(C.:)).(the Intent of CPD) = (ObjectDerivation(C))
.(the Extent of CP) by Th18
.= the Extent of CPD by CONLAT_1:def 10;
A2: CPD = CP.: by Def8;
(ObjectDerivation(C.:)).(the Extent of CPD) = (AttributeDerivation(C))
.(the Intent of CP) by Th19
.= the Intent of CPD by CONLAT_1:def 10;
hence thesis by A1,A2,Lm3,CONLAT_1:def 10;
end;
end;
theorem
for C being strict FormalContext for CP being strict FormalConcept of
C holds (CP.:).: = CP
proof
let C be strict FormalContext;
let CP be strict FormalConcept of C;
A1: the Intent of (CP.:).: = the Extent of CP.: by Def8
.= the Intent of CP by Def8;
the Extent of (CP.:).: = the Intent of CP.: by Def8
.= the Extent of CP by Def8;
hence thesis by A1;
end;
definition
let C be FormalContext;
func DualHomomorphism(C) -> Homomorphism of (ConceptLattice(C)).:,
ConceptLattice(C.:) means
:Def9:
for CP being strict FormalConcept of C holds it.CP = CP.:;
existence
proof
set f = {[ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] where O is Subset of
the carrier of C, A is Subset of the carrier' of C : ConceptStr(#O,A#) is
FormalConcept of C };
A1: ConceptLattice(C.:) = LattStr(#B-carrier(C.:),B-join(C.:),B-meet(C.:)
#) by CONLAT_1:def 20;
A2: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
then
A3: (ConceptLattice(C)).: = LattStr(#B-carrier(C),B-meet(C),B-join(C)#) by
LATTICE2:def 2;
f c= [: the carrier of (ConceptLattice(C)).:, the carrier of
ConceptLattice(C.:) :]
proof
let y be object;
assume y in f;
then consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A4: y = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and
A5: ConceptStr(#O,A#) is FormalConcept of C;
(ConceptStr(#O,A#)).: is strict FormalConcept of C.: by A5;
then
A6: (ConceptStr(#O,A#)).: in the carrier of ConceptLattice(C.:) by A1,
CONLAT_1:31;
ConceptStr(#O,A#) in the carrier of (ConceptLattice(C)).: by A3,A5,
CONLAT_1:31;
hence thesis by A4,A6,ZFMISC_1:def 2;
end;
then reconsider f as Relation of the carrier of (ConceptLattice(C)).:, the
carrier of ConceptLattice(C.:);
the carrier of (ConceptLattice(C)).: c= dom f
proof
let y be object;
assume y in the carrier of (ConceptLattice(C)).:;
then
A7: y is strict FormalConcept of C by A3,CONLAT_1:31;
then consider
O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A8: y = ConceptStr(#O9,A9#);
set z = (ConceptStr(#O9,A9#)).:;
(ConceptStr(#O9,A9#)).: is strict FormalConcept of C.: by A7,A8;
then reconsider z as Element of ConceptLattice(C.:) by A1,CONLAT_1:31;
[y,z] in f by A7,A8;
hence thesis by XTUPLE_0:def 12;
end;
then
A9: the carrier of (ConceptLattice(C)).: = dom f;
for x,y1,y2 being object st [x,y1] in f & [x,y2] in f holds y1 = y2
proof
let x,y1,y2 be object;
assume that
A10: [x,y1] in f and
A11: [x,y2] in f;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A12: [x,y2] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and
ConceptStr(#O9,A9#) is FormalConcept of C by A11;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A13: [x,y1] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and
ConceptStr(#O,A#) is FormalConcept of C by A10;
A14: ConceptStr(#O,A#) = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1
.= [x,y1]`1 by A13
.= x
.= [x,y2]`1
.= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`1 by A12
.= ConceptStr(#O9,A9#);
thus y1 = [x,y1]`2
.= [x,y2]`2 by A13,A12,A14
.= y2;
end;
then reconsider f as Function of the carrier of (ConceptLattice(C)).:, the
carrier of ConceptLattice(C.:) by A9,FUNCT_1:def 1,FUNCT_2:def 1;
A15: (ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the
L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by
LATTICE2:def 2;
A16: for a,b being Element of (ConceptLattice(C)).: holds a [= b implies f
.a [= f.b
proof
let a,b be Element of (ConceptLattice(C)).:;
reconsider aa = a%, bb = b% as Element of LattPOSet ConceptLattice(C) by
A15;
reconsider a9 = a, b9 = b as Element of ConceptLattice(C) by A15;
A17: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
then consider fa being object such that
A18: [a,fa] in f by XTUPLE_0:def 12;
assume a [= b;
then a% <= b% by LATTICE3:7;
then
[a%,b%] in the InternalRel of (LattPOSet((ConceptLattice(C)).:)) by
ORDERS_2:def 5;
then
[a%,b%] in (the InternalRel of (LattPOSet (ConceptLattice(C))))~ by
LATTICE3:20;
then [b%,a%] in the InternalRel of (LattPOSet (ConceptLattice(C))) by
RELAT_1:def 7;
then
A19: bb <= aa by ORDERS_2:def 5;
(%aa)% = aa & (%bb)% = bb;
then %bb [= %aa by A19,LATTICE3:7;
then
A20: (%bb)@ is-SubConcept-of (%aa)@ by CONLAT_1:43;
consider fb being object such that
A21: [b,fb] in f by A17,XTUPLE_0:def 12;
A22: fb in rng f by A21,XTUPLE_0:def 13;
A23: f.b = fb by A21,FUNCT_1:1;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A24: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and
ConceptStr(#O9,A9#) is FormalConcept of C by A21;
A25: b = [b,fb]`1
.= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`1 by A24
.= (ConceptStr(#O9,A9#));
A26: fa in rng f by A18,XTUPLE_0:def 13;
A27: f.a = fa by A18,FUNCT_1:1;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A28: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and
ConceptStr(#O,A#) is FormalConcept of C by A18;
reconsider fa as Element of ConceptLattice(C.:) by A26;
A29: a = [a,fa]`1
.= [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`1 by A28
.= (ConceptStr(#O,A#));
reconsider fb as Element of ConceptLattice(C.:) by A22;
fb = [b,fb]`2
.= [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:]`2 by A24
.= (ConceptStr(#O9,A9#)).:;
then
A30: the Intent of fb@ = the Intent of (ConceptStr(#O9,A9#)).: by
CONLAT_1:def 21
.= the Extent of ConceptStr(#O9,A9#) by Def8
.= the Extent of (b9)@ by A25,CONLAT_1:def 21;
fa = [a,fa]`2
.= [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:]`2 by A28
.= (ConceptStr(#O,A#)).:;
then the Intent of fa@ = the Intent of (ConceptStr(#O,A#)).: by
CONLAT_1:def 21
.= the Extent of ConceptStr(#O,A#) by Def8
.= the Extent of (a9)@ by A29,CONLAT_1:def 21;
then the Intent of (fb)@ c= the Intent of (fa)@ by A20,A30,
CONLAT_1:def 16;
then (fa)@ is-SubConcept-of (fb)@ by CONLAT_1:28;
hence thesis by A27,A23,CONLAT_1:43;
end;
the carrier of ConceptLattice(C.:) c= rng f
proof
let u be object;
A31: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
assume u in the carrier of ConceptLattice(C.:);
then reconsider u as Element of ConceptLattice(C.:);
reconsider A9 = the Intent of u@ as Subset of the carrier of C;
reconsider O9 = the Extent of u@ as Subset of the carrier' of C;
set CP = ConceptStr(#A9,O9#);
A32: not(the Extent of u@ is empty & the Intent of u@ is empty) by
CONLAT_1:def 8;
A33: (AttributeDerivation(C)).(the Intent of CP) = (ObjectDerivation(C.:
)).(the Extent of u@) by Th19
.= the Extent of CP by CONLAT_1:def 10;
(ObjectDerivation(C)).(the Extent of CP) = (AttributeDerivation(C.:
)).(the Intent of u@) by Th18
.= the Intent of CP by CONLAT_1:def 10;
then CP is FormalConcept of C by A33,A32,CONLAT_1:def 8,def 10;
then CP in dom f by A15,A2,A31,CONLAT_1:31;
then consider v being object such that
A34: [CP,v] in f by XTUPLE_0:def 12;
consider Ov being Subset of the carrier of C, Av being Subset of the
carrier' of C such that
A35: [CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] and
ConceptStr(#Ov,Av#) is FormalConcept of C by A34;
A36: CP = [CP,v]`1
.= [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).: ]`1 by A35
.= ConceptStr(#Ov,Av#);
A37: v in rng f by A34,XTUPLE_0:def 13;
then reconsider v as strict FormalConcept of C.: by A1,CONLAT_1:31;
v = [CP,v]`2
.= [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).: ]`2 by A35
.= (ConceptStr(#Ov,Av#)).:;
then the Extent of v = the Extent of u@ & the Intent of v = the Intent
of u@ by A36,Def8;
hence thesis by A37,CONLAT_1:def 21;
end;
then
A38: rng f = the carrier of ConceptLattice(C.:);
A39: f is one-to-one
proof
let a,b be object;
assume that
A40: a in dom f and
A41: b in dom f and
A42: f.a = f.b;
reconsider a,b as Element of (ConceptLattice(C)).: by A40,A41;
consider fa being object such that
A43: [a,fa] in f by A40,XTUPLE_0:def 12;
consider fb being object such that
A44: [b,fb] in f by A41,XTUPLE_0:def 12;
A45: f.b = fb by A44,FUNCT_1:1;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A46: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and
ConceptStr(#O,A#) is FormalConcept of C by A43;
A47: a = (ConceptStr(#O,A#)) by A46,XTUPLE_0:1;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A48: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and
ConceptStr(#O9,A9#) is FormalConcept of C by A44;
A49: b = (ConceptStr(#O9,A9#)) by A48,XTUPLE_0:1;
A50: (ConceptStr(#O9,A9#)).:
= fb by A48,XTUPLE_0:1
.= fa by A42,A43,A45,FUNCT_1:1
.= (ConceptStr(#O,A#)).: by A46,XTUPLE_0:1;
then
A51: the Intent of ConceptStr(#O9,A9#) = the Extent of (ConceptStr(#O,A
#)).: by Def8
.= the Intent of ConceptStr(#O,A#) by Def8;
the Extent of ConceptStr(#O9,A9#) = the Intent of (ConceptStr(#O,A
#)).: by A50,Def8
.= the Extent of ConceptStr(#O,A#) by Def8;
hence thesis by A47,A49,A51;
end;
for a,b being Element of (ConceptLattice(C)).: holds f.a [= f.b
implies a [= b
proof
let a,b be Element of (ConceptLattice(C)).:;
A52: dom f = the carrier of (ConceptLattice(C)).: by FUNCT_2:def 1;
then consider fa being object such that
A53: [a,fa] in f by XTUPLE_0:def 12;
reconsider a9 = a, b9 = b as Element of ConceptLattice(C) by A15;
assume f.a [= f.b;
then
A54: (f.a)@ is-SubConcept-of (f.b)@ by CONLAT_1:43;
consider O being Subset of the carrier of C, A being Subset of the
carrier' of C such that
A55: [a,fa] = [ConceptStr(#O,A#),(ConceptStr(#O,A#)).:] and
ConceptStr(#O,A#) is FormalConcept of C by A53;
A56: a = (ConceptStr(#O,A#)) by A55,XTUPLE_0:1;
A57: fa in rng f by A53,XTUPLE_0:def 13;
consider fb being object such that
A58: [b,fb] in f by A52,XTUPLE_0:def 12;
A59: fb in rng f by A58,XTUPLE_0:def 13;
consider O9 being Subset of the carrier of C, A9 being Subset of the
carrier' of C such that
A60: [b,fb] = [ConceptStr(#O9,A9#),(ConceptStr(#O9,A9#)).:] and
ConceptStr(#O9,A9#) is FormalConcept of C by A58;
A61: b = (ConceptStr(#O9,A9#)) by A60,XTUPLE_0:1;
reconsider fb as Element of ConceptLattice(C.:) by A59;
A62: fb = (ConceptStr(#O9,A9#)).: by A60,XTUPLE_0:1;
A63: the Intent of (f.b)@ = the Intent of fb@ by A58,FUNCT_1:1
.= the Intent of (ConceptStr(#O9,A9#)).: by A62,CONLAT_1:def 21
.= the Extent of ConceptStr(#O9,A9#) by Def8
.= the Extent of (b9)@ by A61,CONLAT_1:def 21;
reconsider fa as Element of ConceptLattice(C.:) by A57;
A64: fa = (ConceptStr(#O,A#)).: by A55,XTUPLE_0:1;
the Intent of (f.a)@ = the Intent of fa@ by A53,FUNCT_1:1
.= the Intent of (ConceptStr(#O,A#)).: by A64,CONLAT_1:def 21
.= the Extent of ConceptStr(#O,A#) by Def8
.= the Extent of (a9)@ by A56,CONLAT_1:def 21;
then the Extent of (b9)@ c= the Extent of (a9)@ by A54,A63,CONLAT_1:28;
then (b9)@ is-SubConcept-of (a9)@ by CONLAT_1:def 16;
then b9 [= a9 by CONLAT_1:43;
then (b9)% <= (a9)% by LATTICE3:7;
then
[(b9)%,(a9)%] in the InternalRel of (LattPOSet(ConceptLattice(C)) )
by ORDERS_2:def 5;
then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)))~ by
RELAT_1:def 7;
then [a%,b%] in the InternalRel of (LattPOSet (ConceptLattice(C)).:) by
LATTICE3:20;
then a% <= b% by ORDERS_2:def 5;
hence thesis by LATTICE3:7;
end;
then reconsider
f as Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:)
by A16,A38,A39,Lm2;
for CP being strict FormalConcept of C holds f.CP = CP.:
proof
let CP be strict FormalConcept of C;
CP in B-carrier(C) by CONLAT_1:31;
then CP in dom f by A3,FUNCT_2:def 1;
then consider v being object such that
A65: [CP,v] in f by XTUPLE_0:def 12;
A66: v in rng f by A65,XTUPLE_0:def 13;
consider Ov being Subset of the carrier of C, Av being Subset of the
carrier' of C such that
A67: [CP,v] = [ConceptStr(#Ov,Av#),(ConceptStr(#Ov,Av#)).:] and
ConceptStr(#Ov,Av#) is FormalConcept of C by A65;
reconsider v as strict FormalConcept of C.: by A1,A66,CONLAT_1:31;
A68: CP = ConceptStr(#Ov,Av#) by A67,XTUPLE_0:1;
v = (ConceptStr(#Ov,Av#)).: by A67,XTUPLE_0:1;
hence thesis by A65,A68,FUNCT_1:1;
end;
hence thesis;
end;
uniqueness
proof
let F1,F2 be Homomorphism of (ConceptLattice(C)).:,ConceptLattice(C.:);
assume
A69: for CP being strict FormalConcept of C holds F1.CP = CP.:;
assume
A70: for CP being strict FormalConcept of C holds F2.CP = CP.:;
A71: for u being object st u in the carrier of (ConceptLattice(C)).: holds
F1.u = F2.u
proof
let u be object;
ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
then
A72: (ConceptLattice(C)).: = LattStr(#B-carrier(C),B-meet(C),B-join(C)
#) by LATTICE2:def 2;
assume u in the carrier of (ConceptLattice(C)).:;
then reconsider u as strict FormalConcept of C by A72,CONLAT_1:31;
F1.u = u.: by A69
.= F2.u by A70;
hence thesis;
end;
dom F1 = the carrier of (ConceptLattice(C)).: & dom F2 = the carrier
of ( ConceptLattice(C)).: by FUNCT_2:def 1;
hence thesis by A71;
end;
end;
theorem Th21:
for C being FormalContext holds DualHomomorphism(C) is bijective
proof
let C be FormalContext;
set f = DualHomomorphism(C);
A1: ConceptLattice(C) = LattStr(#B-carrier(C),B-join(C),B-meet(C)#) by
CONLAT_1:def 20;
A2: (ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the
L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by
LATTICE2:def 2;
the carrier of ConceptLattice(C.:) c= rng f
proof
let u be object;
assume u in the carrier of ConceptLattice(C.:);
then reconsider u as Element of ConceptLattice(C.:);
reconsider A9 = the Intent of u@ as Subset of the carrier of C;
reconsider O9 = the Extent of u@ as Subset of the carrier' of C;
set CP = ConceptStr(#A9,O9#);
A3: not(the Extent of u@ is empty & the Intent of u@ is empty) by
CONLAT_1:def 8;
A4: (AttributeDerivation(C)).(the Intent of CP) = (ObjectDerivation(C.:))
.(the Extent of u@) by Th19
.= the Extent of CP by CONLAT_1:def 10;
A5: (ObjectDerivation(C)).(the Extent of CP) = (AttributeDerivation(C.:))
.(the Intent of u@) by Th18
.= the Intent of CP by CONLAT_1:def 10;
then CP is FormalConcept of C by A4,A3,CONLAT_1:def 8,def 10;
then
A6: CP in the carrier of (ConceptLattice(C)) by A1,CONLAT_1:31;
reconsider CP as strict FormalConcept of C by A5,A4,A3,CONLAT_1:def 8
,def 10;
A7: the Extent of CP.: = the Extent of u@ by Def8;
f.CP = CP.: & the Intent of CP.: = the Intent of u@ by Def8,Def9;
then
A8: f.CP = u by A7,CONLAT_1:def 21;
CP in dom f by A2,A6,FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:def 3;
end;
then rng f = the carrier of ConceptLattice(C.:);
then
A9: f is onto by FUNCT_2:def 3;
f is one-to-one
proof
let a,b be object;
assume that
A10: a in dom f & b in dom f and
A11: f.a = f.b;
reconsider a,b as Element of (ConceptLattice(C)).: by A10;
(ConceptLattice(C)).: = LattStr(#the carrier of ConceptLattice(C), the
L_meet of ConceptLattice(C), the L_join of ConceptLattice(C)#) by
LATTICE2:def 2;
then reconsider a,b as Element of ConceptLattice(C);
A12: f.(a@) = f.a & f.(b@) = f.b by CONLAT_1:def 21;
A13: f.(a@) = (a@).: & f.(b@) = (b@).: by Def9;
then
A14: the Extent of a@ = the Intent of (b@).: by A11,A12,Def8
.= the Extent of b@ by Def8;
the Intent of a@ = the Extent of (b@).: by A11,A13,A12,Def8
.= the Intent of b@ by Def8;
then a = b@ by A14,CONLAT_1:def 21
.= b by CONLAT_1:def 21;
hence thesis;
end;
hence thesis by A9;
end;
theorem
for C being FormalContext holds
ConceptLattice(C.:),(ConceptLattice(C)).: are_isomorphic
proof
let C be FormalContext;
DualHomomorphism(C) is bijective by Th21;
hence thesis by LATTICE4:def 3;
end;