:: CONLAT_2 semantic presentation
begin
definition
let C be FormalContext;
let CP be strict FormalConcept of C;
func @ CP -> Element of (ConceptLattice C) equals :: CONLAT_2:def 1
CP;
coherence
CP is Element of (ConceptLattice C)
proof
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20;
hence CP is Element of (ConceptLattice C) by CONLAT_1:31; ::_thesis: verum
end;
end;
:: deftheorem defines @ CONLAT_2:def_1_:_
for C being FormalContext
for CP being strict FormalConcept of C holds @ CP = CP;
registration
let C be FormalContext;
cluster ConceptLattice C -> bounded ;
coherence
ConceptLattice C is bounded
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); ::_thesis: a [= @ (Concept-with-all-Objects C)
a @ is-SubConcept-of (@ (Concept-with-all-Objects C)) @ by A1, CONLAT_1:30;
hence a [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum
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) )
proof
let a be Element of (ConceptLattice C); ::_thesis: ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) )
a [= @ (Concept-with-all-Objects C) by A2;
hence ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) by LATTICES:def_3; ::_thesis: verum
end;
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); ::_thesis: @ (Concept-with-all-Attributes C) [= a
(@ (Concept-with-all-Attributes C)) @ is-SubConcept-of a @ by A4, CONLAT_1:30;
hence @ (Concept-with-all-Attributes C) [= a by CONLAT_1:43; ::_thesis: verum
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) )
proof
let a be Element of (ConceptLattice C); ::_thesis: ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) )
@ (Concept-with-all-Attributes C) [= a by A5;
hence ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) by LATTICES:4; ::_thesis: verum
end;
then ConceptLattice C is lower-bounded by LATTICES:def_13;
hence ConceptLattice C is bounded by A3; ::_thesis: verum
end;
end;
theorem Th1: :: CONLAT_2:1
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; ::_thesis: ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C )
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); ::_thesis: a [= @ (Concept-with-all-Objects C)
a @ is-SubConcept-of (@ (Concept-with-all-Objects C)) @ by A1, CONLAT_1:30;
hence a [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum
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) )
proof
let a be Element of (ConceptLattice C); ::_thesis: ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) )
a [= @ (Concept-with-all-Objects C) by A2;
hence ( (@ (Concept-with-all-Objects C)) "\/" a = @ (Concept-with-all-Objects C) & a "\/" (@ (Concept-with-all-Objects C)) = @ (Concept-with-all-Objects C) ) by LATTICES:def_3; ::_thesis: verum
end;
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); ::_thesis: @ (Concept-with-all-Attributes C) [= a
(@ (Concept-with-all-Attributes C)) @ is-SubConcept-of a @ by A4, CONLAT_1:30;
hence @ (Concept-with-all-Attributes C) [= a by CONLAT_1:43; ::_thesis: verum
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) )
proof
let a be Element of (ConceptLattice C); ::_thesis: ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) )
@ (Concept-with-all-Attributes C) [= a by A5;
hence ( (@ (Concept-with-all-Attributes C)) "/\" a = @ (Concept-with-all-Attributes C) & a "/\" (@ (Concept-with-all-Attributes C)) = @ (Concept-with-all-Attributes C) ) by LATTICES:4; ::_thesis: verum
end;
hence ( Bottom (ConceptLattice C) = Concept-with-all-Attributes C & Top (ConceptLattice C) = Concept-with-all-Objects C ) by A3, LATTICES:def_16, LATTICES:def_17; ::_thesis: verum
end;
theorem Th2: :: CONLAT_2:2
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; ::_thesis: 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 }
let D be non empty Subset-Family of the carrier of C; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }
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 } ;
percases ( { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } <> {} or { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = {} ) ;
supposeA1: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } <> {} ; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }
thus (ObjectDerivation C) . (union D) c= meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } :: according to XBOOLE_0:def_10 ::_thesis: meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } c= (ObjectDerivation C) . (union D)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (ObjectDerivation C) . (union D) or x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } )
assume x in (ObjectDerivation C) . (union D) ; ::_thesis: x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D }
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 = x as Attribute of C ;
A3: for O being Subset of the carrier of C st O in D holds
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; ::_thesis: ( O in D implies for o being Object of C st o in O holds
o is-connected-with x )
assume A4: O in D ; ::_thesis: for o being Object of C st o in O holds
o is-connected-with x
let o be Object of C; ::_thesis: ( o in O implies o is-connected-with x )
assume o in O ; ::_thesis: o is-connected-with x
then o in union D by A4, TARSKI:def_4;
hence o is-connected-with x by A2; ::_thesis: verum
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; ::_thesis: ( O in D implies x in (ObjectDerivation C) . O )
assume O in D ; ::_thesis: x in (ObjectDerivation C) . O
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 x in (ObjectDerivation C) . O by CONLAT_1:def_3; ::_thesis: verum
end;
for Y being set st Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } implies x in Y )
assume Y in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: x in Y
then ex O being Subset of the carrier of C st
( Y = (ObjectDerivation C) . O & O in D ) ;
hence x in Y by A5; ::_thesis: verum
end;
hence x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } by A1, SETFAM_1:def_1; ::_thesis: verum
end;
thus meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } c= (ObjectDerivation C) . (union D) ::_thesis: verum
proof
set d = the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } or x in (ObjectDerivation C) . (union D) )
assume A6: x in meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: x in (ObjectDerivation C) . (union D)
then A7: x in the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } by A1, SETFAM_1:def_1;
the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in 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
( the Element of { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = (ObjectDerivation C) . X & X in D ) ;
then reconsider x = 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; ::_thesis: ( O in D implies x in (ObjectDerivation C) . O )
assume O in D ; ::_thesis: x in (ObjectDerivation C) . O
then (ObjectDerivation C) . O in { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 in D } ;
hence x in (ObjectDerivation C) . O by A6, SETFAM_1:def_1; ::_thesis: verum
end;
A9: for O being Subset of the carrier of C st O in D holds
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; ::_thesis: ( O in D implies for o being Object of C st o in O holds
o is-connected-with x )
assume O in D ; ::_thesis: for o being Object of C st o in O holds
o is-connected-with x
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; ::_thesis: ( o in O implies o is-connected-with x )
assume o in O ; ::_thesis: o is-connected-with x
hence o is-connected-with x by A10; ::_thesis: verum
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; ::_thesis: ( o in union D implies o is-connected-with x )
assume o in union D ; ::_thesis: o is-connected-with x
then ex Y being set st
( o in Y & Y in D ) by TARSKI:def_4;
hence o is-connected-with x by A9; ::_thesis: verum
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 x in (ObjectDerivation C) . (union D) by CONLAT_1:def_3; ::_thesis: verum
end;
end;
supposeA11: { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } = {} ; ::_thesis: (ObjectDerivation C) . (union D) = meet { ((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 <> {} ; ::_thesis: contradiction
(ObjectDerivation C) . the Element of D in { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ;
hence contradiction by A11; ::_thesis: verum
end;
hence (ObjectDerivation C) . (union D) = meet { ((ObjectDerivation C) . O) where O is Subset of the carrier of C : O in D } ; ::_thesis: verum
end;
end;
end;
theorem Th3: :: CONLAT_2:3
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; ::_thesis: 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 }
let D be non empty Subset-Family of the carrier' of C; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
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__::_thesis:_(_(__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__<>_{}_&_(AttributeDerivation_C)_._(union_D)_=_meet__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__)_or_(__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__=_{}_&_(AttributeDerivation_C)_._(union_D)_=_meet__{__((AttributeDerivation_C)_._A)_where_A_is_Subset_of_the_carrier'_of_C_:_A_in_D__}__)_)
percases ( { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} or { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ) ;
caseA1: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } <> {} ; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
thus (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ::_thesis: verum
proof
thus (AttributeDerivation C) . (union D) c= meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } :: according to XBOOLE_0:def_10 ::_thesis: meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } c= (AttributeDerivation C) . (union D)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (AttributeDerivation C) . (union D) or x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } )
assume x in (AttributeDerivation C) . (union D) ; ::_thesis: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D }
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 = x as Object of C ;
A3: for A being Subset of the carrier' of C st A in D holds
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; ::_thesis: ( A in D implies for a being Attribute of C st a in A holds
x is-connected-with a )
assume A4: A in D ; ::_thesis: for a being Attribute of C st a in A holds
x is-connected-with a
let a be Attribute of C; ::_thesis: ( a in A implies x is-connected-with a )
assume a in A ; ::_thesis: x is-connected-with a
then a in union D by A4, TARSKI:def_4;
hence x is-connected-with a by A2; ::_thesis: verum
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; ::_thesis: ( A in D implies x in (AttributeDerivation C) . A )
assume A in D ; ::_thesis: x in (AttributeDerivation C) . A
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 x in (AttributeDerivation C) . A by CONLAT_1:def_4; ::_thesis: verum
end;
for Y being set st Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } implies x in Y )
assume Y in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: x in Y
then ex A being Subset of the carrier' of C st
( Y = (AttributeDerivation C) . A & A in D ) ;
hence x in Y by A5; ::_thesis: verum
end;
hence x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def_1; ::_thesis: verum
end;
set d = the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } or x in (AttributeDerivation C) . (union D) )
assume A6: x in meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: x in (AttributeDerivation C) . (union D)
then A7: x in the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } by A1, SETFAM_1:def_1;
the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in 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
( the Element of { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = (AttributeDerivation C) . X & X in D ) ;
then reconsider x = 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; ::_thesis: ( A in D implies x in (AttributeDerivation C) . A )
assume A in D ; ::_thesis: x in (AttributeDerivation C) . A
then (AttributeDerivation C) . A in { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in D } ;
hence x in (AttributeDerivation C) . A by A6, SETFAM_1:def_1; ::_thesis: verum
end;
A9: for A being Subset of the carrier' of C st A in D holds
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; ::_thesis: ( A in D implies for a being Attribute of C st a in A holds
x is-connected-with a )
assume A in D ; ::_thesis: for a being Attribute of C st a in A holds
x is-connected-with a
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; ::_thesis: ( a in A implies x is-connected-with a )
assume a in A ; ::_thesis: x is-connected-with a
hence x is-connected-with a by A10; ::_thesis: verum
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; ::_thesis: ( a in union D implies x is-connected-with a )
assume a in union D ; ::_thesis: x is-connected-with a
then ex Y being set st
( a in Y & Y in D ) by TARSKI:def_4;
hence x is-connected-with a by A9; ::_thesis: verum
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 x in (AttributeDerivation C) . (union D) by CONLAT_1:def_4; ::_thesis: verum
end;
end;
caseA11: { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } = {} ; ::_thesis: (AttributeDerivation C) . (union D) = meet { ((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 <> {} ; ::_thesis: contradiction
(AttributeDerivation C) . the Element of D in { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ;
hence contradiction by A11; ::_thesis: verum
end;
hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: verum
end;
end;
end;
hence (AttributeDerivation C) . (union D) = meet { ((AttributeDerivation C) . A) where A is Subset of the carrier' of C : A in D } ; ::_thesis: verum
end;
theorem Th4: :: CONLAT_2:4
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; ::_thesis: for D being Subset of (ConceptLattice C) holds
( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )
let D be Subset of (ConceptLattice C); ::_thesis: ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C )
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20;
hence ( "/\" (D,(ConceptLattice C)) is FormalConcept of C & "\/" (D,(ConceptLattice C)) is FormalConcept of C ) by CONLAT_1:31; ::_thesis: verum
end;
definition
let C be FormalContext;
let D be Subset of (ConceptLattice C);
func "/\" (D,C) -> FormalConcept of C equals :: CONLAT_2:def 2
"/\" (D,(ConceptLattice C));
coherence
"/\" (D,(ConceptLattice C)) is FormalConcept of C by Th4;
func "\/" (D,C) -> FormalConcept of C equals :: CONLAT_2:def 3
"\/" (D,(ConceptLattice C));
coherence
"\/" (D,(ConceptLattice C)) is FormalConcept of C by Th4;
end;
:: deftheorem defines "/\" CONLAT_2:def_2_:_
for C being FormalContext
for D being Subset of (ConceptLattice C) holds "/\" (D,C) = "/\" (D,(ConceptLattice C));
:: deftheorem defines "\/" CONLAT_2:def_3_:_
for C being FormalContext
for D being Subset of (ConceptLattice C) holds "\/" (D,C) = "\/" (D,(ConceptLattice C));
theorem :: CONLAT_2:5
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; ::_thesis: ( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C )
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); ::_thesis: ( b is_less_than {} implies b [= @ (Concept-with-all-Objects C) )
assume b is_less_than {} ; ::_thesis: b [= @ (Concept-with-all-Objects C)
( b @ is-SubConcept-of Concept-with-all-Objects C & Concept-with-all-Objects C = (@ (Concept-with-all-Objects C)) @ ) by CONLAT_1:30, CONLAT_1:def_21;
hence b [= @ (Concept-with-all-Objects C) by CONLAT_1:43; ::_thesis: verum
end;
for q being Element of (ConceptLattice C) st q in {} holds
@ (Concept-with-all-Objects C) [= q ;
then ( "\/" (({} (ConceptLattice C)),C) = Bottom (ConceptLattice C) & @ (Concept-with-all-Objects C) is_less_than {} ) by LATTICE3:49, LATTICE3:def_16;
hence ( "\/" (({} (ConceptLattice C)),C) = Concept-with-all-Attributes C & "/\" (({} (ConceptLattice C)),C) = Concept-with-all-Objects C ) by A1, Th1, LATTICE3:34; ::_thesis: verum
end;
theorem :: CONLAT_2:6
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; ::_thesis: ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C )
A1: @ (Concept-with-all-Attributes C) is_less_than [#] the carrier of (ConceptLattice C)
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in [#] the carrier of (ConceptLattice C) or @ (Concept-with-all-Attributes C) [= q )
assume q in [#] the carrier of (ConceptLattice C) ; ::_thesis: @ (Concept-with-all-Attributes C) [= q
( Concept-with-all-Attributes C is-SubConcept-of q @ & Concept-with-all-Attributes C = (@ (Concept-with-all-Attributes C)) @ ) by CONLAT_1:30, CONLAT_1:def_21;
hence @ (Concept-with-all-Attributes C) [= q by CONLAT_1:43; ::_thesis: verum
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, LATTICE3:def_16;
hence ( "\/" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Objects C & "/\" (([#] the carrier of (ConceptLattice C)),C) = Concept-with-all-Attributes C ) by A1, Th1, LATTICE3:34; ::_thesis: verum
end;
theorem :: CONLAT_2:7
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; ::_thesis: 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 } )
let D be non empty Subset of (ConceptLattice C); ::_thesis: ( 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 } )
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in bool the carrier of C )
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 } ; ::_thesis: x in bool the carrier of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( x = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
hence x in bool the carrier of C ; ::_thesis: verum
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 ;
(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 } )) 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 } ;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier of C )
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 } ; ::_thesis: x in the carrier of C
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 ex I being Subset of the carrier' of C st
( Y = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A2;
hence x in the carrier of C by A1; ::_thesis: verum
end;
then reconsider 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 } as Subset of the carrier of C ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } )) or x in the carrier of C )
A3: (AttributeDerivation C) . ((ObjectDerivation C) . u) is Element of bool the carrier of C ;
assume x in (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 } )) ; ::_thesis: x in the carrier of C
hence x in the carrier of C by A3; ::_thesis: verum
end;
then reconsider 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 } )) 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 set st x in D holds
( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )
proof
let x be set ; ::_thesis: ( x in D implies ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) )
assume x in D ; ::_thesis: ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )
then x is strict FormalConcept of C by A4, CONLAT_1:31;
hence ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ; ::_thesis: verum
end;
then ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) ;
then the Extent of the Element of D 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 = 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } } )
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 } ; ::_thesis: 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 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 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 } } by A9; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } } or 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 } )
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 } } ; ::_thesis: 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 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 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 } by A13; ::_thesis: verum
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, XBOOLE_0:def_10;
A15: (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 } ) = meet { ((ObjectDerivation C) . O9) where O9 is Subset of the carrier of C : O9 in OO } by Th2;
(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 } ) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } ) or x in the carrier' of C )
ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then A16: the Intent of the Element of D 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 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 } 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 ex I1 being Subset of the carrier' of C st
( 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 } = the Intent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ;
assume x in (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 } ) ; ::_thesis: x in the carrier' of C
then x in 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 } by A15, A14, A16, SETFAM_1:def_1;
hence x in the carrier' of C by A17; ::_thesis: verum
end;
then reconsider a = (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 } ) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier of C )
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 } ; ::_thesis: x in the carrier of C
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 ex I being Subset of the carrier' of C st
( Y = the Extent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A19;
hence x in the carrier of C by A18; ::_thesis: verum
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); ::_thesis: ( D is_less_than r implies CP [= r )
assume A22: D is_less_than r ; ::_thesis: CP [= 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); ::_thesis: ( q in D implies the Intent of (r @) c= the Intent of (q @) )
assume q in D ; ::_thesis: the Intent of (r @) c= the Intent of (q @)
then q [= r by A22, LATTICE3:def_17;
then q @ is-SubConcept-of r @ by CONLAT_1:43;
hence the Intent of (r @) c= the Intent of (q @) by CONLAT_1:28; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Intent of (r @) or x in 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 } )
assume A24: x in the Intent of (r @) ; ::_thesis: x in 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 }
A25: for Y being set st 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 } holds
x in Y
proof
let Y be set ; ::_thesis: ( 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 )
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 } ; ::_thesis: x in Y
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 x in Y by A26, CONLAT_1:def_21; ::_thesis: verum
end;
ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then the Intent of the Element of D 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 x in 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 A25, SETFAM_1:def_1; ::_thesis: verum
end;
then CP @ is-SubConcept-of r @ by A20, CONLAT_1:28;
hence CP [= r by CONLAT_1:43; ::_thesis: verum
end;
D is_less_than CP
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_17 ::_thesis: ( not q in D or q [= CP )
assume q in D ; ::_thesis: q [= CP
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 q [= CP by CONLAT_1:43; ::_thesis: verum
end;
hence ( 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 } ) by A15, A14, A21, LATTICE3:def_21; ::_thesis: verum
end;
theorem :: CONLAT_2:8
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; ::_thesis: 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 } )) )
let D be non empty Subset of (ConceptLattice C); ::_thesis: ( 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 } )) )
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in bool the carrier' of C )
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 } ; ::_thesis: x in bool the carrier' of C
then ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st
( x = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) ;
hence x in bool the carrier' of C ; ::_thesis: verum
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 ;
(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 } )) 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 } ;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier' of C )
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 } ; ::_thesis: x in the carrier' of C
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 ex I being Subset of the carrier' of C st
( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A2;
hence x in the carrier' of C by A1; ::_thesis: verum
end;
then reconsider 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 } as Subset of the carrier' of C ;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } )) or x in the carrier' of C )
A3: (ObjectDerivation C) . ((AttributeDerivation C) . u) is Element of bool the carrier' of C ;
assume x in (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 } )) ; ::_thesis: x in the carrier' of C
hence x in the carrier' of C by A3; ::_thesis: verum
end;
then reconsider 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 } )) 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 set st x in D holds
( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )
proof
let x be set ; ::_thesis: ( x in D implies ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) )
assume x in D ; ::_thesis: ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) )
then x is strict FormalConcept of C by A4, CONLAT_1:31;
hence ( x is strict FormalConcept of C & ex E being Subset of the carrier of C ex I being Subset of the carrier' of C st x = ConceptStr(# E,I #) ) ; ::_thesis: verum
end;
then ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) ;
then the Intent of the Element of D 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 = 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } } )
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 } ; ::_thesis: 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 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 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 } } by A9; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } } or 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 } )
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 } } ; ::_thesis: 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 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 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 } by A13; ::_thesis: verum
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, XBOOLE_0:def_10;
A15: (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 } ) = meet { ((AttributeDerivation C) . A9) where A9 is Subset of the carrier' of C : A9 in AA } by Th3;
(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 } ) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (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 } ) or x in the carrier of C )
ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then A16: the Extent of the Element of D 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 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 } 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 ex I1 being Subset of the carrier' of C st
( 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 } = the Extent of ConceptStr(# E1,I1 #) & ConceptStr(# E1,I1 #) in D ) ;
assume x in (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 } ) ; ::_thesis: x in the carrier of C
then x in 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 } by A15, A14, A16, SETFAM_1:def_1;
hence x in the carrier of C by A17; ::_thesis: verum
end;
then reconsider o = (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 } ) 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or x in the carrier' of C )
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 } ; ::_thesis: x in the carrier' of C
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 ex I being Subset of the carrier' of C st
( Y = the Intent of ConceptStr(# E,I #) & ConceptStr(# E,I #) in D ) by A19;
hence x in the carrier' of C by A18; ::_thesis: verum
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); ::_thesis: ( r is_less_than D implies r [= CP )
assume A22: r is_less_than D ; ::_thesis: r [= CP
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); ::_thesis: ( q in D implies the Extent of (r @) c= the Extent of (q @) )
assume q in D ; ::_thesis: the Extent of (r @) c= the Extent of (q @)
then r [= q by A22, LATTICE3:def_16;
then r @ is-SubConcept-of q @ by CONLAT_1:43;
hence the Extent of (r @) c= the Extent of (q @) by CONLAT_1:def_16; ::_thesis: verum
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of (r @) or x in 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 } )
assume A24: x in the Extent of (r @) ; ::_thesis: x in 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 }
A25: for Y being set st 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 } holds
x in Y
proof
let Y be set ; ::_thesis: ( 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 )
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 } ; ::_thesis: x in Y
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 x in Y by A26, CONLAT_1:def_21; ::_thesis: verum
end;
ex E9 being Subset of the carrier of C ex I9 being Subset of the carrier' of C st the Element of D = ConceptStr(# E9,I9 #) by A5;
then the Extent of the Element of D 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 x in 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 A25, SETFAM_1:def_1; ::_thesis: verum
end;
then r @ is-SubConcept-of CP @ by A20, CONLAT_1:def_16;
hence r [= CP by CONLAT_1:43; ::_thesis: verum
end;
CP is_less_than D
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in D or CP [= q )
assume q in D ; ::_thesis: CP [= q
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 CP [= q by CONLAT_1:43; ::_thesis: verum
end;
hence ( 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 } )) ) by A15, A14, A21, LATTICE3:34; ::_thesis: verum
end;
theorem Th9: :: CONLAT_2:9
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; ::_thesis: 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
let CP be strict FormalConcept of C; ::_thesis: "\/" ( { 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
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 { 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} ) } is_less_than CP9 holds
@ CP [= CP9
proof
let CP9 be Element of (ConceptLattice C); ::_thesis: ( { 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} ) } is_less_than CP9 implies @ CP [= CP9 )
assume A2: { 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} ) } is_less_than CP9 ; ::_thesis: @ CP [= CP9
A3: the Extent of CP c= the Extent of (CP9 @)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Extent of CP or x in the Extent of (CP9 @) )
assume A4: x in the Extent of CP ; ::_thesis: x in the Extent of (CP9 @)
then reconsider x = x as Element of C ;
set Ax = (ObjectDerivation C) . {x};
set Ox = (AttributeDerivation C) . ((ObjectDerivation C) . {x});
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . {x})),((ObjectDerivation C) . {x}) #) 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, LATTICE3:def_17;
then A5: (@ Cx) @ is-SubConcept-of CP9 @ by CONLAT_1:43;
{x} c= (AttributeDerivation C) . ((ObjectDerivation C) . {x}) 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 x in the Extent of (CP9 @) by A6; ::_thesis: verum
end;
CP = (@ CP) @ by CONLAT_1:def_21;
then (@ CP) @ is-SubConcept-of CP9 @ by A3, CONLAT_1:def_16;
hence @ CP [= CP9 by CONLAT_1:43; ::_thesis: verum
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 CP & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) } is_less_than @ CP
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_17 ::_thesis: ( not q 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} ) } or q [= @ CP )
assume q 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} ) } ; ::_thesis: q [= @ CP
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, CONLAT_1: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 q [= @ CP by A12, CONLAT_1:43; ::_thesis: verum
end;
hence "\/" ( { 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 by A1, LATTICE3:def_21; ::_thesis: verum
end;
theorem Th10: :: CONLAT_2:10
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; ::_thesis: 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
let CP be strict FormalConcept of C; ::_thesis: "/\" ( { 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
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 { 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}) ) } holds
CP9 [= @ CP
proof
let CP9 be Element of (ConceptLattice C); ::_thesis: ( CP9 is_less_than { 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}) ) } implies CP9 [= @ CP )
assume A2: CP9 is_less_than { 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}) ) } ; ::_thesis: CP9 [= @ CP
A3: the Intent of CP c= the Intent of (CP9 @)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the Intent of CP or x in the Intent of (CP9 @) )
assume A4: x in the Intent of CP ; ::_thesis: x in the Intent of (CP9 @)
then reconsider x = x as Element of the carrier' of C ;
set Ax = (ObjectDerivation C) . ((AttributeDerivation C) . {x});
set Ox = (AttributeDerivation C) . {x};
reconsider Cx = ConceptStr(# ((AttributeDerivation C) . {x}),((ObjectDerivation C) . ((AttributeDerivation C) . {x})) #) 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, LATTICE3:def_16;
then A5: CP9 @ is-SubConcept-of (@ Cx) @ by CONLAT_1:43;
{x} c= (ObjectDerivation C) . ((AttributeDerivation C) . {x}) 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 x in the Intent of (CP9 @) by A6; ::_thesis: verum
end;
CP = (@ CP) @ by CONLAT_1:def_21;
then CP9 @ is-SubConcept-of (@ CP) @ by A3, CONLAT_1:28;
hence CP9 [= @ CP by CONLAT_1:43; ::_thesis: verum
end;
@ CP is_less_than { 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}) ) }
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q 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}) ) } or @ CP [= q )
assume q 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}) ) } ; ::_thesis: @ CP [= q
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, CONLAT_1: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 @ CP [= q by A12, CONLAT_1:43; ::_thesis: verum
end;
hence "/\" ( { 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 by A1, LATTICE3:34; ::_thesis: verum
end;
definition
let C be FormalContext;
func gamma C -> Function of the carrier of C, the carrier of (ConceptLattice C) means :Def4: :: CONLAT_2:def 4
for o being Element of C ex O being Subset of the carrier of C ex 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
ex b1 being Function of the carrier of C, the carrier of (ConceptLattice C) st
for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
proof
defpred S1[ set , set ] means ex O being Subset of the carrier of C ex 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 set st e in the carrier of C holds
ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier of C implies ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] ) )
assume e in the carrier of C ; ::_thesis: ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
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(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) ; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] )
( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) is FormalConcept of C ) by CONLAT_1:19, CONLAT_1:def_20;
hence ( ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . ((ObjectDerivation C) . se)),((ObjectDerivation C) . se) #)] ) by CONLAT_1:31; ::_thesis: verum
end;
consider f being Function of the carrier of C, the carrier of (ConceptLattice C) such that
A2: for e being set st e in the carrier of C holds
S1[e,f . e] from FUNCT_2:sch_1(A1);
take f ; ::_thesis: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
let o be Element of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} )
thus ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the carrier of C, the carrier of (ConceptLattice C) st ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) holds
b1 = b2
proof
let F1, F2 be Function of the carrier of C, the carrier of (ConceptLattice C); ::_thesis: ( ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) & ( for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ) implies F1 = F2 )
assume A3: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; ::_thesis: ( ex o being Element of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . o = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) or not A = (ObjectDerivation C) . {o} ) or F1 = F2 )
assume A4: for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) ; ::_thesis: F1 = F2
A5: for o being set st o in the carrier of C holds
F1 . o = F2 . o
proof
let o be set ; ::_thesis: ( o in the carrier of C implies F1 . o = F2 . o )
assume o in the carrier of C ; ::_thesis: F1 . o = F2 . o
then reconsider o = o as Element of C ;
( ex O being Subset of the carrier of C ex 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 ex 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 F1 . o = F2 . o ; ::_thesis: verum
end;
( dom F1 = the carrier of C & dom F2 = the carrier of C ) by FUNCT_2:def_1;
hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines gamma CONLAT_2:def_4_:_
for C being FormalContext
for b2 being Function of the carrier of C, the carrier of (ConceptLattice C) holds
( b2 = gamma C iff for o being Element of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . ((ObjectDerivation C) . {o}) & A = (ObjectDerivation C) . {o} ) );
definition
let C be FormalContext;
func delta C -> Function of the carrier' of C, the carrier of (ConceptLattice C) means :Def5: :: CONLAT_2:def 5
for a being Element of the carrier' of C ex O being Subset of the carrier of C ex 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
ex b1 being Function of the carrier' of C, the carrier of (ConceptLattice C) st
for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
proof
defpred S1[ set , set ] means ex O being Subset of the carrier of C ex 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 set st e in the carrier' of C holds
ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier' of C implies ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] ) )
assume e in the carrier' of C ; ::_thesis: ex u being set st
( u in the carrier of (ConceptLattice C) & S1[e,u] )
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(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) ; ::_thesis: ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #)] )
( ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) & ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) is FormalConcept of C ) by CONLAT_1:21, CONLAT_1:def_20;
hence ( ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #) in the carrier of (ConceptLattice C) & S1[e, ConceptStr(# ((AttributeDerivation C) . se),((ObjectDerivation C) . ((AttributeDerivation C) . se)) #)] ) by CONLAT_1:31; ::_thesis: verum
end;
consider f being Function of the carrier' of C, the carrier of (ConceptLattice C) such that
A2: for e being set st e in the carrier' of C holds
S1[e,f . e] from FUNCT_2:sch_1(A1);
take f ; ::_thesis: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) )
let o be Element of the carrier' of C; ::_thesis: ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {o}) )
thus ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( f . o = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {o} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {o}) ) by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) st ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) holds
b1 = b2
proof
let F1, F2 be Function of the carrier' of C, the carrier of (ConceptLattice C); ::_thesis: ( ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) & ( for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ) implies F1 = F2 )
assume A3: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F1 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; ::_thesis: ( ex a being Element of the carrier' of C st
for O being Subset of the carrier of C
for A being Subset of the carrier' of C holds
( not F2 . a = ConceptStr(# O,A #) or not O = (AttributeDerivation C) . {a} or not A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) or F1 = F2 )
assume A4: for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( F2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) ; ::_thesis: F1 = F2
A5: for a being set st a in the carrier' of C holds
F1 . a = F2 . a
proof
let a be set ; ::_thesis: ( a in the carrier' of C implies F1 . a = F2 . a )
assume a in the carrier' of C ; ::_thesis: F1 . a = F2 . a
then reconsider a = a as Element of the carrier' of C ;
( ex O being Subset of the carrier of C ex 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 ex 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 F1 . a = F2 . a ; ::_thesis: verum
end;
( dom F1 = the carrier' of C & dom F2 = the carrier' of C ) by FUNCT_2:def_1;
hence F1 = F2 by A5, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines delta CONLAT_2:def_5_:_
for C being FormalContext
for b2 being Function of the carrier' of C, the carrier of (ConceptLattice C) holds
( b2 = delta C iff for a being Element of the carrier' of C ex O being Subset of the carrier of C ex A being Subset of the carrier' of C st
( b2 . a = ConceptStr(# O,A #) & O = (AttributeDerivation C) . {a} & A = (ObjectDerivation C) . ((AttributeDerivation C) . {a}) ) );
theorem :: CONLAT_2:11
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; ::_thesis: 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 )
let o be Object of C; ::_thesis: for a being Attribute of C holds
( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
let a be Attribute of C; ::_thesis: ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C )
ConceptLattice C = LattStr(# (B-carrier C),(B-join C),(B-meet C) #) by CONLAT_1:def_20;
hence ( (gamma C) . o is FormalConcept of C & (delta C) . a is FormalConcept of C ) by CONLAT_1:def_15; ::_thesis: verum
end;
theorem Th12: :: CONLAT_2:12
for C being FormalContext holds
( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
proof
let C be FormalContext; ::_thesis: ( rng (gamma C) is supremum-dense & rng (delta C) is infimum-dense )
set G = rng (gamma C);
thus rng (gamma C) is supremum-dense ::_thesis: rng (delta C) is infimum-dense
proof
let a be Element of (ConceptLattice C); :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(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= rng (gamma C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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} ) } or x in rng (gamma C) )
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} ) } ; ::_thesis: x in rng (gamma C)
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 ex 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 x in rng (gamma C) by A2, A3, A4, A5, FUNCT_1:def_3; ::_thesis: verum
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 ex b1 being Element of bool (rng (gamma C)) st a = "\/" (b1,(ConceptLattice C)) by A1; ::_thesis: verum
end;
let b be Element of (ConceptLattice C); :: according to LATTICE6:def_14 ::_thesis: ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(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= rng (delta C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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}) ) } or x in rng (delta C) )
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}) ) } ; ::_thesis: x in rng (delta C)
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 ex 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 x in rng (delta C) by A7, A8, A9, A10, FUNCT_1:def_3; ::_thesis: verum
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 ex b1 being Element of bool (rng (delta C)) st b = "/\" (b1,(ConceptLattice C)) by A6; ::_thesis: verum
end;
theorem Th13: :: CONLAT_2:13
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; ::_thesis: 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 )
let o be Object of C; ::_thesis: for a being Attribute of C holds
( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
let a be Attribute of C; ::_thesis: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a )
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 ::_thesis: ( (gamma C) . o [= (delta C) . a implies o is-connected-with a )
assume o is-connected-with a ; ::_thesis: (gamma C) . o [= (delta C) . 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; ::_thesis: verum
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 ; ::_thesis: o is-connected-with 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 {a} c= (ObjectDerivation C) . ((AttributeDerivation C) . ((ObjectDerivation C) . {o})) by A2, A10, CONLAT_1:11;
then {a} c= (ObjectDerivation C) . {o} 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 o is-connected-with a ; ::_thesis: verum
end;
begin
Lm1: for L1, L2 being Lattice
for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
proof
let L1, L2 be Lattice; ::_thesis: for f being Function of the carrier of L1, the carrier of L2 st ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) holds
f is one-to-one
let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( ( for a, b being Element of L1 st f . a [= f . b holds
a [= b ) implies f is one-to-one )
assume A1: for a, b being Element of L1 st f . a [= f . b holds
a [= b ; ::_thesis: f is one-to-one
let x, y be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume that
A2: x in dom f and
A3: y in dom f and
A4: f . x = f . y ; ::_thesis: x = y
reconsider y = y as Element of L1 by A3;
reconsider x = x as Element of L1 by A2;
( x [= y & y [= x ) by A1, A4;
hence x = y by LATTICES:8; ::_thesis: verum
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 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
proof
let L1, L2 be complete Lattice; ::_thesis: 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 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) holds
f is Homomorphism of L1,L2
let f be Function of the carrier of L1, the carrier of L2; ::_thesis: ( f is one-to-one & rng f = the carrier of L2 & ( for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ) implies f is Homomorphism of L1,L2 )
assume A1: ( f is one-to-one & rng f = the carrier of L2 ) ; ::_thesis: ( ex a, b being Element of L1 st
( ( a [= b implies f . a [= f . b ) implies ( f . a [= f . b & not a [= b ) ) or f is Homomorphism of L1,L2 )
assume A2: for a, b being Element of L1 holds
( a [= b iff f . a [= f . b ) ; ::_thesis: f is Homomorphism of L1,L2
A3: for a, b being Element of L1 holds f . (a "/\" b) = (f . a) "/\" (f . b)
proof
let a, b be Element of L1; ::_thesis: f . (a "/\" b) = (f . a) "/\" (f . b)
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; ::_thesis: ( r is_less_than {(f . a),(f . b)} implies r [= f . (a "/\" b) )
assume A6: r is_less_than {(f . a),(f . b)} ; ::_thesis: r [= f . (a "/\" 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, LATTICE3:def_16;
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, LATTICE3:def_16;
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} by LATTICE3:def_16;
a "/\" b = "/\" {a,b} by LATTICE3:43;
then g . r [= a "/\" b by A9, LATTICE3:34;
hence r [= f . (a "/\" b) by A2, A7; ::_thesis: verum
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)} by LATTICE3:def_16;
then f . (a "/\" b) = "/\" ({(f . a),(f . b)},L2) by A5, LATTICE3:34;
hence f . (a "/\" b) = (f . a) "/\" (f . b) by LATTICE3:43; ::_thesis: verum
end;
for a, b being Element of L1 holds f . (a "\/" b) = (f . a) "\/" (f . b)
proof
let a, b be Element of L1; ::_thesis: f . (a "\/" b) = (f . a) "\/" (f . b)
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; ::_thesis: ( {(f . a),(f . b)} is_less_than r implies f . (a "\/" b) [= r )
assume A12: {(f . a),(f . b)} is_less_than r ; ::_thesis: f . (a "\/" b) [= 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, LATTICE3:def_17;
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, LATTICE3:def_17;
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 by LATTICE3:def_17;
a "\/" b = "\/" {a,b} by LATTICE3:43;
then a "\/" b [= g . r by A15, LATTICE3:def_21;
hence f . (a "\/" b) [= r by A2, A13; ::_thesis: verum
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) by LATTICE3:def_17;
then f . (a "\/" b) = "\/" ({(f . a),(f . b)},L2) by A11, LATTICE3:def_21;
hence f . (a "\/" b) = (f . a) "\/" (f . b) by LATTICE3:43; ::_thesis: verum
end;
hence f is Homomorphism of L1,L2 by A3, LATTICE4:def_1; ::_thesis: verum
end;
Lm3: for C being FormalContext
for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
proof
let C be FormalContext; ::_thesis: for CS being ConceptStr over C st (ObjectDerivation C) . the Extent of CS = the Intent of CS holds
not CS is empty
let CS be ConceptStr over C; ::_thesis: ( (ObjectDerivation C) . the Extent of CS = the Intent of CS implies not CS is empty )
assume A1: (ObjectDerivation C) . the Extent of CS = the Intent of CS ; ::_thesis: not CS is empty
percases ( the Extent of CS is empty or not the Extent of CS is empty ) ;
suppose the Extent of CS is empty ; ::_thesis: not CS is empty
then the Intent of CS = the carrier' of C by A1, CONLAT_1:17;
hence not CS is empty by CONLAT_1:def_8; ::_thesis: verum
end;
suppose not the Extent of CS is empty ; ::_thesis: not CS is empty
hence not CS is empty by CONLAT_1:def_8; ::_thesis: verum
end;
end;
end;
theorem Th14: :: CONLAT_2:14
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 ex 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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )
proof
let L be complete Lattice; ::_thesis: for C being FormalContext holds
( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex 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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )
let C be FormalContext; ::_thesis: ( ConceptLattice C,L are_isomorphic iff ex g being Function of the carrier of C, the carrier of L ex 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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) )
hereby ::_thesis: ( ex g being Function of the carrier of C, the carrier of L ex 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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ) ) implies ConceptLattice C,L are_isomorphic )
assume ConceptLattice C,L are_isomorphic ; ::_thesis: ex g being Element of bool [: the carrier of C, the carrier of L:] ex d being Element of bool [: 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
for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
then consider f being Homomorphism of ConceptLattice C,L such that
A1: f is bijective by LATTICE4:def_2;
take g = f * (gamma C); ::_thesis: ex d being Element of bool [: 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
for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
take d = f * (delta C); ::_thesis: ( rng g is supremum-dense & rng d is infimum-dense & ( for o being Object of C
for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
thus rng g is supremum-dense ::_thesis: ( rng d is infimum-dense & ( for o being Object of C
for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) ) ) )
proof
let a be Element of L; :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng g) st a = "\/" (b1,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)) by LATTICE6:def_13;
set D = { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ;
A4: for r being Element of L st { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r holds
a [= r
proof
let r be Element of L; ::_thesis: ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r implies a [= r )
consider r9 being Element of (ConceptLattice C) such that
A5: r = f . r9 by A1, LATTICE4:6;
reconsider r9 = r9 as Element of (ConceptLattice C) ;
assume A6: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than r ; ::_thesis: a [= r
for q being Element of (ConceptLattice C) st q in D9 holds
q [= r9
proof
let q be Element of (ConceptLattice C); ::_thesis: ( q in D9 implies q [= r9 )
assume q in D9 ; ::_thesis: q [= r9
then f . q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ;
then f . q [= f . r9 by A6, A5, LATTICE3:def_17;
hence q [= r9 by A1, LATTICE4:5; ::_thesis: verum
end;
then D9 is_less_than r9 by LATTICE3:def_17;
then b [= r9 by A3, LATTICE3:def_21;
hence a [= r by A1, A2, A5, LATTICE4:5; ::_thesis: verum
end;
A7: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng g
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or x in rng g )
assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: x in rng g
then consider x9 being Element of (ConceptLattice C) such that
A8: x = f . x9 and
A9: x9 in D9 ;
consider y being set 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 x in rng g by A11, FUNCT_1:def_3; ::_thesis: verum
end;
A12: D9 is_less_than b by A3, LATTICE3:def_21;
{ (f . x) where x is Element of (ConceptLattice C) : x in D9 } is_less_than a
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or q [= a )
assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: q [= a
then consider q9 being Element of (ConceptLattice C) such that
A13: q = f . q9 and
A14: q9 in D9 ;
q9 [= b by A12, A14, LATTICE3:def_17;
hence q [= a by A1, A2, A13, LATTICE4:5; ::_thesis: verum
end;
then a = "\/" ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ,L) by A4, LATTICE3:def_21;
hence ex b1 being Element of bool (rng g) st a = "\/" (b1,L) by A7; ::_thesis: verum
end;
thus rng d is infimum-dense ::_thesis: for o being Object of C
for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )
proof
let a be Element of L; :: according to LATTICE6:def_14 ::_thesis: ex b1 being Element of bool (rng d) st a = "/\" (b1,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)) by LATTICE6:def_14;
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 { (f . x) where x is Element of (ConceptLattice C) : x in D9 } holds
r [= a
proof
let r be Element of L; ::_thesis: ( r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 } implies r [= a )
consider r9 being Element of (ConceptLattice C) such that
A18: r = f . r9 by A1, LATTICE4:6;
reconsider r9 = r9 as Element of (ConceptLattice C) ;
assume A19: r is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: r [= a
r9 is_less_than D9
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in D9 or r9 [= q )
assume q in D9 ; ::_thesis: r9 [= q
then f . q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ;
then f . r9 [= f . q by A19, A18, LATTICE3:def_16;
hence r9 [= q by A1, LATTICE4:5; ::_thesis: verum
end;
then r9 [= b by A16, LATTICE3:34;
hence r [= a by A1, A15, A18, LATTICE4:5; ::_thesis: verum
end;
A20: { (f . x) where x is Element of (ConceptLattice C) : x in D9 } c= rng d
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or x in rng d )
assume x in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: x in rng d
then consider x9 being Element of (ConceptLattice C) such that
A21: x = f . x9 and
A22: x9 in D9 ;
consider y being set 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 x in rng d by A24, FUNCT_1:def_3; ::_thesis: verum
end;
A25: b is_less_than D9 by A16, LATTICE3:34;
a is_less_than { (f . x) where x is Element of (ConceptLattice C) : x in D9 }
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } or a [= q )
assume q in { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ; ::_thesis: a [= q
then consider q9 being Element of (ConceptLattice C) such that
A26: q = f . q9 and
A27: q9 in D9 ;
b [= q9 by A25, A27, LATTICE3:def_16;
hence a [= q by A1, A15, A26, LATTICE4:5; ::_thesis: verum
end;
then a = "/\" ( { (f . x) where x is Element of (ConceptLattice C) : x in D9 } ,L) by A17, LATTICE3:34;
hence ex b1 being Element of bool (rng d) st a = "/\" (b1,L) by A20; ::_thesis: verum
end;
let o be Object of C; ::_thesis: for a being Attribute of C holds
( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )
let a be Attribute of C; ::_thesis: ( ( o is-connected-with a implies g . o [= d . a ) & ( g . o [= d . a implies o is-connected-with a ) )
A28: ( o is-connected-with a iff (gamma C) . o [= (delta C) . a ) by Th13;
hereby ::_thesis: ( g . o [= d . a implies o is-connected-with a )
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 ; ::_thesis: g . o [= d . a
hence g . o [= d . a by A1, A28, A30, A29, LATTICE4:5; ::_thesis: verum
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 ; ::_thesis: o is-connected-with a
then (gamma C) . o [= (delta C) . a by A1, A31, A32, LATTICE4:5;
hence o is-connected-with a by Th13; ::_thesis: verum
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
for a being Attribute of C holds
( o is-connected-with a iff g . o [= d . a ) ; ::_thesis: ConceptLattice C,L are_isomorphic
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: { [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) ) } c= [: the carrier of (ConceptLattice C), the carrier of L:]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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) ) } or y in [: the carrier of (ConceptLattice C), the carrier of L:] )
assume y in { [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) ) } ; ::_thesis: y in [: the carrier of (ConceptLattice C), the carrier of L:]
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 y in [: the carrier of (ConceptLattice C), the carrier of L:] by A38, ZFMISC_1:def_2; ::_thesis: verum
end;
{ [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 } ) } c= [: the carrier of L, the carrier of (ConceptLattice C):]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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 } ) } or y in [: the carrier of L, the carrier of (ConceptLattice C):] )
assume y in { [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 } ) } ; ::_thesis: y in [: the carrier of L, the carrier of (ConceptLattice C):]
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 #) :: according to XBOOLE_0:def_10 ::_thesis: the Extent of ConceptStr(# O,A #) c= (AttributeDerivation C) . the Intent of ConceptStr(# O,A #)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) or u in the Extent of ConceptStr(# O,A #) )
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, LATTICE6:def_14;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } )
assume A47: u in D ; ::_thesis: u in { (d . a9) where a9 is Attribute of C : x [= d . a9 }
then consider v being set such that
A48: v in dom d and
A49: u = d . v by FUNCT_1:def_3;
reconsider v = v as Attribute of C by A48;
x [= d . v by A46, A47, A49, LATTICE3:def_16;
hence u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } by A49; ::_thesis: verum
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; :: according to LATTICE3:def_16 ::_thesis: ( not u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } or x [= u )
assume u in { (d . a9) where a9 is Attribute of C : x [= d . a9 } ; ::_thesis: x [= u
then ex v being Attribute of C st
( u = d . v & x [= d . v ) ;
hence x [= u ; ::_thesis: verum
end;
then x [= "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) by LATTICE3:39;
hence "/\" ( { (d . a9) where a9 is Attribute of C : x [= d . a9 } ,L) = x by A50, LATTICES:8; ::_thesis: verum
end;
assume u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) ; ::_thesis: u in the Extent 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
proof
let v be Attribute of C; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies g . u9 [= d . v )
assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= d . v
then u9 is-connected-with v by A42, A52;
hence g . u9 [= d . v by A35; ::_thesis: verum
end;
g . u9 is_less_than { (d . a) where a is Attribute of C : x [= d . a }
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (d . a) where a is Attribute of C : x [= d . a } or g . u9 [= q )
assume q in { (d . a) where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= q
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 g . u9 [= q by A53, A54; ::_thesis: verum
end;
then g . u9 [= x by A44, LATTICE3:34;
hence u in the Extent of ConceptStr(# O,A #) by A41, A51; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the Extent of ConceptStr(# O,A #) or u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) )
assume u in the Extent of ConceptStr(# O,A #) ; ::_thesis: u in (AttributeDerivation C) . the Intent 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; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies g . u9 [= d . v )
assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: g . u9 [= d . v
then ex v9 being Attribute of C st
( v9 = v & x [= d . v9 ) ;
hence g . u9 [= d . v by A57, LATTICES:7; ::_thesis: verum
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; ::_thesis: ( v in { a where a is Attribute of C : x [= d . a } implies u9 is-connected-with v )
assume v in { a where a is Attribute of C : x [= d . a } ; ::_thesis: u9 is-connected-with v
then g . u9 [= d . v by A58;
hence u9 is-connected-with v by A35; ::_thesis: verum
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 u in (AttributeDerivation C) . the Intent of ConceptStr(# O,A #) by A56, CONLAT_1:def_4; ::_thesis: verum
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 #) :: according to XBOOLE_0:def_10 ::_thesis: the Intent of ConceptStr(# O,A #) c= (ObjectDerivation C) . the Extent of ConceptStr(# O,A #)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) or u in the Intent of ConceptStr(# O,A #) )
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, LATTICE6:def_13;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (g . a9) where a9 is Object of C : g . a9 [= x } )
assume A62: u in D ; ::_thesis: u in { (g . a9) where a9 is Object of C : g . a9 [= x }
then consider v being set such that
A63: v in dom g and
A64: u = g . v by FUNCT_1:def_3;
reconsider v = v as Object of C by A63;
g . v [= x by A61, A62, A64, LATTICE3:def_17;
hence u in { (g . a9) where a9 is Object of C : g . a9 [= x } by A64; ::_thesis: verum
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; :: according to LATTICE3:def_17 ::_thesis: ( not u in { (g . a9) where a9 is Object of C : g . a9 [= x } or u [= x )
assume u in { (g . a9) where a9 is Object of C : g . a9 [= x } ; ::_thesis: u [= x
then ex v being Object of C st
( u = g . v & g . v [= x ) ;
hence u [= x ; ::_thesis: verum
end;
then "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) [= x by LATTICE3:def_21;
hence "\/" ( { (g . a9) where a9 is Object of C : g . a9 [= x } ,L) = x by A65, LATTICES:8; ::_thesis: verum
end;
assume u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) ; ::_thesis: u in the Intent 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
proof
let v be Object of C; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies g . v [= d . u9 )
assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: g . v [= d . u9
then v is-connected-with u9 by A41, A67;
hence g . v [= d . u9 by A35; ::_thesis: verum
end;
{ (g . a) where a is Object of C : g . a [= x } is_less_than d . u9
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (g . a) where a is Object of C : g . a [= x } or q [= d . u9 )
assume q in { (g . a) where a is Object of C : g . a [= x } ; ::_thesis: q [= d . u9
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 q [= d . u9 by A68, A69; ::_thesis: verum
end;
then x [= d . u9 by A59, LATTICE3:def_21;
hence u in the Intent of ConceptStr(# O,A #) by A42, A66; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the Intent of ConceptStr(# O,A #) or u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) )
assume u in the Intent of ConceptStr(# O,A #) ; ::_thesis: u in (ObjectDerivation C) . the Extent 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; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies g . v [= d . u9 )
assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: g . v [= d . u9
then ex v9 being Object of C st
( v9 = v & g . v9 [= x ) ;
hence g . v [= d . u9 by A72, LATTICES:7; ::_thesis: verum
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; ::_thesis: ( v in { a where a is Object of C : g . a [= x } implies v is-connected-with u9 )
assume v in { a where a is Object of C : g . a [= x } ; ::_thesis: v is-connected-with u9
then g . v [= d . u9 by A73;
hence v is-connected-with u9 by A35; ::_thesis: verum
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 u in (ObjectDerivation C) . the Extent of ConceptStr(# O,A #) by A71, CONLAT_1:def_3; ::_thesis: verum
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 y in [: the carrier of L, the carrier of (ConceptLattice C):] by A40, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider 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 } ) } as Relation of the carrier of L, the carrier of (ConceptLattice C) ;
A74: for x, y1, y2 being set st [x,y1] in fi & [x,y2] in fi holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in fi & [x,y2] in fi implies y1 = y2 )
assume that
A75: [x,y1] in fi and
A76: [x,y2] in fi ; ::_thesis: y1 = y2
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 ; ::_thesis: verum
end;
the carrier of L c= dom fi
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of L or y in dom fi )
assume y in the carrier of L ; ::_thesis: y in dom fi
then reconsider y = y as Element of L ;
set A = { a where a is Attribute of C : y [= d . a } ;
{ a where a is Attribute of C : y [= d . a } c= the carrier' of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : y [= d . a } or u in the carrier' of C )
assume u in { a where a is Attribute of C : y [= d . a } ; ::_thesis: u in the carrier' of C
then ex u9 being Attribute of C st
( u9 = u & y [= d . u9 ) ;
hence u in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = { a where a is Attribute of C : y [= d . a } as Subset of the carrier' of C ;
set O = { o where o is Object of C : g . o [= y } ;
{ o where o is Object of C : g . o [= y } c= the carrier of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= y } or u in the carrier of C )
assume u in { o where o is Object of C : g . o [= y } ; ::_thesis: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & g . u9 [= y ) ;
hence u in the carrier of C ; ::_thesis: verum
end;
then reconsider O = { o where o is Object of C : g . o [= y } as Subset of the carrier of C ;
[y,ConceptStr(# O,A #)] in fi ;
hence y in dom fi by XTUPLE_0:def_12; ::_thesis: verum
end;
then A82: the carrier of L = dom fi by XBOOLE_0:def_10;
reconsider 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) ) } 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of (ConceptLattice C) or y in dom f )
assume y in the carrier of (ConceptLattice C) ; ::_thesis: y in dom f
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 y in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A85: the carrier of (ConceptLattice C) = dom f by XBOOLE_0:def_10;
reconsider fi = 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 set st [x,y1] in f & [x,y2] in f holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume that
A86: [x,y1] in f and
A87: [x,y2] in f ; ::_thesis: y1 = y2
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 ; ::_thesis: verum
end;
then reconsider f = 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; ::_thesis: f . (fi . a) = a
reconsider a = a as Element of L ;
set A = { a9 where a9 is Attribute of C : a [= d . a9 } ;
{ a9 where a9 is Attribute of C : a [= d . a9 } c= the carrier' of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a9 where a9 is Attribute of C : a [= d . a9 } or u in the carrier' of C )
assume u in { a9 where a9 is Attribute of C : a [= d . a9 } ; ::_thesis: u in the carrier' of C
then ex u9 being Attribute of C st
( u9 = u & a [= d . u9 ) ;
hence u in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = { a9 where a9 is Attribute of C : a [= d . a9 } as Subset of the carrier' of C ;
set O = { o where o is Object of C : g . o [= a } ;
{ o where o is Object of C : g . o [= a } c= the carrier of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= a } or u in the carrier of C )
assume u in { o where o is Object of C : g . o [= a } ; ::_thesis: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & g . u9 [= a ) ;
hence u in the carrier of C ; ::_thesis: verum
end;
then reconsider O = { o where o is Object of C : g . o [= a } 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, LATTICE6:def_13;
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } )
assume A98: u in D ; ::_thesis: 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 set such that
A99: v in dom g and
A100: u = g . v by FUNCT_1:def_3;
reconsider v = v as Object of C by A99;
g . v [= a by A97, A98, A100, LATTICE3:def_17;
then v in { o9 where o9 is Object of C : g . o9 [= a } ;
hence u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } by A100; ::_thesis: verum
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; :: according to LATTICE3:def_17 ::_thesis: ( not u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } or u [= a )
assume u in { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ; ::_thesis: u [= 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 u [= a by A102; ::_thesis: verum
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 "\/" ( { (g . o) where o is Object of C : o in { o9 where o9 is Object of C : g . o9 [= a } } ,L) = a by A101, LATTICES:8; ::_thesis: verum
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 #),("\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L))] in f ;
then f . ConceptStr(# O,A #) = "\/" ( { (g . o) where o is Object of C : o in the Extent of ConceptStr(# O,A #) } ,L) by FUNCT_1:1;
hence f . (fi . a) = a by A104, A95, FUNCT_1:1; ::_thesis: verum
end;
the carrier of L c= rng f
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of L or u in rng f )
A105: dom f = the carrier of (ConceptLattice C) by FUNCT_2:def_1;
assume A106: u in the carrier of L ; ::_thesis: u in rng f
then u in dom fi by FUNCT_2:def_1;
then consider v being set such that
A107: [u,v] in fi by XTUPLE_0:def_12;
reconsider u = u as Element of L by A106;
v in rng fi by A107, XTUPLE_0:def_13;
then reconsider v = v as Element of (ConceptLattice C) ;
f . v = f . (fi . u) by A107, FUNCT_1:1
.= u by A94 ;
hence u in rng f by A105, FUNCT_1:def_3; ::_thesis: verum
end;
then A108: rng f = the carrier of L by XBOOLE_0:def_10;
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); ::_thesis: f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L)
set y = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L);
A110: [(x @),("\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L))] in f ;
A111: for o being set st o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } holds
o in { (d . a) where a is Attribute of C : a in the Intent of (x @) }
proof
let o be set ; ::_thesis: ( o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } implies o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } )
assume o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ; ::_thesis: o in { (d . a) where a is Attribute of C : a in the Intent of (x @) }
then consider u being Attribute of C such that
A112: o = d . u and
A113: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= 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; ::_thesis: ( o in the Extent of (x @) implies g . o [= d . u )
assume o in the Extent of (x @) ; ::_thesis: g . o [= d . u
then g . o in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } ;
then g . o [= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by LATTICE3:38;
hence g . o [= d . u by A113, LATTICES:7; ::_thesis: verum
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; ::_thesis: ( o in the Extent of (x @) implies o is-connected-with u )
assume o in the Extent of (x @) ; ::_thesis: o is-connected-with u
then g . o [= d . u by A114;
hence o is-connected-with u by A35; ::_thesis: verum
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 o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } by A112; ::_thesis: verum
end;
A115: for o9 being Object of C st o9 in the Extent of (x @) holds
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; ::_thesis: ( o9 in the Extent of (x @) implies for a9 being Attribute of C st a9 in the Intent of (x @) holds
g . o9 [= d . a9 )
assume A116: o9 in the Extent of (x @) ; ::_thesis: for a9 being Attribute of C st a9 in the Intent of (x @) holds
g . o9 [= d . a9
let a9 be Attribute of C; ::_thesis: ( a9 in the Intent of (x @) implies g . o9 [= d . a9 )
assume a9 in the Intent of (x @) ; ::_thesis: g . o9 [= d . a9
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 g . o9 [= d . a9 by A35; ::_thesis: verum
end;
A117: for o being set st o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } holds
o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }
proof
let o be set ; ::_thesis: ( 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 : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } )
assume o in { (d . a) where a is Attribute of C : a in the Intent of (x @) } ; ::_thesis: o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }
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; :: according to LATTICE3:def_17 ::_thesis: ( not q in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } or q [= d . b )
assume q in { (g . o9) where o9 is Object of C : o9 in the Extent of (x @) } ; ::_thesis: q [= d . b
then ex u being Object of C st
( q = g . u & u in the Extent of (x @) ) ;
hence q [= d . b by A115, A119; ::_thesis: verum
end;
then "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . b by LATTICE3:def_21;
hence o in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } by A118; ::_thesis: verum
end;
A120: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L)
proof
consider D being Subset of (rng d) such that
A121: "/\" (D,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A34, LATTICE6:def_14;
A122: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than D by A121, LATTICE3:34;
D c= { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in D or u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } )
assume A123: u in D ; ::_thesis: u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }
then consider v being set such that
A124: v in dom d and
A125: u = d . v by FUNCT_1:def_3;
reconsider v = v as Attribute of C by A124;
"\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . v by A122, A123, A125, LATTICE3:def_16;
hence u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } by A125; ::_thesis: verum
end;
then A126: "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) [= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A121, LATTICE3:45;
"\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) is_less_than { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 }
proof
let u be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } or "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u )
assume u in { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ; ::_thesis: "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u
then ex v being Attribute of C st
( u = d . v & "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . v ) ;
hence "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= u ; ::_thesis: verum
end;
then "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) by LATTICE3:39;
hence "/\" ( { (d . a9) where a9 is Attribute of C : "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) [= d . a9 } ,L) = "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A126, LATTICES:8; ::_thesis: verum
end;
f . x = f . (x @) by CONLAT_1:def_21
.= "\/" ( { (g . o) where o is Object of C : o in the Extent of (x @) } ,L) by A110, FUNCT_1:1 ;
hence f . x = "/\" ( { (d . a) where a is Attribute of C : a in the Intent of (x @) } ,L) by A111, A117, A120, TARSKI:1; ::_thesis: verum
end;
A127: for a being Element of (ConceptLattice C) holds fi . (f . a) = a
proof
let a be Element of (ConceptLattice C); ::_thesis: fi . (f . a) = a
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 : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } ;
{ a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } c= the carrier' of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } or u in the carrier' of C )
assume u in { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } ; ::_thesis: u in the carrier' of C
then ex u9 being Attribute of C st
( u9 = u & "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . u9 ) ;
hence u in the carrier' of C ; ::_thesis: verum
end;
then reconsider A = { a9 where a9 is Attribute of C : "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 } as Subset of the carrier' of C ;
set O = { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } ;
{ o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } c= the carrier of C
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } or u in the carrier of C )
assume u in { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } ; ::_thesis: u in the carrier of C
then ex u9 being Object of C st
( u9 = u & g . u9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) ) ;
hence u in the carrier of C ; ::_thesis: verum
end;
then reconsider O = { o where o is Object of C : g . o [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) } 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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in O or 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 } )
assume u in O ; ::_thesis: 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
A129: u = o9 and
A130: g . o9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) ;
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; ::_thesis: ( a9 in the Intent of (a @) implies g . o9 [= d . a9 )
assume a9 in the Intent of (a @) ; ::_thesis: g . o9 [= d . a9
then d . a9 in { (d . y) where y is Attribute of C : y in the Intent of (a @) } ;
then "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) [= d . a9 by LATTICE3:38;
hence g . o9 [= d . a9 by A130, LATTICES:7; ::_thesis: verum
end;
hence 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 } by A129; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or u in O )
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 } ; ::_thesis: u in O
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; :: according to LATTICE3:def_16 ::_thesis: ( not q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } or g . o9 [= q )
assume q in { (d . y) where y is Attribute of C : y in the Intent of (a @) } ; ::_thesis: g . o9 [= q
then ex qa being Attribute of C st
( q = d . qa & qa in the Intent of (a @) ) ;
hence g . o9 [= q by A132; ::_thesis: verum
end;
then g . o9 [= "/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L) by LATTICE3:34;
hence u in O by A131; ::_thesis: verum
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 } :: according to XBOOLE_0:def_10 ::_thesis: { 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 } 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } )
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 } ; ::_thesis: 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
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; ::_thesis: ( a9 in the Intent of (a @) implies u9 is-connected-with a9 )
assume a9 in the Intent of (a @) ; ::_thesis: u9 is-connected-with a9
then g . u9 [= d . a9 by A134;
hence u9 is-connected-with a9 by A35; ::_thesis: verum
end;
hence 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 } by A133; ::_thesis: verum
end;
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not 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 } or 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 } )
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 } ; ::_thesis: 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
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
proof
let a9 be Attribute of C; ::_thesis: ( a9 in the Intent of (a @) implies g . u9 [= d . a9 )
assume a9 in the Intent of (a @) ; ::_thesis: g . u9 [= d . a9
then u9 is-connected-with a9 by A136;
hence g . u9 [= d . a9 by A35; ::_thesis: verum
end;
hence 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 } by A135; ::_thesis: verum
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;
[("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)),ConceptStr(# O,A #)] in fi ;
then A139: fi . ("/\" ( { (d . u) where u is Attribute of C : u in the Intent of (a @) } ,L)) = 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 fi . (f . a) = a by A138, A139, A137, CONLAT_1:def_21; ::_thesis: verum
end;
A140: for a, b being Element of L st a [= b holds
fi . a [= fi . b
proof
let a, b be Element of L; ::_thesis: ( a [= b implies fi . a [= fi . b )
set ca = fi . a;
set cb = fi . b;
assume A141: a [= b ; ::_thesis: fi . a [= fi . 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { o where o is Object of C : g . o [= a } or x in { o where o is Object of C : g . o [= b } )
assume x in { o where o is Object of C : g . o [= a } ; ::_thesis: x in { o where o is Object of C : g . o [= b }
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 x in { o where o is Object of C : g . o [= b } by A143; ::_thesis: verum
end;
A145: dom fi = the carrier of L by FUNCT_2:def_1;
then consider ya being set such that
A146: [a,ya] in fi by XTUPLE_0:def_12;
consider yb being set 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 ((fi . b) @) = 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 ((fi . a) @) = Oa by CONLAT_1:def_21;
then (fi . a) @ is-SubConcept-of (fi . b) @ by A142, A153, A149, A154, A150, A151, CONLAT_1:def_16;
hence fi . a [= fi . b by CONLAT_1:43; ::_thesis: verum
end;
A155: for a, b being Element of (ConceptLattice C) st f . a [= f . b holds
a [= b
proof
let a, b be Element of (ConceptLattice C); ::_thesis: ( f . a [= f . b implies a [= b )
assume A156: f . a [= f . b ; ::_thesis: a [= b
( fi . (f . a) = a & fi . (f . b) = b ) by A127;
hence a [= b by A140, A156; ::_thesis: verum
end;
for a, b being Element of (ConceptLattice C) st a [= b holds
f . a [= f . b
proof
let a, b be Element of (ConceptLattice C); ::_thesis: ( a [= b implies f . a [= f . b )
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 ; ::_thesis: f . a [= f . 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (g . o) where o is Object of C : o in the Extent of (a @) } or x in { (g . o) where o is Object of C : o in the Extent of (b @) } )
assume x in { (g . o) where o is Object of C : o in the Extent of (a @) } ; ::_thesis: x in { (g . o) where o is Object of C : o in the Extent of (b @) }
then ex o being Object of C st
( x = g . o & o in the Extent of (a @) ) ;
hence x in { (g . o) where o is Object of C : o in the Extent of (b @) } by A159; ::_thesis: verum
end;
( a @ = a & b @ = b ) by CONLAT_1:def_21;
hence f . a [= f . b by A160, A157, A158, LATTICE3:45; ::_thesis: verum
end;
then reconsider f = 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 ConceptLattice C,L are_isomorphic by A161, LATTICE4:def_2; ::_thesis: verum
end;
definition
let L be Lattice;
func Context L -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 6
ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);
coherence
ContextStr(# the carrier of L, the carrier of L,(LattRel L) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1;
end;
:: deftheorem defines Context CONLAT_2:def_6_:_
for L being Lattice holds Context L = ContextStr(# the carrier of L, the carrier of L,(LattRel L) #);
theorem Th15: :: CONLAT_2:15
for L being complete Lattice holds ConceptLattice (Context L),L are_isomorphic
proof
let L be complete Lattice; ::_thesis: ConceptLattice (Context L),L are_isomorphic
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)
for 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); ::_thesis: for a being Attribute of (Context L) holds
( o is-connected-with a iff g . o [= d . a )
let a be Attribute of (Context L); ::_thesis: ( o is-connected-with a iff g . o [= d . a )
reconsider o9 = o, a9 = a as Element of L ;
A2: ( g . o = o9 & d . a = a9 ) by FUNCT_1:17;
( o is-connected-with a iff [o,a] in the Information of (Context L) ) by CONLAT_1:def_2;
hence ( o is-connected-with a iff g . o [= d . a ) by A2, FILTER_1:31; ::_thesis: verum
end;
for a being Element of L ex D9 being Subset of (rng d) st a = "/\" (D9,L)
proof
let a be Element of L; ::_thesis: ex D9 being Subset of (rng d) st a = "/\" (D9,L)
( "/\" ({a},L) = a & rng d = the carrier of L ) by LATTICE3:42, RELAT_1:45;
hence ex D9 being Subset of (rng d) st a = "/\" (D9,L) ; ::_thesis: verum
end;
then A3: rng d is infimum-dense by LATTICE6:def_14;
rng g is supremum-dense
proof
let a be Element of L; :: according to LATTICE6:def_13 ::_thesis: ex b1 being Element of bool (rng g) st a = "\/" (b1,L)
( "\/" ({a},L) = a & rng g = the carrier of L ) by LATTICE3:42, RELAT_1:45;
hence ex b1 being Element of bool (rng g) st a = "\/" (b1,L) ; ::_thesis: verum
end;
hence ConceptLattice (Context L),L are_isomorphic by A3, A1, Th14; ::_thesis: verum
end;
theorem :: CONLAT_2:16
for L being Lattice holds
( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )
proof
let L be Lattice; ::_thesis: ( L is complete iff ex C being FormalContext st ConceptLattice C,L are_isomorphic )
hereby ::_thesis: ( ex C being FormalContext st ConceptLattice C,L are_isomorphic implies L is complete )
assume L is complete ; ::_thesis: ex C being FormalContext st ConceptLattice C,L are_isomorphic
then ConceptLattice (Context L),L are_isomorphic by Th15;
hence ex C being FormalContext st ConceptLattice C,L are_isomorphic ; ::_thesis: verum
end;
given C being FormalContext such that A1: ConceptLattice C,L are_isomorphic ; ::_thesis: L is complete
let X be Subset of L; :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of L st
( b1 is_less_than X & ( for b2 being Element of the carrier of L holds
( not b2 is_less_than X or b2 [= b1 ) ) )
consider f being Homomorphism of L, ConceptLattice C such that
A2: f is bijective by A1, LATTICE4:def_2;
set FX = { (f . x) where x is Element of L : x in X } ;
{ (f . x) where x is Element of L : x in X } c= the carrier of (ConceptLattice C)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (f . x) where x is Element of L : x in X } or x in the carrier of (ConceptLattice C) )
assume x in { (f . x) where x is Element of L : x in X } ; ::_thesis: x in the carrier of (ConceptLattice C)
then ex y being Element of L st
( x = f . y & y in X ) ;
hence x in the carrier of (ConceptLattice C) ; ::_thesis: verum
end;
then reconsider FX = { (f . x) where x is Element of L : x in X } as Subset of (ConceptLattice C) ;
set Fa = "/\" (FX,(ConceptLattice C));
consider a being Element of L such that
A3: "/\" (FX,(ConceptLattice C)) = 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; ::_thesis: ( b is_less_than X implies b [= a )
assume A5: b is_less_than X ; ::_thesis: b [= a
f . b is_less_than FX
proof
let q be Element of (ConceptLattice C); :: according to LATTICE3:def_16 ::_thesis: ( not q in FX or f . b [= q )
assume q in FX ; ::_thesis: f . b [= q
then consider y being Element of L such that
A6: q = f . y and
A7: y in X ;
b [= y by A5, A7, LATTICE3:def_16;
hence f . b [= q by A2, A6, LATTICE4:5; ::_thesis: verum
end;
then f . b [= f . a by A3, LATTICE3:34;
hence b [= a by A2, LATTICE4:5; ::_thesis: verum
end;
A8: "/\" (FX,(ConceptLattice C)) is_less_than FX by LATTICE3:34;
a is_less_than X
proof
let q be Element of L; :: according to LATTICE3:def_16 ::_thesis: ( not q in X or a [= q )
assume q in X ; ::_thesis: a [= q
then f . q in FX ;
then "/\" (FX,(ConceptLattice C)) [= f . q by A8, LATTICE3:def_16;
hence a [= q by A2, A3, LATTICE4:5; ::_thesis: verum
end;
hence ex b1 being Element of the carrier of L st
( b1 is_less_than X & ( for b2 being Element of the carrier of L holds
( not b2 is_less_than X or b2 [= b1 ) ) ) by A4; ::_thesis: verum
end;
begin
registration
let L be complete Lattice;
clusterL .: -> complete ;
coherence
L .: is complete
proof
let X be Subset of (L .:); :: according to VECTSP_8:def_6 ::_thesis: ex b1 being Element of the carrier of (L .:) st
( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds
( not b2 is_less_than X or b2 [= b1 ) ) )
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 = "\/" (X9,L) 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 .:); ::_thesis: ( b is_less_than X implies b [= a )
reconsider b9 = b as Element of L by A1;
assume A4: b is_less_than X ; ::_thesis: b [= a
X9 is_less_than b9
proof
let q be Element of L; :: according to LATTICE3:def_17 ::_thesis: ( not q in X9 or q [= b9 )
reconsider q9 = q as Element of (L .:) by A1;
assume q in X9 ; ::_thesis: q [= b9
then b [= q9 by A4, LATTICE3:def_16;
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 q [= b9 by LATTICE3:7; ::_thesis: verum
end;
then "\/" (X9,L) [= b9 by LATTICE3:def_21;
then ("\/" (X9,L)) % <= b9 % by LATTICE3:7;
then [(("\/" (X9,L)) %),(b9 %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def_5;
then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def_7;
then [(b9 %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20;
then b % <= a % by ORDERS_2:def_5;
hence b [= a by LATTICE3:7; ::_thesis: verum
end;
A5: X9 is_less_than "\/" (X9,L) by LATTICE3:def_21;
a is_less_than X
proof
let q9 be Element of (L .:); :: according to LATTICE3:def_16 ::_thesis: ( not q9 in X or a [= q9 )
reconsider q = q9 as Element of L by A1;
assume q9 in X ; ::_thesis: a [= q9
then q [= "\/" (X9,L) by A5, LATTICE3:def_17;
then q % <= ("\/" (X9,L)) % by LATTICE3:7;
then [(q %),(("\/" (X9,L)) %)] in the InternalRel of (LattPOSet L) by ORDERS_2:def_5;
then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet L) ~ by RELAT_1:def_7;
then [(("\/" (X9,L)) %),(q %)] in the InternalRel of (LattPOSet (L .:)) by LATTICE3:20;
then a % <= q9 % by ORDERS_2:def_5;
hence a [= q9 by LATTICE3:7; ::_thesis: verum
end;
hence ex b1 being Element of the carrier of (L .:) st
( b1 is_less_than X & ( for b2 being Element of the carrier of (L .:) holds
( not b2 is_less_than X or b2 [= b1 ) ) ) by A3; ::_thesis: verum
end;
end;
definition
let C be FormalContext;
funcC .: -> non quasi-empty strict ContextStr equals :: CONLAT_2:def 7
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);
coherence
ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #) is non quasi-empty strict ContextStr by CONLAT_1:def_1;
end;
:: deftheorem defines .: CONLAT_2:def_7_:_
for C being FormalContext holds C .: = ContextStr(# the carrier' of C, the carrier of C,( the Information of C ~) #);
theorem :: CONLAT_2:17
for C being strict FormalContext holds (C .:) .: = C ;
theorem Th18: :: CONLAT_2:18
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; ::_thesis: for O being Subset of the carrier of C holds (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O
let O be Subset of the carrier of C; ::_thesis: (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O
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: { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } c= { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } or u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } )
assume u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o }
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 .:); ::_thesis: ( o9 in O9 implies u9 is-connected-with o9 )
reconsider o = o9 as Object of C ;
assume o9 in O9 ; ::_thesis: u9 is-connected-with 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 u9 is-connected-with o9 by A2, CONLAT_1:def_2; ::_thesis: verum
end;
hence u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ; ::_thesis: verum
end;
A4: { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } c= { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } or u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } )
assume u in { a where a is Object of (C .:) : for o being Attribute of (C .:) st o in O9 holds
a is-connected-with o } ; ::_thesis: u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a }
then 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; ::_thesis: ( o9 in O implies o9 is-connected-with u9 )
reconsider o = o9 as Attribute of (C .:) ;
assume o9 in O ; ::_thesis: o9 is-connected-with u9
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 o9 is-connected-with u9 by CONLAT_1:def_2; ::_thesis: verum
end;
hence u in { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } ; ::_thesis: verum
end;
( (ObjectDerivation C) . O = { a where a is Attribute of C : for o being Object of C st o in O holds
o is-connected-with a } & (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, CONLAT_1:def_4;
hence (ObjectDerivation C) . O = (AttributeDerivation (C .:)) . O by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th19: :: CONLAT_2:19
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; ::_thesis: for A being Subset of the carrier' of C holds (AttributeDerivation C) . A = (ObjectDerivation (C .:)) . A
let O be Subset of the carrier' of C; ::_thesis: (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O
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: { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } c= { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } or u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } )
assume u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ; ::_thesis: u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a }
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 .:); ::_thesis: ( o9 in O9 implies o9 is-connected-with u9 )
reconsider o = o9 as Attribute of C ;
assume o9 in O9 ; ::_thesis: o9 is-connected-with u9
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 o9 is-connected-with u9 by CONLAT_1:def_2; ::_thesis: verum
end;
hence u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ; ::_thesis: verum
end;
A4: { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } c= { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o }
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } or u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } )
assume u in { a where a is Attribute of (C .:) : for o being Object of (C .:) st o in O9 holds
o is-connected-with a } ; ::_thesis: u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o }
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; ::_thesis: ( o9 in O implies u9 is-connected-with o9 )
reconsider o = o9 as Object of (C .:) ;
assume o9 in O ; ::_thesis: u9 is-connected-with o9
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 u9 is-connected-with o9 by CONLAT_1:def_2; ::_thesis: verum
end;
hence u in { a where a is Object of C : for o being Attribute of C st o in O holds
a is-connected-with o } ; ::_thesis: verum
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, CONLAT_1:def_4;
hence (AttributeDerivation C) . O = (ObjectDerivation (C .:)) . O by A1, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
definition
let C be FormalContext;
let CP be ConceptStr over C;
funcCP .: -> strict ConceptStr over C .: means :Def8: :: CONLAT_2:def 8
( the Extent of it = the Intent of CP & the Intent of it = the Extent of CP );
existence
ex b1 being strict ConceptStr over C .: st
( the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP )
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 #) ; ::_thesis: ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP )
thus ( the Extent of ConceptStr(# O,A #) = the Intent of CP & the Intent of ConceptStr(# O,A #) = the Extent of CP ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict ConceptStr over C .: st the Extent of b1 = the Intent of CP & the Intent of b1 = the Extent of CP & the Extent of b2 = the Intent of CP & the Intent of b2 = the Extent of CP holds
b1 = b2 ;
end;
:: deftheorem Def8 defines .: CONLAT_2:def_8_:_
for C being FormalContext
for CP being ConceptStr over C
for b3 being strict ConceptStr over C .: holds
( b3 = CP .: iff ( the Extent of b3 = the Intent of CP & the Intent of b3 = the Extent of CP ) );
registration
let C be FormalContext;
let CP be FormalConcept of C;
clusterCP .: -> strict non empty concept-like ;
coherence
( not CP .: is empty & CP .: is concept-like )
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 ConceptStr(# O,A #) = (ObjectDerivation C) . the Extent of CP by Th18
.= the Extent of ConceptStr(# O,A #) by CONLAT_1:def_10 ;
A2: ConceptStr(# O,A #) = CP .: by Def8;
(ObjectDerivation (C .:)) . the Extent of ConceptStr(# O,A #) = (AttributeDerivation C) . the Intent of CP by Th19
.= the Intent of ConceptStr(# O,A #) by CONLAT_1:def_10 ;
hence ( not CP .: is empty & CP .: is concept-like ) by A1, A2, Lm3, CONLAT_1:def_10; ::_thesis: verum
end;
end;
theorem :: CONLAT_2:20
for C being strict FormalContext
for CP being strict FormalConcept of C holds (CP .:) .: = CP
proof
let C be strict FormalContext; ::_thesis: for CP being strict FormalConcept of C holds (CP .:) .: = CP
let CP be strict FormalConcept of C; ::_thesis: (CP .:) .: = CP
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 (CP .:) .: = CP by A1; ::_thesis: verum
end;
definition
let C be FormalContext;
func DualHomomorphism C -> Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) means :Def9: :: CONLAT_2:def 9
for CP being strict FormalConcept of C holds it . CP = CP .: ;
existence
ex b1 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st
for CP being strict FormalConcept of C holds b1 . CP = CP .:
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;
{ [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 } c= [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { [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 } or y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] )
assume y in { [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 } ; ::_thesis: y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):]
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 y in [: the carrier of ((ConceptLattice C) .:), the carrier of (ConceptLattice (C .:)):] by A4, A6, ZFMISC_1:def_2; ::_thesis: verum
end;
then reconsider 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 } 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not y in the carrier of ((ConceptLattice C) .:) or y in dom f )
assume y in the carrier of ((ConceptLattice C) .:) ; ::_thesis: y in dom f
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 = ConceptStr(# O9,A9 #) .: as Element of (ConceptLattice (C .:)) by A1, CONLAT_1:31;
[y,z] in f by A7, A8;
hence y in dom f by XTUPLE_0:def_12; ::_thesis: verum
end;
then A9: the carrier of ((ConceptLattice C) .:) = dom f by XBOOLE_0:def_10;
for x, y1, y2 being set st [x,y1] in f & [x,y2] in f holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( [x,y1] in f & [x,y2] in f implies y1 = y2 )
assume that
A10: [x,y1] in f and
A11: [x,y2] in f ; ::_thesis: y1 = y2
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 ; ::_thesis: verum
end;
then reconsider f = 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) .:) st a [= b holds
f . a [= f . b
proof
let a, b be Element of ((ConceptLattice C) .:); ::_thesis: ( a [= b implies f . a [= f . b )
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 set such that
A18: [a,fa] in f by XTUPLE_0:def_12;
assume a [= b ; ::_thesis: f . a [= f . 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 set 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 = 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 = 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 f . a [= f . b by A27, A23, CONLAT_1:43; ::_thesis: verum
end;
the carrier of (ConceptLattice (C .:)) c= rng f
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of (ConceptLattice (C .:)) or u in rng f )
A31: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def_1;
assume u in the carrier of (ConceptLattice (C .:)) ; ::_thesis: u in rng f
then reconsider u = 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 or not the Intent of (u @) is empty ) by CONLAT_1:def_8;
A33: (AttributeDerivation C) . the Intent of ConceptStr(# A9,O9 #) = (ObjectDerivation (C .:)) . the Extent of (u @) by Th19
.= the Extent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ;
(ObjectDerivation C) . the Extent of ConceptStr(# A9,O9 #) = (AttributeDerivation (C .:)) . the Intent of (u @) by Th18
.= the Intent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ;
then ConceptStr(# A9,O9 #) is FormalConcept of C by A33, A32, CONLAT_1:def_8, CONLAT_1:def_10;
then ConceptStr(# A9,O9 #) in dom f by A15, A2, A31, CONLAT_1:31;
then consider v being set such that
A34: [ConceptStr(# A9,O9 #),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: [ConceptStr(# A9,O9 #),v] = [ConceptStr(# Ov,Av #),(ConceptStr(# Ov,Av #) .:)] and
ConceptStr(# Ov,Av #) is FormalConcept of C by A34;
A36: ConceptStr(# A9,O9 #) = [ConceptStr(# A9,O9 #),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 = v as strict FormalConcept of C .: by A1, CONLAT_1:31;
v = [ConceptStr(# A9,O9 #),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 u in rng f by A37, CONLAT_1:def_21; ::_thesis: verum
end;
then A38: rng f = the carrier of (ConceptLattice (C .:)) by XBOOLE_0:def_10;
A39: f is one-to-one
proof
let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 f or not b in proj1 f or not f . a = f . b or a = b )
assume that
A40: a in dom f and
A41: b in dom f and
A42: f . a = f . b ; ::_thesis: a = b
reconsider a = a, b = b as Element of ((ConceptLattice C) .:) by A40, A41;
consider fa being set such that
A43: [a,fa] in f by A40, XTUPLE_0:def_12;
consider fb being set 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 a = b by A47, A49, A51; ::_thesis: verum
end;
for a, b being Element of ((ConceptLattice C) .:) st f . a [= f . b holds
a [= b
proof
let a, b be Element of ((ConceptLattice C) .:); ::_thesis: ( f . a [= f . b implies a [= b )
A52: dom f = the carrier of ((ConceptLattice C) .:) by FUNCT_2:def_1;
then consider fa being set 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 ; ::_thesis: a [= 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 set 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 = 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 = 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 a [= b by LATTICE3:7; ::_thesis: verum
end;
then reconsider f = 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; ::_thesis: f . CP = CP .:
CP in B-carrier C by CONLAT_1:31;
then CP in dom f by A3, FUNCT_2:def_1;
then consider v being set 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 = 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 f . CP = CP .: by A65, A68, FUNCT_1:1; ::_thesis: verum
end;
hence ex b1 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st
for CP being strict FormalConcept of C holds b1 . CP = CP .: ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) st ( for CP being strict FormalConcept of C holds b1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds b2 . CP = CP .: ) holds
b1 = b2
proof
let F1, F2 be Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:); ::_thesis: ( ( for CP being strict FormalConcept of C holds F1 . CP = CP .: ) & ( for CP being strict FormalConcept of C holds F2 . CP = CP .: ) implies F1 = F2 )
assume A69: for CP being strict FormalConcept of C holds F1 . CP = CP .: ; ::_thesis: ( ex CP being strict FormalConcept of C st not F2 . CP = CP .: or F1 = F2 )
assume A70: for CP being strict FormalConcept of C holds F2 . CP = CP .: ; ::_thesis: F1 = F2
A71: for u being set st u in the carrier of ((ConceptLattice C) .:) holds
F1 . u = F2 . u
proof
let u be set ; ::_thesis: ( u in the carrier of ((ConceptLattice C) .:) implies F1 . u = F2 . u )
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) .:) ; ::_thesis: F1 . u = F2 . u
then reconsider u = u as strict FormalConcept of C by A72, CONLAT_1:31;
F1 . u = u .: by A69
.= F2 . u by A70 ;
hence F1 . u = F2 . u ; ::_thesis: verum
end;
( dom F1 = the carrier of ((ConceptLattice C) .:) & dom F2 = the carrier of ((ConceptLattice C) .:) ) by FUNCT_2:def_1;
hence F1 = F2 by A71, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines DualHomomorphism CONLAT_2:def_9_:_
for C being FormalContext
for b2 being Homomorphism of (ConceptLattice C) .: , ConceptLattice (C .:) holds
( b2 = DualHomomorphism C iff for CP being strict FormalConcept of C holds b2 . CP = CP .: );
theorem Th21: :: CONLAT_2:21
for C being FormalContext holds DualHomomorphism C is bijective
proof
let C be FormalContext; ::_thesis: DualHomomorphism C is bijective
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 (DualHomomorphism C)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in the carrier of (ConceptLattice (C .:)) or u in rng (DualHomomorphism C) )
assume u in the carrier of (ConceptLattice (C .:)) ; ::_thesis: u in rng (DualHomomorphism C)
then reconsider u = 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 or not the Intent of (u @) is empty ) by CONLAT_1:def_8;
A4: (AttributeDerivation C) . the Intent of ConceptStr(# A9,O9 #) = (ObjectDerivation (C .:)) . the Extent of (u @) by Th19
.= the Extent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ;
A5: (ObjectDerivation C) . the Extent of ConceptStr(# A9,O9 #) = (AttributeDerivation (C .:)) . the Intent of (u @) by Th18
.= the Intent of ConceptStr(# A9,O9 #) by CONLAT_1:def_10 ;
then ConceptStr(# A9,O9 #) is FormalConcept of C by A4, A3, CONLAT_1:def_8, CONLAT_1:def_10;
then A6: ConceptStr(# A9,O9 #) in the carrier of (ConceptLattice C) by A1, CONLAT_1:31;
reconsider CP = ConceptStr(# A9,O9 #) as strict FormalConcept of C by A5, A4, A3, CONLAT_1:def_8, CONLAT_1:def_10;
A7: the Extent of (CP .:) = the Extent of (u @) by Def8;
( (DualHomomorphism C) . CP = CP .: & the Intent of (CP .:) = the Intent of (u @) ) by Def8, Def9;
then A8: (DualHomomorphism C) . CP = u by A7, CONLAT_1:def_21;
CP in dom (DualHomomorphism C) by A2, A6, FUNCT_2:def_1;
hence u in rng (DualHomomorphism C) by A8, FUNCT_1:def_3; ::_thesis: verum
end;
then rng (DualHomomorphism C) = the carrier of (ConceptLattice (C .:)) by XBOOLE_0:def_10;
then A9: DualHomomorphism C is onto by FUNCT_2:def_3;
DualHomomorphism C is one-to-one
proof
let a, b be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not a in proj1 (DualHomomorphism C) or not b in proj1 (DualHomomorphism C) or not (DualHomomorphism C) . a = (DualHomomorphism C) . b or a = b )
assume that
A10: ( a in dom (DualHomomorphism C) & b in dom (DualHomomorphism C) ) and
A11: (DualHomomorphism C) . a = (DualHomomorphism C) . b ; ::_thesis: a = b
reconsider a = a, b = 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 = a, b = b as Element of (ConceptLattice C) ;
A12: ( (DualHomomorphism C) . (a @) = (DualHomomorphism C) . a & (DualHomomorphism C) . (b @) = (DualHomomorphism C) . b ) by CONLAT_1:def_21;
A13: ( (DualHomomorphism C) . (a @) = (a @) .: & (DualHomomorphism C) . (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 a = b ; ::_thesis: verum
end;
hence DualHomomorphism C is bijective by A9; ::_thesis: verum
end;
theorem :: CONLAT_2:22
for C being FormalContext holds ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic
proof
let C be FormalContext; ::_thesis: ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic
DualHomomorphism C is bijective by Th21;
hence ConceptLattice (C .:),(ConceptLattice C) .: are_isomorphic by LATTICE4:def_2; ::_thesis: verum
end;