let C be FormalContext; 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
object ;
TARSKI:def 3 ( not u in the carrier of (ConceptLattice (C .:)) or u in rng (DualHomomorphism C) )
assume
u in the
carrier of
(ConceptLattice (C .:))
;
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;
verum
end;
then
rng (DualHomomorphism C) = the carrier of (ConceptLattice (C .:))
;
then A9:
DualHomomorphism C is onto
by FUNCT_2:def 3;
DualHomomorphism C is one-to-one
proof
let a,
b be
object ;
FUNCT_1:def 4 ( 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
;
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
;
verum
end;
hence
DualHomomorphism C is bijective
by A9; verum