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 23;
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 ;
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 11;
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 13
;
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 13
;
then
ConceptStr(#
A9,
O9 #) is
FormalConcept of
C
by A4, A3, CONLAT_1:def 11, CONLAT_1:def 13;
then A6:
ConceptStr(#
A9,
O9 #)
in the
carrier of
(ConceptLattice C)
by A1, CONLAT_1:35;
reconsider CP =
ConceptStr(#
A9,
O9 #) as
strict FormalConcept of
C by A5, A4, A3, CONLAT_1:def 11, CONLAT_1:def 13;
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 24;
CP in dom (DualHomomorphism C)
by A2, A6, FUNCT_2:def 1;
hence
u in rng (DualHomomorphism C)
by A8, FUNCT_1:def 5;
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 ;
FUNCT_1:def 8 ( not a in K41((DualHomomorphism C)) or not b in K41((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 24;
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 24
.=
b
by CONLAT_1:def 24
;
hence
a = b
;
verum
end;
hence
DualHomomorphism C is bijective
by A9; verum