let P, R be non empty Poset; for Con being Connection of P,R
for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let Con be Connection of P,R; for f being Function of P,R
for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let f be Function of P,R; for g being Function of R,P st Con = [f,g] holds
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
let g be Function of R,P; ( Con = [f,g] implies ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) )
assume A1:
Con = [f,g]
; ( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
A2:
now ( ( for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) ) implies Con is co-Galois )assume A3:
for
p being
Element of
P for
r being
Element of
R holds
(
p <= g . r iff
r <= f . p )
;
Con is co-Galois
for
p1,
p2 being
Element of
P st
p1 <= p2 holds
for
r1,
r2 being
Element of
R st
r1 = f . p1 &
r2 = f . p2 holds
r1 >= r2
proof
let p1,
p2 be
Element of
P;
( p1 <= p2 implies for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2 )
assume A4:
p1 <= p2
;
for r1, r2 being Element of R st r1 = f . p1 & r2 = f . p2 holds
r1 >= r2
let r1,
r2 be
Element of
R;
( r1 = f . p1 & r2 = f . p2 implies r1 >= r2 )
assume A5:
(
r1 = f . p1 &
r2 = f . p2 )
;
r1 >= r2
p2 <= g . (f . p2)
by A3;
then
p1 <= g . (f . p2)
by A4, ORDERS_2:3;
hence
r1 >= r2
by A3, A5;
verum
end; then A6:
f is
antitone
by WAYBEL_0:def 5;
for
r1,
r2 being
Element of
R st
r1 <= r2 holds
for
p1,
p2 being
Element of
P st
p1 = g . r1 &
p2 = g . r2 holds
p1 >= p2
proof
let r1,
r2 be
Element of
R;
( r1 <= r2 implies for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2 )
assume A7:
r1 <= r2
;
for p1, p2 being Element of P st p1 = g . r1 & p2 = g . r2 holds
p1 >= p2
let p1,
p2 be
Element of
P;
( p1 = g . r1 & p2 = g . r2 implies p1 >= p2 )
assume A8:
(
p1 = g . r1 &
p2 = g . r2 )
;
p1 >= p2
r2 <= f . (g . r2)
by A3;
then
r1 <= f . (g . r2)
by A7, ORDERS_2:3;
hence
p1 >= p2
by A3, A8;
verum
end; then A9:
g is
antitone
by WAYBEL_0:def 5;
for
p1,
p2 being
Element of
P for
r1,
r2 being
Element of
R holds
(
p1 <= g . (f . p1) &
r1 <= f . (g . r1) )
by A3;
hence
Con is
co-Galois
by A1, A6, A9;
verum end;
now ( Con is co-Galois implies for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )assume
Con is
co-Galois
;
for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p )then consider f9 being
Function of
P,
R,
g9 being
Function of
R,
P such that A10:
Con = [f9,g9]
and A11:
f9 is
antitone
and A12:
g9 is
antitone
and A13:
for
p1,
p2 being
Element of
P for
r1,
r2 being
Element of
R holds
(
p1 <= g9 . (f9 . p1) &
r1 <= f9 . (g9 . r1) )
;
A14:
g =
[f,g] `2
.=
Con `2
by A1
.=
[f9,g9] `2
by A10
.=
g9
;
A15:
f =
[f,g] `1
.=
Con `1
by A1
.=
[f9,g9] `1
by A10
.=
f9
;
A16:
for
p being
Element of
P for
r being
Element of
R st
r <= f . p holds
p <= g . r
for
p being
Element of
P for
r being
Element of
R st
p <= g . r holds
r <= f . p
hence
for
p being
Element of
P for
r being
Element of
R holds
(
p <= g . r iff
r <= f . p )
by A16;
verum end;
hence
( Con is co-Galois iff for p being Element of P
for r being Element of R holds
( p <= g . r iff r <= f . p ) )
by A2; verum