:: WAYBEL_1 semantic presentation
begin
definition
let L1, L2 be non empty 1-sorted ;
let f be Function of L1,L2;
:: original: one-to-one
redefine attrf is one-to-one means :: WAYBEL_1:def 1
for x, y being Element of L1 st f . x = f . y holds
x = y;
compatibility
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y )
proof
thus ( f is one-to-one implies for x, y being Element of L1 st f . x = f . y holds
x = y ) by FUNCT_2:19; ::_thesis: ( ( for x, y being Element of L1 st f . x = f . y holds
x = y ) implies f is one-to-one )
assume for x, y being Element of L1 st f . x = f . y holds
x = y ; ::_thesis: f is one-to-one
then for x, y being set st x in the carrier of L1 & y in the carrier of L1 & f . x = f . y holds
x = y ;
hence f is one-to-one by FUNCT_2:19; ::_thesis: verum
end;
end;
:: deftheorem defines one-to-one WAYBEL_1:def_1_:_
for L1, L2 being non empty 1-sorted
for f being Function of L1,L2 holds
( f is one-to-one iff for x, y being Element of L1 st f . x = f . y holds
x = y );
definition
let L1, L2 be non empty RelStr ;
let f be Function of L1,L2;
redefine attr f is monotone means :Def2: :: WAYBEL_1:def 2
for x, y being Element of L1 st x <= y holds
f . x <= f . y;
compatibility
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y )
proof
thus ( f is monotone implies for x, y being Element of L1 st x <= y holds
f . x <= f . y ) by ORDERS_3:def_5; ::_thesis: ( ( for x, y being Element of L1 st x <= y holds
f . x <= f . y ) implies f is monotone )
assume for x, y being Element of L1 st x <= y holds
f . x <= f . y ; ::_thesis: f is monotone
hence for x, y being Element of L1 st x <= y holds
for a, b being Element of L2 st a = f . x & b = f . y holds
a <= b ; :: according to ORDERS_3:def_5 ::_thesis: verum
end;
end;
:: deftheorem Def2 defines monotone WAYBEL_1:def_2_:_
for L1, L2 being non empty RelStr
for f being Function of L1,L2 holds
( f is monotone iff for x, y being Element of L1 st x <= y holds
f . x <= f . y );
theorem Th1: :: WAYBEL_1:1
for L being transitive antisymmetric with_infima RelStr
for x, y, z being Element of L st x <= y holds
x "/\" z <= y "/\" z
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for x, y, z being Element of L st x <= y holds
x "/\" z <= y "/\" z
let x, y, z be Element of L; ::_thesis: ( x <= y implies x "/\" z <= y "/\" z )
A1: x "/\" z <= x by YELLOW_0:23;
A2: x "/\" z <= z by YELLOW_0:23;
assume x <= y ; ::_thesis: x "/\" z <= y "/\" z
then x "/\" z <= y by A1, ORDERS_2:3;
hence x "/\" z <= y "/\" z by A2, YELLOW_0:23; ::_thesis: verum
end;
theorem Th2: :: WAYBEL_1:2
for L being transitive antisymmetric with_suprema RelStr
for x, y, z being Element of L st x <= y holds
x "\/" z <= y "\/" z
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for x, y, z being Element of L st x <= y holds
x "\/" z <= y "\/" z
let x, y, z be Element of L; ::_thesis: ( x <= y implies x "\/" z <= y "\/" z )
A1: y <= y "\/" z by YELLOW_0:22;
A2: z <= y "\/" z by YELLOW_0:22;
assume x <= y ; ::_thesis: x "\/" z <= y "\/" z
then x <= y "\/" z by A1, ORDERS_2:3;
hence x "\/" z <= y "\/" z by A2, YELLOW_0:22; ::_thesis: verum
end;
theorem Th3: :: WAYBEL_1:3
for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L holds
( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L holds
( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )
let x be Element of L; ::_thesis: ( ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) & ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x ) )
thus ( L is with_infima implies (Bottom L) "/\" x = Bottom L ) ::_thesis: ( L is with_suprema & L is reflexive & L is transitive implies (Bottom L) "\/" x = x )
proof
assume L is with_infima ; ::_thesis: (Bottom L) "/\" x = Bottom L
then ( Bottom L <= (Bottom L) "/\" x & (Bottom L) "/\" x <= Bottom L ) by YELLOW_0:23, YELLOW_0:44;
hence (Bottom L) "/\" x = Bottom L by ORDERS_2:2; ::_thesis: verum
end;
assume A1: L is with_suprema ; ::_thesis: ( not L is reflexive or not L is transitive or (Bottom L) "\/" x = x )
then A2: x <= (Bottom L) "\/" x by YELLOW_0:22;
assume ( L is reflexive & L is transitive ) ; ::_thesis: (Bottom L) "\/" x = x
then A3: x <= x by ORDERS_2:1;
Bottom L <= x by YELLOW_0:44;
then (Bottom L) "\/" x <= x by A1, A3, YELLOW_0:22;
hence (Bottom L) "\/" x = x by A2, ORDERS_2:2; ::_thesis: verum
end;
theorem Th4: :: WAYBEL_1:4
for L being non empty antisymmetric upper-bounded RelStr
for x being Element of L holds
( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) )
proof
let L be non empty antisymmetric upper-bounded RelStr ; ::_thesis: for x being Element of L holds
( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) )
let x be Element of L; ::_thesis: ( ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) & ( L is with_suprema implies (Top L) "\/" x = Top L ) )
thus ( L is with_infima & L is transitive & L is reflexive implies (Top L) "/\" x = x ) ::_thesis: ( L is with_suprema implies (Top L) "\/" x = Top L )
proof
assume A1: ( L is with_infima & L is transitive & L is reflexive ) ; ::_thesis: (Top L) "/\" x = x
then x "/\" x <= (Top L) "/\" x by Th1, YELLOW_0:45;
then A2: x <= (Top L) "/\" x by A1, YELLOW_0:25;
(Top L) "/\" x <= x by A1, YELLOW_0:23;
hence (Top L) "/\" x = x by A2, ORDERS_2:2; ::_thesis: verum
end;
assume L is with_suprema ; ::_thesis: (Top L) "\/" x = Top L
then ( (Top L) "\/" x <= Top L & Top L <= (Top L) "\/" x ) by YELLOW_0:22, YELLOW_0:45;
hence (Top L) "\/" x = Top L by ORDERS_2:2; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
attrL is distributive means :Def3: :: WAYBEL_1:def 3
for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z);
end;
:: deftheorem Def3 defines distributive WAYBEL_1:def_3_:_
for L being non empty RelStr holds
( L is distributive iff for x, y, z being Element of L holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) );
theorem Th5: :: WAYBEL_1:5
for L being LATTICE holds
( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) )
proof
let L be LATTICE; ::_thesis: ( L is distributive iff for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) )
hereby ::_thesis: ( ( for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ) implies L is distributive )
assume A1: L is distributive ; ::_thesis: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
let x, y, z be Element of L; ::_thesis: x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z)
thus x "\/" (y "/\" z) = (x "\/" (z "/\" x)) "\/" (y "/\" z) by LATTICE3:17
.= x "\/" ((z "/\" x) "\/" (z "/\" y)) by LATTICE3:14
.= x "\/" ((x "\/" y) "/\" z) by A1, Def3
.= ((x "\/" y) "/\" x) "\/" ((x "\/" y) "/\" z) by LATTICE3:18
.= (x "\/" y) "/\" (x "\/" z) by A1, Def3 ; ::_thesis: verum
end;
assume A2: for x, y, z being Element of L holds x "\/" (y "/\" z) = (x "\/" y) "/\" (x "\/" z) ; ::_thesis: L is distributive
let x, y, z be Element of L; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = (x "/\" (x "\/" z)) "/\" (y "\/" z) by LATTICE3:18
.= x "/\" ((z "\/" x) "/\" (y "\/" z)) by LATTICE3:16
.= x "/\" (z "\/" (x "/\" y)) by A2
.= ((y "/\" x) "\/" x) "/\" ((x "/\" y) "\/" z) by LATTICE3:17
.= (x "/\" y) "\/" (x "/\" z) by A2 ; ::_thesis: verum
end;
registration
let X be set ;
cluster BoolePoset X -> distributive ;
coherence
BoolePoset X is distributive
proof
let x, y, z be Element of (BoolePoset X); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by YELLOW_1:17
.= x /\ (y \/ z) by YELLOW_1:17
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by YELLOW_1:17
.= (x "/\" y) \/ (x "/\" z) by YELLOW_1:17
.= (x "/\" y) "\/" (x "/\" z) by YELLOW_1:17 ; ::_thesis: verum
end;
end;
definition
let S be non empty RelStr ;
let X be set ;
pred ex_min_of X,S means :: WAYBEL_1:def 4
( ex_inf_of X,S & "/\" (X,S) in X );
pred ex_max_of X,S means :Def5: :: WAYBEL_1:def 5
( ex_sup_of X,S & "\/" (X,S) in X );
end;
:: deftheorem defines ex_min_of WAYBEL_1:def_4_:_
for S being non empty RelStr
for X being set holds
( ex_min_of X,S iff ( ex_inf_of X,S & "/\" (X,S) in X ) );
:: deftheorem Def5 defines ex_max_of WAYBEL_1:def_5_:_
for S being non empty RelStr
for X being set holds
( ex_max_of X,S iff ( ex_sup_of X,S & "\/" (X,S) in X ) );
notation
let S be non empty RelStr ;
let X be set ;
synonym X has_the_min_in S for ex_min_of X,S;
synonym X has_the_max_in S for ex_max_of X,S;
end;
definition
let S be non empty RelStr ;
let s be Element of S;
let X be set ;
preds is_minimum_of X means :Def6: :: WAYBEL_1:def 6
( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X );
preds is_maximum_of X means :Def7: :: WAYBEL_1:def 7
( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X );
end;
:: deftheorem Def6 defines is_minimum_of WAYBEL_1:def_6_:_
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_minimum_of X iff ( ex_inf_of X,S & s = "/\" (X,S) & "/\" (X,S) in X ) );
:: deftheorem Def7 defines is_maximum_of WAYBEL_1:def_7_:_
for S being non empty RelStr
for s being Element of S
for X being set holds
( s is_maximum_of X iff ( ex_sup_of X,S & s = "\/" (X,S) & "\/" (X,S) in X ) );
registration
let L be RelStr ;
cluster id L -> isomorphic ;
coherence
id L is isomorphic
proof
percases ( not L is empty or L is empty ) ;
supposeA1: not L is empty ; ::_thesis: id L is isomorphic
A2: id L = (id L) " by FUNCT_1:45;
id L is monotone by A1, YELLOW_2:11;
hence id L is isomorphic by A1, A2, WAYBEL_0:def_38; ::_thesis: verum
end;
suppose L is empty ; ::_thesis: id L is isomorphic
hence id L is isomorphic by WAYBEL_0:def_38; ::_thesis: verum
end;
end;
end;
end;
definition
let L1, L2 be RelStr ;
predL1,L2 are_isomorphic means :Def8: :: WAYBEL_1:def 8
ex f being Function of L1,L2 st f is isomorphic ;
reflexivity
for L1 being RelStr ex f being Function of L1,L1 st f is isomorphic
proof
let L be RelStr ; ::_thesis: ex f being Function of L,L st f is isomorphic
take id L ; ::_thesis: id L is isomorphic
thus id L is isomorphic ; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines are_isomorphic WAYBEL_1:def_8_:_
for L1, L2 being RelStr holds
( L1,L2 are_isomorphic iff ex f being Function of L1,L2 st f is isomorphic );
theorem :: WAYBEL_1:6
for L1, L2 being non empty RelStr st L1,L2 are_isomorphic holds
L2,L1 are_isomorphic
proof
let L1, L2 be non empty RelStr ; ::_thesis: ( L1,L2 are_isomorphic implies L2,L1 are_isomorphic )
given f being Function of L1,L2 such that A1: f is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: L2,L1 are_isomorphic
consider g being Function of L2,L1 such that
A2: g = f " and
A3: g is monotone by A1, WAYBEL_0:def_38;
f = g " by A1, A2, FUNCT_1:43;
then g is isomorphic by A1, A2, A3, WAYBEL_0:def_38;
hence L2,L1 are_isomorphic by Def8; ::_thesis: verum
end;
theorem :: WAYBEL_1:7
for L1, L2, L3 being RelStr st L1,L2 are_isomorphic & L2,L3 are_isomorphic holds
L1,L3 are_isomorphic
proof
let L1, L2, L3 be RelStr ; ::_thesis: ( L1,L2 are_isomorphic & L2,L3 are_isomorphic implies L1,L3 are_isomorphic )
given f1 being Function of L1,L2 such that A1: f1 is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: ( not L2,L3 are_isomorphic or L1,L3 are_isomorphic )
given f2 being Function of L2,L3 such that A2: f2 is isomorphic ; :: according to WAYBEL_1:def_8 ::_thesis: L1,L3 are_isomorphic
A3: now__::_thesis:_(_L1_is_empty_implies_f2_*_f1_is_Function_of_L1,L3_)
assume L1 is empty ; ::_thesis: f2 * f1 is Function of L1,L3
then the carrier of L1 is empty ;
hence f2 * f1 is Function of L1,L3 by FUNCT_2:13; ::_thesis: verum
end;
percases ( ( not L1 is empty & not L2 is empty & not L3 is empty ) or L1 is empty or L2 is empty or L3 is empty ) ;
suppose ( not L1 is empty & not L2 is empty & not L3 is empty ) ; ::_thesis: L1,L3 are_isomorphic
then reconsider L1 = L1, L2 = L2, L3 = L3 as non empty RelStr ;
reconsider f1 = f1 as Function of L1,L2 ;
reconsider f2 = f2 as Function of L2,L3 ;
consider g1 being Function of L2,L1 such that
A4: ( g1 = f1 " & g1 is monotone ) by A1, WAYBEL_0:def_38;
consider g2 being Function of L3,L2 such that
A5: ( g2 = f2 " & g2 is monotone ) by A2, WAYBEL_0:def_38;
A6: f2 * f1 is monotone by A1, A2, YELLOW_2:12;
( g1 * g2 is monotone & g1 * g2 = (f2 * f1) " ) by A1, A2, A4, A5, FUNCT_1:44, YELLOW_2:12;
then f2 * f1 is isomorphic by A1, A2, A6, WAYBEL_0:def_38;
hence L1,L3 are_isomorphic by Def8; ::_thesis: verum
end;
supposeA7: L1 is empty ; ::_thesis: L1,L3 are_isomorphic
then reconsider f = f2 * f1 as Function of L1,L3 by A3;
L2 is empty by A1, A7, WAYBEL_0:def_38;
then L3 is empty by A2, WAYBEL_0:def_38;
then f is isomorphic by A7, WAYBEL_0:def_38;
hence L1,L3 are_isomorphic by Def8; ::_thesis: verum
end;
supposeA8: L2 is empty ; ::_thesis: L1,L3 are_isomorphic
then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def_38;
( L1 is empty & L3 is empty ) by A1, A2, A8, WAYBEL_0:def_38;
then f is isomorphic by WAYBEL_0:def_38;
hence L1,L3 are_isomorphic by Def8; ::_thesis: verum
end;
supposeA9: L3 is empty ; ::_thesis: L1,L3 are_isomorphic
then A10: L2 is empty by A2, WAYBEL_0:def_38;
then reconsider f = f2 * f1 as Function of L1,L3 by A1, A3, WAYBEL_0:def_38;
L1 is empty by A1, A10, WAYBEL_0:def_38;
then f is isomorphic by A9, WAYBEL_0:def_38;
hence L1,L3 are_isomorphic by Def8; ::_thesis: verum
end;
end;
end;
begin
definition
let S, T be RelStr ;
mode Connection of S,T -> set means :Def9: :: WAYBEL_1:def 9
ex g being Function of S,T ex d being Function of T,S st it = [g,d];
existence
ex b1 being set ex g being Function of S,T ex d being Function of T,S st b1 = [g,d]
proof
set g = the Function of S,T;
set d = the Function of T,S;
take [ the Function of S,T, the Function of T,S] ; ::_thesis: ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d]
thus ex g being Function of S,T ex d being Function of T,S st [ the Function of S,T, the Function of T,S] = [g,d] ; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Connection WAYBEL_1:def_9_:_
for S, T being RelStr
for b3 being set holds
( b3 is Connection of S,T iff ex g being Function of S,T ex d being Function of T,S st b3 = [g,d] );
definition
let S, T be RelStr ;
let g be Function of S,T;
let d be Function of T,S;
:: original: [
redefine func[g,d] -> Connection of S,T;
coherence
[g,d] is Connection of S,T by Def9;
end;
definition
let S, T be non empty RelStr ;
let gc be Connection of S,T;
attrgc is Galois means :Def10: :: WAYBEL_1:def 10
ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) );
end;
:: deftheorem Def10 defines Galois WAYBEL_1:def_10_:_
for S, T being non empty RelStr
for gc being Connection of S,T holds
( gc is Galois iff ex g being Function of S,T ex d being Function of T,S st
( gc = [g,d] & g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) );
theorem Th8: :: WAYBEL_1:8
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
let g be Function of S,T; ::_thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) )
hereby ::_thesis: ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois )
assume [g,d] is Galois ; ::_thesis: ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) )
then consider g9 being Function of S,T, d9 being Function of T,S such that
A1: [g,d] = [g9,d9] and
A2: ( g9 is monotone & d9 is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g9 . s iff d9 . t <= s ) ) ) by Def10;
( g = g9 & d = d9 ) by A1, XTUPLE_0:1;
hence ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) ) by A2; ::_thesis: verum
end;
thus ( g is monotone & d is monotone & ( for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s ) ) implies [g,d] is Galois ) by Def10; ::_thesis: verum
end;
definition
let S, T be non empty RelStr ;
let g be Function of S,T;
attrg is upper_adjoint means :Def11: :: WAYBEL_1:def 11
ex d being Function of T,S st [g,d] is Galois ;
end;
:: deftheorem Def11 defines upper_adjoint WAYBEL_1:def_11_:_
for S, T being non empty RelStr
for g being Function of S,T holds
( g is upper_adjoint iff ex d being Function of T,S st [g,d] is Galois );
definition
let S, T be non empty RelStr ;
let d be Function of T,S;
attrd is lower_adjoint means :Def12: :: WAYBEL_1:def 12
ex g being Function of S,T st [g,d] is Galois ;
end;
:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def_12_:_
for S, T being non empty RelStr
for d being Function of T,S holds
( d is lower_adjoint iff ex g being Function of S,T st [g,d] is Galois );
theorem Th9: :: WAYBEL_1:9
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds
( g is upper_adjoint & d is lower_adjoint )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is upper_adjoint & d is lower_adjoint ) )
assume A1: [g,d] is Galois ; ::_thesis: ( g is upper_adjoint & d is lower_adjoint )
hence ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: d is lower_adjoint
thus ex g being Function of S,T st [g,d] is Galois by A1; :: according to WAYBEL_1:def_12 ::_thesis: verum
end;
theorem Th10: :: WAYBEL_1:10
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
let g be Function of S,T; ::_thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
hereby ::_thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) implies [g,d] is Galois )
assume A1: [g,d] is Galois ; ::_thesis: ( g is monotone & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
hence g is monotone by Th8; ::_thesis: for t being Element of T holds d . t is_minimum_of g " (uparrow t)
let t be Element of T; ::_thesis: d . t is_minimum_of g " (uparrow t)
thus d . t is_minimum_of g " (uparrow t) ::_thesis: verum
proof
set X = g " (uparrow t);
t <= g . (d . t) by A1, Th8;
then g . (d . t) in uparrow t by WAYBEL_0:18;
then A2: d . t in g " (uparrow t) by FUNCT_2:38;
then A3: for s being Element of S st s is_<=_than g " (uparrow t) holds
d . t >= s by LATTICE3:def_8;
A4: d . t is_<=_than g " (uparrow t)
proof
let s be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not s in g " (uparrow t) or d . t <= s )
assume s in g " (uparrow t) ; ::_thesis: d . t <= s
then g . s in uparrow t by FUNCT_1:def_7;
then t <= g . s by WAYBEL_0:18;
hence d . t <= s by A1, Th8; ::_thesis: verum
end;
hence ( ex_inf_of g " (uparrow t),S & d . t = inf (g " (uparrow t)) ) by A3, YELLOW_0:31; :: according to WAYBEL_1:def_6 ::_thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t)
thus "/\" ((g " (uparrow t)),S) in g " (uparrow t) by A4, A2, A3, YELLOW_0:31; ::_thesis: verum
end;
end;
assume that
A5: g is monotone and
A6: for t being Element of T holds d . t is_minimum_of g " (uparrow t) ; ::_thesis: [g,d] is Galois
A7: for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )
proof
let t be Element of T; ::_thesis: for s being Element of S holds
( t <= g . s iff d . t <= s )
let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s )
set X = g " (uparrow t);
hereby ::_thesis: ( d . t <= s implies t <= g . s )
assume t <= g . s ; ::_thesis: d . t <= s
then g . s in uparrow t by WAYBEL_0:18;
then A8: s in g " (uparrow t) by FUNCT_2:38;
A9: d . t is_minimum_of g " (uparrow t) by A6;
then ex_inf_of g " (uparrow t),S by Def6;
then g " (uparrow t) is_>=_than inf (g " (uparrow t)) by YELLOW_0:def_10;
then s >= inf (g " (uparrow t)) by A8, LATTICE3:def_8;
hence d . t <= s by A9, Def6; ::_thesis: verum
end;
A10: d . t is_minimum_of g " (uparrow t) by A6;
then inf (g " (uparrow t)) in g " (uparrow t) by Def6;
then g . (inf (g " (uparrow t))) in uparrow t by FUNCT_1:def_7;
then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:18;
then A11: g . (d . t) >= t by A10, Def6;
assume d . t <= s ; ::_thesis: t <= g . s
then g . (d . t) <= g . s by A5, Def2;
hence t <= g . s by A11, ORDERS_2:3; ::_thesis: verum
end;
d is monotone
proof
let t1, t2 be Element of T; :: according to WAYBEL_1:def_2 ::_thesis: ( t1 <= t2 implies d . t1 <= d . t2 )
assume t1 <= t2 ; ::_thesis: d . t1 <= d . t2
then A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
A13: d . t2 is_minimum_of g " (uparrow t2) by A6;
then A14: ex_inf_of g " (uparrow t2),S by Def6;
A15: d . t1 is_minimum_of g " (uparrow t1) by A6;
then ex_inf_of g " (uparrow t1),S by Def6;
then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A14, A12, RELAT_1:143, YELLOW_0:35;
then d . t1 <= inf (g " (uparrow t2)) by A15, Def6;
hence d . t1 <= d . t2 by A13, Def6; ::_thesis: verum
end;
hence [g,d] is Galois by A5, A7, Th8; ::_thesis: verum
end;
theorem Th11: :: WAYBEL_1:11
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let g be Function of S,T; ::_thesis: for d being Function of T,S holds
( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois iff ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
hereby ::_thesis: ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) implies [g,d] is Galois )
assume A1: [g,d] is Galois ; ::_thesis: ( d is monotone & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
hence d is monotone by Th8; ::_thesis: for s being Element of S holds g . s is_maximum_of d " (downarrow s)
let s be Element of S; ::_thesis: g . s is_maximum_of d " (downarrow s)
thus g . s is_maximum_of d " (downarrow s) ::_thesis: verum
proof
set X = d " (downarrow s);
s >= d . (g . s) by A1, Th8;
then d . (g . s) in downarrow s by WAYBEL_0:17;
then A2: g . s in d " (downarrow s) by FUNCT_2:38;
then A3: for t being Element of T st t is_>=_than d " (downarrow s) holds
g . s <= t by LATTICE3:def_9;
A4: g . s is_>=_than d " (downarrow s)
proof
let t be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not t in d " (downarrow s) or t <= g . s )
assume t in d " (downarrow s) ; ::_thesis: t <= g . s
then d . t in downarrow s by FUNCT_1:def_7;
then s >= d . t by WAYBEL_0:17;
hence t <= g . s by A1, Th8; ::_thesis: verum
end;
hence ( ex_sup_of d " (downarrow s),T & g . s = sup (d " (downarrow s)) ) by A3, YELLOW_0:30; :: according to WAYBEL_1:def_7 ::_thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s)
thus "\/" ((d " (downarrow s)),T) in d " (downarrow s) by A4, A2, A3, YELLOW_0:30; ::_thesis: verum
end;
end;
assume that
A5: d is monotone and
A6: for s being Element of S holds g . s is_maximum_of d " (downarrow s) ; ::_thesis: [g,d] is Galois
A7: for t being Element of T
for s being Element of S holds
( s >= d . t iff g . s >= t )
proof
let t be Element of T; ::_thesis: for s being Element of S holds
( s >= d . t iff g . s >= t )
let s be Element of S; ::_thesis: ( s >= d . t iff g . s >= t )
set X = d " (downarrow s);
A8: g . s is_maximum_of d " (downarrow s) by A6;
then sup (d " (downarrow s)) in d " (downarrow s) by Def7;
then d . (sup (d " (downarrow s))) in downarrow s by FUNCT_1:def_7;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:17;
then A9: d . (g . s) <= s by A8, Def7;
hereby ::_thesis: ( g . s >= t implies s >= d . t )
assume s >= d . t ; ::_thesis: g . s >= t
then d . t in downarrow s by WAYBEL_0:17;
then A10: t in d " (downarrow s) by FUNCT_2:38;
ex_sup_of d " (downarrow s),T by A8, Def7;
then d " (downarrow s) is_<=_than sup (d " (downarrow s)) by YELLOW_0:def_9;
then t <= sup (d " (downarrow s)) by A10, LATTICE3:def_9;
hence g . s >= t by A8, Def7; ::_thesis: verum
end;
assume g . s >= t ; ::_thesis: s >= d . t
then d . (g . s) >= d . t by A5, Def2;
hence s >= d . t by A9, ORDERS_2:3; ::_thesis: verum
end;
g is monotone
proof
let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies g . s1 <= g . s2 )
assume s1 <= s2 ; ::_thesis: g . s1 <= g . s2
then A11: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
A12: g . s2 is_maximum_of d " (downarrow s2) by A6;
then A13: ex_sup_of d " (downarrow s2),T by Def7;
A14: g . s1 is_maximum_of d " (downarrow s1) by A6;
then ex_sup_of d " (downarrow s1),T by Def7;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A13, A11, RELAT_1:143, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A14, Def7;
hence g . s1 <= g . s2 by A12, Def7; ::_thesis: verum
end;
hence [g,d] is Galois by A5, A7, Th8; ::_thesis: verum
end;
theorem Th12: :: WAYBEL_1:12
for S, T being non empty Poset
for g being Function of S,T st g is upper_adjoint holds
g is infs-preserving
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T st g is upper_adjoint holds
g is infs-preserving
let g be Function of S,T; ::_thesis: ( g is upper_adjoint implies g is infs-preserving )
given d being Function of T,S such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: g is infs-preserving
let X be Subset of S; :: according to WAYBEL_0:def_32 ::_thesis: g preserves_inf_of X
set s = inf X;
assume A2: ex_inf_of X,S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) )
A3: for t being Element of T st t is_<=_than g .: X holds
g . (inf X) >= t
proof
let t be Element of T; ::_thesis: ( t is_<=_than g .: X implies g . (inf X) >= t )
assume A4: t is_<=_than g .: X ; ::_thesis: g . (inf X) >= t
d . t is_<=_than X
proof
let si be Element of S; :: according to LATTICE3:def_8 ::_thesis: ( not si in X or d . t <= si )
assume si in X ; ::_thesis: d . t <= si
then g . si in g .: X by FUNCT_2:35;
then t <= g . si by A4, LATTICE3:def_8;
hence d . t <= si by A1, Th8; ::_thesis: verum
end;
then d . t <= inf X by A2, YELLOW_0:31;
hence g . (inf X) >= t by A1, Th8; ::_thesis: verum
end;
g . (inf X) is_<=_than g .: X
proof
let t be Element of T; :: according to LATTICE3:def_8 ::_thesis: ( not t in g .: X or g . (inf X) <= t )
assume t in g .: X ; ::_thesis: g . (inf X) <= t
then consider si being Element of S such that
A5: si in X and
A6: t = g . si by FUNCT_2:65;
A7: g is monotone by A1, Th8;
reconsider si = si as Element of S ;
inf X is_<=_than X by A2, YELLOW_0:31;
then inf X <= si by A5, LATTICE3:def_8;
hence g . (inf X) <= t by A7, A6, Def2; ::_thesis: verum
end;
hence ( ex_inf_of g .: X,T & "/\" ((g .: X),T) = g . ("/\" (X,S)) ) by A3, YELLOW_0:31; ::_thesis: verum
end;
registration
let S, T be non empty Poset;
cluster Function-like quasi_total upper_adjoint -> infs-preserving for M2( bool [: the carrier of S, the carrier of T:]);
coherence
for b1 being Function of S,T st b1 is upper_adjoint holds
b1 is infs-preserving by Th12;
end;
theorem Th13: :: WAYBEL_1:13
for S, T being non empty Poset
for d being Function of T,S st d is lower_adjoint holds
d is sups-preserving
proof
let S, T be non empty Poset; ::_thesis: for d being Function of T,S st d is lower_adjoint holds
d is sups-preserving
let d be Function of T,S; ::_thesis: ( d is lower_adjoint implies d is sups-preserving )
given g being Function of S,T such that A1: [g,d] is Galois ; :: according to WAYBEL_1:def_12 ::_thesis: d is sups-preserving
let X be Subset of T; :: according to WAYBEL_0:def_33 ::_thesis: d preserves_sup_of X
set t = sup X;
assume A2: ex_sup_of X,T ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of d .: X,S & "\/" ((d .: X),S) = d . ("\/" (X,T)) )
A3: for s being Element of S st s is_>=_than d .: X holds
d . (sup X) <= s
proof
let s be Element of S; ::_thesis: ( s is_>=_than d .: X implies d . (sup X) <= s )
assume A4: s is_>=_than d .: X ; ::_thesis: d . (sup X) <= s
g . s is_>=_than X
proof
let ti be Element of T; :: according to LATTICE3:def_9 ::_thesis: ( not ti in X or ti <= g . s )
assume ti in X ; ::_thesis: ti <= g . s
then d . ti in d .: X by FUNCT_2:35;
then s >= d . ti by A4, LATTICE3:def_9;
hence ti <= g . s by A1, Th8; ::_thesis: verum
end;
then g . s >= sup X by A2, YELLOW_0:30;
hence d . (sup X) <= s by A1, Th8; ::_thesis: verum
end;
d . (sup X) is_>=_than d .: X
proof
let s be Element of S; :: according to LATTICE3:def_9 ::_thesis: ( not s in d .: X or s <= d . (sup X) )
assume s in d .: X ; ::_thesis: s <= d . (sup X)
then consider ti being Element of T such that
A5: ti in X and
A6: s = d . ti by FUNCT_2:65;
A7: d is monotone by A1, Th8;
reconsider ti = ti as Element of T ;
sup X is_>=_than X by A2, YELLOW_0:30;
then sup X >= ti by A5, LATTICE3:def_9;
hence s <= d . (sup X) by A7, A6, Def2; ::_thesis: verum
end;
hence ( ex_sup_of d .: X,S & "\/" ((d .: X),S) = d . ("\/" (X,T)) ) by A3, YELLOW_0:30; ::_thesis: verum
end;
registration
let S, T be non empty Poset;
cluster Function-like quasi_total lower_adjoint -> sups-preserving for M2( bool [: the carrier of S, the carrier of T:]);
coherence
for b1 being Function of S,T st b1 is lower_adjoint holds
b1 is sups-preserving by Th13;
end;
theorem Th14: :: WAYBEL_1:14
for S, T being non empty Poset
for g being Function of S,T st S is complete & g is infs-preserving holds
ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T st S is complete & g is infs-preserving holds
ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
let g be Function of S,T; ::_thesis: ( S is complete & g is infs-preserving implies ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) )
assume that
A1: S is complete and
A2: g is infs-preserving ; ::_thesis: ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
defpred S1[ set , set ] means ex t being Element of T st
( t = $1 & $2 = inf (g " (uparrow t)) );
A3: for e being set st e in the carrier of T holds
ex u being set st
( u in the carrier of S & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier of T implies ex u being set st
( u in the carrier of S & S1[e,u] ) )
assume e in the carrier of T ; ::_thesis: ex u being set st
( u in the carrier of S & S1[e,u] )
then reconsider t = e as Element of T ;
take inf (g " (uparrow t)) ; ::_thesis: ( inf (g " (uparrow t)) in the carrier of S & S1[e, inf (g " (uparrow t))] )
thus ( inf (g " (uparrow t)) in the carrier of S & S1[e, inf (g " (uparrow t))] ) ; ::_thesis: verum
end;
consider d being Function of the carrier of T, the carrier of S such that
A4: for e being set st e in the carrier of T holds
S1[e,d . e] from FUNCT_2:sch_1(A3);
A5: for t being Element of T holds d . t = inf (g " (uparrow t))
proof
let t be Element of T; ::_thesis: d . t = inf (g " (uparrow t))
ex t1 being Element of T st
( t1 = t & d . t = inf (g " (uparrow t1)) ) by A4;
hence d . t = inf (g " (uparrow t)) ; ::_thesis: verum
end;
reconsider d = d as Function of T,S ;
for X being Filter of S holds g preserves_inf_of X by A2, WAYBEL_0:def_32;
then A6: g is monotone by WAYBEL_0:69;
A7: for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )
proof
let t be Element of T; ::_thesis: for s being Element of S holds
( t <= g . s iff d . t <= s )
let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s )
A8: ex_inf_of uparrow t,T by WAYBEL_0:39;
A9: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17;
then inf (g " (uparrow t)) is_<=_than g " (uparrow t) by YELLOW_0:31;
then A10: d . t is_<=_than g " (uparrow t) by A5;
hereby ::_thesis: ( d . t <= s implies t <= g . s )
assume t <= g . s ; ::_thesis: d . t <= s
then g . s in uparrow t by WAYBEL_0:18;
then s in g " (uparrow t) by FUNCT_2:38;
hence d . t <= s by A10, LATTICE3:def_8; ::_thesis: verum
end;
g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def_32;
then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A9, WAYBEL_0:def_30;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A8, FUNCT_1:75, YELLOW_0:35;
then A11: g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39;
assume d . t <= s ; ::_thesis: t <= g . s
then g . (d . t) <= g . s by A6, Def2;
then g . (inf (g " (uparrow t))) <= g . s by A5;
hence t <= g . s by A11, ORDERS_2:3; ::_thesis: verum
end;
take d ; ::_thesis: ( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) )
d is monotone
proof
let t1, t2 be Element of T; :: according to WAYBEL_1:def_2 ::_thesis: ( t1 <= t2 implies d . t1 <= d . t2 )
assume t1 <= t2 ; ::_thesis: d . t1 <= d . t2
then A12: uparrow t2 c= uparrow t1 by WAYBEL_0:22;
( ex_inf_of g " (uparrow t1),S & ex_inf_of g " (uparrow t2),S ) by A1, YELLOW_0:17;
then inf (g " (uparrow t1)) <= inf (g " (uparrow t2)) by A12, RELAT_1:143, YELLOW_0:35;
then d . t1 <= inf (g " (uparrow t2)) by A5;
hence d . t1 <= d . t2 by A5; ::_thesis: verum
end;
hence [g,d] is Galois by A6, A7, Th8; ::_thesis: for t being Element of T holds d . t is_minimum_of g " (uparrow t)
let t be Element of T; ::_thesis: d . t is_minimum_of g " (uparrow t)
thus A13: ex_inf_of g " (uparrow t),S by A1, YELLOW_0:17; :: according to WAYBEL_1:def_6 ::_thesis: ( d . t = "/\" ((g " (uparrow t)),S) & "/\" ((g " (uparrow t)),S) in g " (uparrow t) )
thus A14: d . t = inf (g " (uparrow t)) by A5; ::_thesis: "/\" ((g " (uparrow t)),S) in g " (uparrow t)
A15: ex_inf_of uparrow t,T by WAYBEL_0:39;
g preserves_inf_of g " (uparrow t) by A2, WAYBEL_0:def_32;
then ( ex_inf_of g .: (g " (uparrow t)),T & g . (inf (g " (uparrow t))) = inf (g .: (g " (uparrow t))) ) by A13, WAYBEL_0:def_30;
then g . (inf (g " (uparrow t))) >= inf (uparrow t) by A15, FUNCT_1:75, YELLOW_0:35;
then g . (inf (g " (uparrow t))) >= t by WAYBEL_0:39;
then g . (d . t) >= t by A5;
then g . (d . t) in uparrow t by WAYBEL_0:18;
hence "/\" ((g " (uparrow t)),S) in g " (uparrow t) by A14, FUNCT_2:38; ::_thesis: verum
end;
theorem Th15: :: WAYBEL_1:15
for S, T being non empty Poset
for d being Function of T,S st T is complete & d is sups-preserving holds
ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
proof
let S, T be non empty Poset; ::_thesis: for d being Function of T,S st T is complete & d is sups-preserving holds
ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
let d be Function of T,S; ::_thesis: ( T is complete & d is sups-preserving implies ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) )
assume that
A1: T is complete and
A2: d is sups-preserving ; ::_thesis: ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
defpred S1[ set , set ] means ex s being Element of S st
( s = $1 & $2 = sup (d " (downarrow s)) );
A3: for e being set st e in the carrier of S holds
ex u being set st
( u in the carrier of T & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in the carrier of S implies ex u being set st
( u in the carrier of T & S1[e,u] ) )
assume e in the carrier of S ; ::_thesis: ex u being set st
( u in the carrier of T & S1[e,u] )
then reconsider s = e as Element of S ;
take sup (d " (downarrow s)) ; ::_thesis: ( sup (d " (downarrow s)) in the carrier of T & S1[e, sup (d " (downarrow s))] )
thus ( sup (d " (downarrow s)) in the carrier of T & S1[e, sup (d " (downarrow s))] ) ; ::_thesis: verum
end;
consider g being Function of the carrier of S, the carrier of T such that
A4: for e being set st e in the carrier of S holds
S1[e,g . e] from FUNCT_2:sch_1(A3);
A5: for s being Element of S holds g . s = sup (d " (downarrow s))
proof
let s be Element of S; ::_thesis: g . s = sup (d " (downarrow s))
ex s1 being Element of S st
( s1 = s & g . s = sup (d " (downarrow s1)) ) by A4;
hence g . s = sup (d " (downarrow s)) ; ::_thesis: verum
end;
reconsider g = g as Function of S,T ;
for X being Ideal of T holds d preserves_sup_of X by A2, WAYBEL_0:def_33;
then A6: d is monotone by WAYBEL_0:72;
A7: for t being Element of T
for s being Element of S holds
( s >= d . t iff g . s >= t )
proof
let t be Element of T; ::_thesis: for s being Element of S holds
( s >= d . t iff g . s >= t )
let s be Element of S; ::_thesis: ( s >= d . t iff g . s >= t )
A8: ex_sup_of downarrow s,S by WAYBEL_0:34;
A9: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17;
then sup (d " (downarrow s)) is_>=_than d " (downarrow s) by YELLOW_0:30;
then A10: g . s is_>=_than d " (downarrow s) by A5;
hereby ::_thesis: ( g . s >= t implies s >= d . t )
assume s >= d . t ; ::_thesis: g . s >= t
then d . t in downarrow s by WAYBEL_0:17;
then t in d " (downarrow s) by FUNCT_2:38;
hence g . s >= t by A10, LATTICE3:def_9; ::_thesis: verum
end;
d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def_33;
then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A9, WAYBEL_0:def_31;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A8, FUNCT_1:75, YELLOW_0:34;
then A11: d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34;
assume g . s >= t ; ::_thesis: s >= d . t
then d . (g . s) >= d . t by A6, Def2;
then d . (sup (d " (downarrow s))) >= d . t by A5;
hence s >= d . t by A11, ORDERS_2:3; ::_thesis: verum
end;
take g ; ::_thesis: ( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) )
g is monotone
proof
let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies g . s1 <= g . s2 )
assume s1 <= s2 ; ::_thesis: g . s1 <= g . s2
then A12: downarrow s1 c= downarrow s2 by WAYBEL_0:21;
( ex_sup_of d " (downarrow s1),T & ex_sup_of d " (downarrow s2),T ) by A1, YELLOW_0:17;
then sup (d " (downarrow s1)) <= sup (d " (downarrow s2)) by A12, RELAT_1:143, YELLOW_0:34;
then g . s1 <= sup (d " (downarrow s2)) by A5;
hence g . s1 <= g . s2 by A5; ::_thesis: verum
end;
hence [g,d] is Galois by A6, A7, Th8; ::_thesis: for s being Element of S holds g . s is_maximum_of d " (downarrow s)
let s be Element of S; ::_thesis: g . s is_maximum_of d " (downarrow s)
thus A13: ex_sup_of d " (downarrow s),T by A1, YELLOW_0:17; :: according to WAYBEL_1:def_7 ::_thesis: ( g . s = "\/" ((d " (downarrow s)),T) & "\/" ((d " (downarrow s)),T) in d " (downarrow s) )
thus A14: g . s = sup (d " (downarrow s)) by A5; ::_thesis: "\/" ((d " (downarrow s)),T) in d " (downarrow s)
A15: ex_sup_of downarrow s,S by WAYBEL_0:34;
d preserves_sup_of d " (downarrow s) by A2, WAYBEL_0:def_33;
then ( ex_sup_of d .: (d " (downarrow s)),S & d . (sup (d " (downarrow s))) = sup (d .: (d " (downarrow s))) ) by A13, WAYBEL_0:def_31;
then d . (sup (d " (downarrow s))) <= sup (downarrow s) by A15, FUNCT_1:75, YELLOW_0:34;
then d . (sup (d " (downarrow s))) <= s by WAYBEL_0:34;
then d . (g . s) <= s by A5;
then d . (g . s) in downarrow s by WAYBEL_0:17;
hence "\/" ((d " (downarrow s)),T) in d " (downarrow s) by A14, FUNCT_2:38; ::_thesis: verum
end;
theorem :: WAYBEL_1:16
for S, T being non empty Poset
for g being Function of S,T st S is complete holds
( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T st S is complete holds
( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )
let g be Function of S,T; ::_thesis: ( S is complete implies ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) ) )
assume A1: S is complete ; ::_thesis: ( g is infs-preserving iff ( g is monotone & g is upper_adjoint ) )
hereby ::_thesis: ( g is monotone & g is upper_adjoint implies g is infs-preserving )
assume g is infs-preserving ; ::_thesis: ( g is monotone & g is upper_adjoint )
then ex d being Function of T,S st
( [g,d] is Galois & ( for t being Element of T holds d . t is_minimum_of g " (uparrow t) ) ) by A1, Th14;
hence ( g is monotone & g is upper_adjoint ) by Def11, Th10; ::_thesis: verum
end;
assume g is monotone ; ::_thesis: ( not g is upper_adjoint or g is infs-preserving )
assume ex d being Function of T,S st [g,d] is Galois ; :: according to WAYBEL_1:def_11 ::_thesis: g is infs-preserving
then g is upper_adjoint by Def11;
hence g is infs-preserving ; ::_thesis: verum
end;
theorem Th17: :: WAYBEL_1:17
for S, T being non empty Poset
for d being Function of T,S st T is complete holds
( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
proof
let S, T be non empty Poset; ::_thesis: for d being Function of T,S st T is complete holds
( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
let d be Function of T,S; ::_thesis: ( T is complete implies ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) ) )
assume A1: T is complete ; ::_thesis: ( d is sups-preserving iff ( d is monotone & d is lower_adjoint ) )
hereby ::_thesis: ( d is monotone & d is lower_adjoint implies d is sups-preserving )
assume d is sups-preserving ; ::_thesis: ( d is monotone & d is lower_adjoint )
then ex g being Function of S,T st
( [g,d] is Galois & ( for s being Element of S holds g . s is_maximum_of d " (downarrow s) ) ) by A1, Th15;
hence ( d is monotone & d is lower_adjoint ) by Def12, Th11; ::_thesis: verum
end;
assume d is monotone ; ::_thesis: ( not d is lower_adjoint or d is sups-preserving )
assume ex g being Function of S,T st [g,d] is Galois ; :: according to WAYBEL_1:def_12 ::_thesis: d is sups-preserving
then d is lower_adjoint by Def12;
hence d is sups-preserving ; ::_thesis: verum
end;
theorem Th18: :: WAYBEL_1:18
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds
( d * g <= id S & id T <= g * d )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( d * g <= id S & id T <= g * d ) )
assume A1: [g,d] is Galois ; ::_thesis: ( d * g <= id S & id T <= g * d )
for s being Element of S holds (d * g) . s <= (id S) . s
proof
let s be Element of S; ::_thesis: (d * g) . s <= (id S) . s
d . (g . s) <= s by A1, Th8;
then (d * g) . s <= s by FUNCT_2:15;
hence (d * g) . s <= (id S) . s by FUNCT_1:18; ::_thesis: verum
end;
hence d * g <= id S by YELLOW_2:9; ::_thesis: id T <= g * d
for t being Element of T holds (id T) . t <= (g * d) . t
proof
let t be Element of T; ::_thesis: (id T) . t <= (g * d) . t
t <= g . (d . t) by A1, Th8;
then t <= (g * d) . t by FUNCT_2:15;
hence (id T) . t <= (g * d) . t by FUNCT_1:18; ::_thesis: verum
end;
hence id T <= g * d by YELLOW_2:9; ::_thesis: verum
end;
theorem Th19: :: WAYBEL_1:19
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois
let g be Function of S,T; ::_thesis: for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
[g,d] is Galois
let d be Function of T,S; ::_thesis: ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies [g,d] is Galois )
assume that
A1: g is monotone and
A2: d is monotone and
A3: d * g <= id S and
A4: id T <= g * d ; ::_thesis: [g,d] is Galois
for t being Element of T
for s being Element of S holds
( t <= g . s iff d . t <= s )
proof
let t be Element of T; ::_thesis: for s being Element of S holds
( t <= g . s iff d . t <= s )
let s be Element of S; ::_thesis: ( t <= g . s iff d . t <= s )
hereby ::_thesis: ( d . t <= s implies t <= g . s )
(d * g) . s <= (id S) . s by A3, YELLOW_2:9;
then d . (g . s) <= (id S) . s by FUNCT_2:15;
then A5: d . (g . s) <= s by FUNCT_1:18;
assume t <= g . s ; ::_thesis: d . t <= s
then d . t <= d . (g . s) by A2, Def2;
hence d . t <= s by A5, ORDERS_2:3; ::_thesis: verum
end;
(id T) . t <= (g * d) . t by A4, YELLOW_2:9;
then (id T) . t <= g . (d . t) by FUNCT_2:15;
then A6: t <= g . (d . t) by FUNCT_1:18;
assume d . t <= s ; ::_thesis: t <= g . s
then g . (d . t) <= g . s by A1, Def2;
hence t <= g . s by A6, ORDERS_2:3; ::_thesis: verum
end;
hence [g,d] is Galois by A1, A2, Th8; ::_thesis: verum
end;
theorem Th20: :: WAYBEL_1:20
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
( d = (d * g) * d & g = (g * d) * g )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
( d = (d * g) * d & g = (g * d) * g )
let g be Function of S,T; ::_thesis: for d being Function of T,S st g is monotone & d is monotone & d * g <= id S & id T <= g * d holds
( d = (d * g) * d & g = (g * d) * g )
let d be Function of T,S; ::_thesis: ( g is monotone & d is monotone & d * g <= id S & id T <= g * d implies ( d = (d * g) * d & g = (g * d) * g ) )
assume that
A1: g is monotone and
A2: d is monotone and
A3: d * g <= id S and
A4: id T <= g * d ; ::_thesis: ( d = (d * g) * d & g = (g * d) * g )
for t being Element of T holds d . t = ((d * g) * d) . t
proof
let t be Element of T; ::_thesis: d . t = ((d * g) * d) . t
(id T) . t <= (g * d) . t by A4, YELLOW_2:9;
then t <= (g * d) . t by FUNCT_1:18;
then d . t <= d . ((g * d) . t) by A2, Def2;
then d . t <= (d * (g * d)) . t by FUNCT_2:15;
then A5: d . t <= ((d * g) * d) . t by RELAT_1:36;
(d * g) . (d . t) <= (id S) . (d . t) by A3, YELLOW_2:9;
then (d * g) . (d . t) <= d . t by FUNCT_1:18;
then d . t >= ((d * g) * d) . t by FUNCT_2:15;
hence d . t = ((d * g) * d) . t by A5, ORDERS_2:2; ::_thesis: verum
end;
hence d = (d * g) * d by FUNCT_2:63; ::_thesis: g = (g * d) * g
for s being Element of S holds g . s = ((g * d) * g) . s
proof
let s be Element of S; ::_thesis: g . s = ((g * d) * g) . s
(d * g) . s <= (id S) . s by A3, YELLOW_2:9;
then (d * g) . s <= s by FUNCT_1:18;
then g . ((d * g) . s) <= g . s by A1, Def2;
then (g * (d * g)) . s <= g . s by FUNCT_2:15;
then A6: g . s >= ((g * d) * g) . s by RELAT_1:36;
(id T) . (g . s) <= (g * d) . (g . s) by A4, YELLOW_2:9;
then g . s <= (g * d) . (g . s) by FUNCT_1:18;
then g . s <= ((g * d) * g) . s by FUNCT_2:15;
hence g . s = ((g * d) * g) . s by A6, ORDERS_2:2; ::_thesis: verum
end;
hence g = (g * d) * g by FUNCT_2:63; ::_thesis: verum
end;
theorem Th21: :: WAYBEL_1:21
for S, T being non empty RelStr
for g being Function of S,T
for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
proof
let S, T be non empty RelStr ; ::_thesis: for g being Function of S,T
for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
let g be Function of S,T; ::_thesis: for d being Function of T,S st g = (g * d) * g holds
g * d is idempotent
let d be Function of T,S; ::_thesis: ( g = (g * d) * g implies g * d is idempotent )
assume g = (g * d) * g ; ::_thesis: g * d is idempotent
hence (g * d) * (g * d) = g * d by RELAT_1:36; :: according to QUANTAL1:def_9 ::_thesis: verum
end;
theorem Th22: :: WAYBEL_1:22
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois & g is onto holds
for t being Element of T holds d . t is_minimum_of g " {t}
let d be Function of T,S; ::_thesis: ( [g,d] is Galois & g is onto implies for t being Element of T holds d . t is_minimum_of g " {t} )
assume that
A1: [g,d] is Galois and
A2: g is onto ; ::_thesis: for t being Element of T holds d . t is_minimum_of g " {t}
A3: g is monotone by A1, Th8;
let t be Element of T; ::_thesis: d . t is_minimum_of g " {t}
A4: rng g = the carrier of T by A2, FUNCT_2:def_3;
then A5: g .: (g " (uparrow t)) = uparrow t by FUNCT_1:77;
A6: d . t is_minimum_of g " (uparrow t) by A1, Th10;
then A7: d . t = inf (g " (uparrow t)) by Def6;
then d . t in g " (uparrow t) by A6, Def6;
then g . (d . t) in g .: (g " (uparrow t)) by FUNCT_2:35;
then A8: t <= g . (d . t) by A5, WAYBEL_0:18;
ex_inf_of g " (uparrow t),S by A6, Def6;
then A9: d . t is_<=_than g " (uparrow t) by A7, YELLOW_0:31;
consider s being set such that
A10: s in the carrier of S and
A11: g . s = t by A4, FUNCT_2:11;
reconsider s = s as Element of S by A10;
A12: t in {t} by TARSKI:def_1;
A13: {t} c= uparrow {t} by WAYBEL_0:16;
then s in g " (uparrow t) by A11, A12, FUNCT_2:38;
then d . t <= s by A9, LATTICE3:def_8;
then g . (d . t) <= t by A11, A3, Def2;
then A14: g . (d . t) = t by A8, ORDERS_2:2;
then A15: d . t in g " {t} by A12, FUNCT_2:38;
A16: g " {t} c= g " (uparrow t) by RELAT_1:143, WAYBEL_0:16;
thus A17: ex_inf_of g " {t},S :: according to WAYBEL_1:def_6 ::_thesis: ( d . t = "/\" ((g " {t}),S) & "/\" ((g " {t}),S) in g " {t} )
proof
take d . t ; :: according to YELLOW_0:def_8 ::_thesis: ( d . t is_<=_than g " {t} & ( for b1 being M2( the carrier of S) holds
( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M2( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) )
thus g " {t} is_>=_than d . t by A9, A16, YELLOW_0:9; ::_thesis: ( ( for b1 being M2( the carrier of S) holds
( not b1 is_<=_than g " {t} or b1 <= d . t ) ) & ( for b1 being M2( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t ) ) )
thus for b being Element of S st g " {t} is_>=_than b holds
b <= d . t by A15, LATTICE3:def_8; ::_thesis: for b1 being M2( the carrier of S) holds
( not b1 is_<=_than g " {t} or ex b2 being M2( the carrier of S) st
( b2 is_<=_than g " {t} & not b2 <= b1 ) or b1 = d . t )
let c be Element of S; ::_thesis: ( not c is_<=_than g " {t} or ex b1 being M2( the carrier of S) st
( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t )
assume g " {t} is_>=_than c ; ::_thesis: ( ex b1 being M2( the carrier of S) st
( b1 is_<=_than g " {t} & not b1 <= c ) or c = d . t )
then A18: c <= d . t by A15, LATTICE3:def_8;
assume for b being Element of S st g " {t} is_>=_than b holds
b <= c ; ::_thesis: c = d . t
then d . t <= c by A9, A16, YELLOW_0:9;
hence c = d . t by A18, ORDERS_2:2; ::_thesis: verum
end;
then inf (g " {t}) is_<=_than g " {t} by YELLOW_0:31;
then A19: inf (g " {t}) <= d . t by A15, LATTICE3:def_8;
ex_inf_of g " (uparrow t),S by A6, Def6;
then inf (g " {t}) >= d . t by A7, A13, A17, RELAT_1:143, YELLOW_0:35;
hence d . t = inf (g " {t}) by A19, ORDERS_2:2; ::_thesis: "/\" ((g " {t}),S) in g " {t}
hence "/\" ((g " {t}),S) in g " {t} by A12, A14, FUNCT_2:38; ::_thesis: verum
end;
theorem Th23: :: WAYBEL_1:23
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T
let g be Function of S,T; ::_thesis: for d being Function of T,S st ( for t being Element of T holds d . t is_minimum_of g " {t} ) holds
g * d = id T
let d be Function of T,S; ::_thesis: ( ( for t being Element of T holds d . t is_minimum_of g " {t} ) implies g * d = id T )
assume A1: for t being Element of T holds d . t is_minimum_of g " {t} ; ::_thesis: g * d = id T
for t being Element of T holds (g * d) . t = t
proof
let t be Element of T; ::_thesis: (g * d) . t = t
d . t is_minimum_of g " {t} by A1;
then ( d . t = inf (g " {t}) & inf (g " {t}) in g " {t} ) by Def6;
then g . (d . t) in {t} by FUNCT_2:38;
then g . (d . t) = t by TARSKI:def_1;
hence (g * d) . t = t by FUNCT_2:15; ::_thesis: verum
end;
hence g * d = id T by FUNCT_2:124; ::_thesis: verum
end;
theorem :: WAYBEL_1:24
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is V13() )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is V13() )
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds
( g is onto iff d is V13() )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is onto iff d is V13() ) )
A1: ( the carrier of T = dom d & the carrier of T = dom (g * d) ) by FUNCT_2:def_1;
assume A2: [g,d] is Galois ; ::_thesis: ( g is onto iff d is V13() )
then A3: ( d * g <= id S & id T <= g * d ) by Th18;
hereby ::_thesis: ( d is V13() implies g is onto )
assume g is onto ; ::_thesis: d is V13()
then for t being Element of T holds d . t is_minimum_of g " {t} by A2, Th22;
then g * d = id T by Th23;
hence d is V13() by FUNCT_2:23; ::_thesis: verum
end;
A4: rng (g * d) c= the carrier of T ;
( g is monotone & d is monotone ) by A2, Th8;
then A5: d = (d * g) * d by A3, Th20
.= d * (g * d) by RELAT_1:36 ;
assume d is V13() ; ::_thesis: g is onto
then g * d = id T by A1, A4, A5, FUNCT_1:28;
hence g is onto by FUNCT_2:23; ::_thesis: verum
end;
theorem Th25: :: WAYBEL_1:25
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois & d is onto holds
for s being Element of S holds g . s is_maximum_of d " {s}
let d be Function of T,S; ::_thesis: ( [g,d] is Galois & d is onto implies for s being Element of S holds g . s is_maximum_of d " {s} )
assume that
A1: [g,d] is Galois and
A2: d is onto ; ::_thesis: for s being Element of S holds g . s is_maximum_of d " {s}
A3: d is monotone by A1, Th8;
let s be Element of S; ::_thesis: g . s is_maximum_of d " {s}
A4: rng d = the carrier of S by A2, FUNCT_2:def_3;
then A5: d .: (d " (downarrow s)) = downarrow s by FUNCT_1:77;
A6: g . s is_maximum_of d " (downarrow s) by A1, Th11;
then A7: g . s = sup (d " (downarrow s)) by Def7;
then g . s in d " (downarrow s) by A6, Def7;
then d . (g . s) in d .: (d " (downarrow s)) by FUNCT_2:35;
then A8: s >= d . (g . s) by A5, WAYBEL_0:17;
ex_sup_of d " (downarrow s),T by A6, Def7;
then A9: g . s is_>=_than d " (downarrow s) by A7, YELLOW_0:30;
consider t being set such that
A10: t in the carrier of T and
A11: d . t = s by A4, FUNCT_2:11;
reconsider t = t as Element of T by A10;
A12: s in {s} by TARSKI:def_1;
A13: {s} c= downarrow {s} by WAYBEL_0:16;
then t in d " (downarrow s) by A11, A12, FUNCT_2:38;
then g . s >= t by A9, LATTICE3:def_9;
then d . (g . s) >= s by A11, A3, Def2;
then A14: d . (g . s) = s by A8, ORDERS_2:2;
then A15: g . s in d " {s} by A12, FUNCT_2:38;
A16: d " {s} c= d " (downarrow s) by RELAT_1:143, WAYBEL_0:16;
thus A17: ex_sup_of d " {s},T :: according to WAYBEL_1:def_7 ::_thesis: ( g . s = "\/" ((d " {s}),T) & "\/" ((d " {s}),T) in d " {s} )
proof
take g . s ; :: according to YELLOW_0:def_7 ::_thesis: ( d " {s} is_<=_than g . s & ( for b1 being M2( the carrier of T) holds
( not d " {s} is_<=_than b1 or g . s <= b1 ) ) & ( for b1 being M2( the carrier of T) holds
( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st
( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s ) ) )
thus d " {s} is_<=_than g . s by A9, A16, YELLOW_0:9; ::_thesis: ( ( for b1 being M2( the carrier of T) holds
( not d " {s} is_<=_than b1 or g . s <= b1 ) ) & ( for b1 being M2( the carrier of T) holds
( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st
( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s ) ) )
thus for b being Element of T st d " {s} is_<=_than b holds
b >= g . s by A15, LATTICE3:def_9; ::_thesis: for b1 being M2( the carrier of T) holds
( not d " {s} is_<=_than b1 or ex b2 being M2( the carrier of T) st
( d " {s} is_<=_than b2 & not b1 <= b2 ) or b1 = g . s )
let c be Element of T; ::_thesis: ( not d " {s} is_<=_than c or ex b1 being M2( the carrier of T) st
( d " {s} is_<=_than b1 & not c <= b1 ) or c = g . s )
assume d " {s} is_<=_than c ; ::_thesis: ( ex b1 being M2( the carrier of T) st
( d " {s} is_<=_than b1 & not c <= b1 ) or c = g . s )
then A18: c >= g . s by A15, LATTICE3:def_9;
assume for b being Element of T st d " {s} is_<=_than b holds
b >= c ; ::_thesis: c = g . s
then g . s >= c by A9, A16, YELLOW_0:9;
hence c = g . s by A18, ORDERS_2:2; ::_thesis: verum
end;
then sup (d " {s}) is_>=_than d " {s} by YELLOW_0:30;
then A19: sup (d " {s}) >= g . s by A15, LATTICE3:def_9;
ex_sup_of d " (downarrow s),T by A6, Def7;
then sup (d " {s}) <= g . s by A7, A13, A17, RELAT_1:143, YELLOW_0:34;
hence g . s = sup (d " {s}) by A19, ORDERS_2:2; ::_thesis: "\/" ((d " {s}),T) in d " {s}
hence "\/" ((d " {s}),T) in d " {s} by A12, A14, FUNCT_2:38; ::_thesis: verum
end;
theorem Th26: :: WAYBEL_1:26
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S
let g be Function of S,T; ::_thesis: for d being Function of T,S st ( for s being Element of S holds g . s is_maximum_of d " {s} ) holds
d * g = id S
let d be Function of T,S; ::_thesis: ( ( for s being Element of S holds g . s is_maximum_of d " {s} ) implies d * g = id S )
assume A1: for s being Element of S holds g . s is_maximum_of d " {s} ; ::_thesis: d * g = id S
for s being Element of S holds (d * g) . s = s
proof
let s be Element of S; ::_thesis: (d * g) . s = s
g . s is_maximum_of d " {s} by A1;
then ( g . s = sup (d " {s}) & sup (d " {s}) in d " {s} ) by Def7;
then d . (g . s) in {s} by FUNCT_2:38;
then d . (g . s) = s by TARSKI:def_1;
hence (d * g) . s = s by FUNCT_2:15; ::_thesis: verum
end;
hence d * g = id S by FUNCT_2:124; ::_thesis: verum
end;
theorem :: WAYBEL_1:27
for S, T being non empty Poset
for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is V13() iff d is onto )
proof
let S, T be non empty Poset; ::_thesis: for g being Function of S,T
for d being Function of T,S st [g,d] is Galois holds
( g is V13() iff d is onto )
let g be Function of S,T; ::_thesis: for d being Function of T,S st [g,d] is Galois holds
( g is V13() iff d is onto )
let d be Function of T,S; ::_thesis: ( [g,d] is Galois implies ( g is V13() iff d is onto ) )
assume A1: [g,d] is Galois ; ::_thesis: ( g is V13() iff d is onto )
hereby ::_thesis: ( d is onto implies g is V13() )
A2: ( d * g <= id S & id T <= g * d ) by A1, Th18;
( g is monotone & d is monotone ) by A1, Th8;
then A3: g = (g * d) * g by A2, Th20
.= g * (d * g) by RELAT_1:36 ;
A4: ( the carrier of S = dom g & the carrier of S = dom (d * g) ) by FUNCT_2:def_1;
A5: rng (d * g) c= the carrier of S ;
assume g is V13() ; ::_thesis: d is onto
then d * g = id S by A4, A5, A3, FUNCT_1:28;
hence d is onto by FUNCT_2:23; ::_thesis: verum
end;
assume d is onto ; ::_thesis: g is V13()
then for s being Element of S holds g . s is_maximum_of d " {s} by A1, Th25;
then d * g = id S by Th26;
hence g is V13() by FUNCT_2:23; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let p be Function of L,L;
attrp is projection means :Def13: :: WAYBEL_1:def 13
( p is idempotent & p is monotone );
end;
:: deftheorem Def13 defines projection WAYBEL_1:def_13_:_
for L being non empty RelStr
for p being Function of L,L holds
( p is projection iff ( p is idempotent & p is monotone ) );
registration
let L be non empty RelStr ;
cluster id L -> projection ;
coherence
id L is projection
proof
thus id L is idempotent by YELLOW_2:21; :: according to WAYBEL_1:def_13 ::_thesis: id L is monotone
thus id L is monotone ; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total projection for M2( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is projection
proof
take id L ; ::_thesis: id L is projection
thus id L is projection ; ::_thesis: verum
end;
end;
definition
let L be non empty RelStr ;
let c be Function of L,L;
attrc is closure means :Def14: :: WAYBEL_1:def 14
( c is projection & id L <= c );
end;
:: deftheorem Def14 defines closure WAYBEL_1:def_14_:_
for L being non empty RelStr
for c being Function of L,L holds
( c is closure iff ( c is projection & id L <= c ) );
registration
let L be non empty RelStr ;
cluster Function-like quasi_total closure -> projection for M2( bool [: the carrier of L, the carrier of L:]);
coherence
for b1 being Function of L,L st b1 is closure holds
b1 is projection by Def14;
end;
Lm1: for L1, L2 being non empty RelStr
for f being Function of L1,L2 st L2 is reflexive holds
f <= f
proof
let L1, L2 be non empty RelStr ; ::_thesis: for f being Function of L1,L2 st L2 is reflexive holds
f <= f
let f be Function of L1,L2; ::_thesis: ( L2 is reflexive implies f <= f )
assume L2 is reflexive ; ::_thesis: f <= f
then for x being Element of L1 holds f . x <= f . x by ORDERS_2:1;
hence f <= f by YELLOW_2:9; ::_thesis: verum
end;
registration
let L be non empty reflexive RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total closure for M2( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is closure
proof
take id L ; ::_thesis: id L is closure
thus id L is projection ; :: according to WAYBEL_1:def_14 ::_thesis: id L <= id L
thus id L <= id L by Lm1; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive RelStr ;
cluster id L -> closure ;
coherence
id L is closure
proof
thus id L is projection ; :: according to WAYBEL_1:def_14 ::_thesis: id L <= id L
thus id L <= id L by Lm1; ::_thesis: verum
end;
end;
definition
let L be non empty RelStr ;
let k be Function of L,L;
attrk is kernel means :Def15: :: WAYBEL_1:def 15
( k is projection & k <= id L );
end;
:: deftheorem Def15 defines kernel WAYBEL_1:def_15_:_
for L being non empty RelStr
for k being Function of L,L holds
( k is kernel iff ( k is projection & k <= id L ) );
registration
let L be non empty RelStr ;
cluster Function-like quasi_total kernel -> projection for M2( bool [: the carrier of L, the carrier of L:]);
coherence
for b1 being Function of L,L st b1 is kernel holds
b1 is projection by Def15;
end;
registration
let L be non empty reflexive RelStr ;
cluster non empty V7() V10( the carrier of L) V11( the carrier of L) Function-like V27( the carrier of L) quasi_total kernel for M2( bool [: the carrier of L, the carrier of L:]);
existence
ex b1 being Function of L,L st b1 is kernel
proof
take id L ; ::_thesis: id L is kernel
thus id L is projection ; :: according to WAYBEL_1:def_15 ::_thesis: id L <= id L
thus id L <= id L by Lm1; ::_thesis: verum
end;
end;
registration
let L be non empty reflexive RelStr ;
cluster id L -> kernel ;
coherence
id L is kernel
proof
thus id L is projection ; :: according to WAYBEL_1:def_15 ::_thesis: id L <= id L
thus id L <= id L by Lm1; ::_thesis: verum
end;
end;
Lm2: for L being non empty 1-sorted
for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
proof
let L be non empty 1-sorted ; ::_thesis: for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
let p be Function of L,L; ::_thesis: ( p is idempotent implies for x being set st x in rng p holds
p . x = x )
assume A1: p is idempotent ; ::_thesis: for x being set st x in rng p holds
p . x = x
let x be set ; ::_thesis: ( x in rng p implies p . x = x )
assume x in rng p ; ::_thesis: p . x = x
then ex a being set st
( a in dom p & x = p . a ) by FUNCT_1:def_3;
hence p . x = x by A1, YELLOW_2:18; ::_thesis: verum
end;
theorem Th28: :: WAYBEL_1:28
for L being non empty Poset
for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
proof
let L be non empty Poset; ::_thesis: for c being Function of L,L
for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
let c be Function of L,L; ::_thesis: for X being Subset of L st c is closure & ex_inf_of X,L & X c= rng c holds
inf X = c . (inf X)
let X be Subset of L; ::_thesis: ( c is closure & ex_inf_of X,L & X c= rng c implies inf X = c . (inf X) )
assume that
A1: c is projection and
A2: id L <= c and
A3: ex_inf_of X,L and
A4: X c= rng c ; :: according to WAYBEL_1:def_14 ::_thesis: inf X = c . (inf X)
A5: c is monotone by A1, Def13;
A6: c is idempotent by A1, Def13;
c . (inf X) is_<=_than X
proof
let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or c . (inf X) <= x )
assume A7: x in X ; ::_thesis: c . (inf X) <= x
inf X is_<=_than X by A3, YELLOW_0:31;
then inf X <= x by A7, LATTICE3:def_8;
then c . (inf X) <= c . x by A5, Def2;
hence c . (inf X) <= x by A4, A6, A7, Lm2; ::_thesis: verum
end;
then A8: c . (inf X) <= inf X by A3, YELLOW_0:31;
(id L) . (inf X) <= c . (inf X) by A2, YELLOW_2:9;
then inf X <= c . (inf X) by FUNCT_1:18;
hence inf X = c . (inf X) by A8, ORDERS_2:2; ::_thesis: verum
end;
theorem Th29: :: WAYBEL_1:29
for L being non empty Poset
for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
proof
let L be non empty Poset; ::_thesis: for k being Function of L,L
for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
let k be Function of L,L; ::_thesis: for X being Subset of L st k is kernel & ex_sup_of X,L & X c= rng k holds
sup X = k . (sup X)
let X be Subset of L; ::_thesis: ( k is kernel & ex_sup_of X,L & X c= rng k implies sup X = k . (sup X) )
assume that
A1: k is projection and
A2: k <= id L and
A3: ex_sup_of X,L and
A4: X c= rng k ; :: according to WAYBEL_1:def_15 ::_thesis: sup X = k . (sup X)
A5: k is monotone by A1, Def13;
A6: k is idempotent by A1, Def13;
k . (sup X) is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= k . (sup X) )
assume A7: x in X ; ::_thesis: x <= k . (sup X)
sup X is_>=_than X by A3, YELLOW_0:30;
then sup X >= x by A7, LATTICE3:def_9;
then k . (sup X) >= k . x by A5, Def2;
hence x <= k . (sup X) by A4, A6, A7, Lm2; ::_thesis: verum
end;
then A8: k . (sup X) >= sup X by A3, YELLOW_0:30;
(id L) . (sup X) >= k . (sup X) by A2, YELLOW_2:9;
then sup X >= k . (sup X) by FUNCT_1:18;
hence sup X = k . (sup X) by A8, ORDERS_2:2; ::_thesis: verum
end;
definition
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
func corestr g -> Function of L1,(Image g) equals :: WAYBEL_1:def 16
the carrier of (Image g) |` g;
coherence
the carrier of (Image g) |` g is Function of L1,(Image g)
proof
A1: the carrier of L1 = dom g by FUNCT_2:def_1;
A2: the carrier of (Image g) = rng g by YELLOW_0:def_15;
then the carrier of (Image g) |` g = g by RELAT_1:94;
hence the carrier of (Image g) |` g is Function of L1,(Image g) by A2, A1, FUNCT_2:1; ::_thesis: verum
end;
end;
:: deftheorem defines corestr WAYBEL_1:def_16_:_
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = the carrier of (Image g) |` g;
theorem Th30: :: WAYBEL_1:30
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g = g
proof
let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds corestr g = g
let g be Function of L1,L2; ::_thesis: corestr g = g
the carrier of (Image g) = rng g by YELLOW_0:def_15;
hence corestr g = g by RELAT_1:94; ::_thesis: verum
end;
Lm3: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g is onto
proof
let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds corestr g is onto
let g be Function of L1,L2; ::_thesis: corestr g is onto
the carrier of (Image g) = rng g by YELLOW_0:def_15
.= rng (corestr g) by Th30 ;
hence corestr g is onto by FUNCT_2:def_3; ::_thesis: verum
end;
registration
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
cluster corestr g -> onto ;
coherence
corestr g is onto by Lm3;
end;
theorem Th31: :: WAYBEL_1:31
for L1, L2 being non empty RelStr
for g being Function of L1,L2 st g is monotone holds
corestr g is monotone
proof
let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 st g is monotone holds
corestr g is monotone
let g be Function of L1,L2; ::_thesis: ( g is monotone implies corestr g is monotone )
assume A1: g is monotone ; ::_thesis: corestr g is monotone
let s1, s2 be Element of L1; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (corestr g) . s1 <= (corestr g) . s2 )
assume s1 <= s2 ; ::_thesis: (corestr g) . s1 <= (corestr g) . s2
then A2: g . s1 <= g . s2 by A1, Def2;
reconsider s19 = g . s1, s29 = g . s2 as Element of L2 ;
( s19 = (corestr g) . s1 & s29 = (corestr g) . s2 ) by Th30;
hence (corestr g) . s1 <= (corestr g) . s2 by A2, YELLOW_0:60; ::_thesis: verum
end;
definition
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
func inclusion g -> Function of (Image g),L2 equals :: WAYBEL_1:def 17
id (Image g);
coherence
id (Image g) is Function of (Image g),L2
proof
A1: rng (id (Image g)) = the carrier of (Image g) by RELAT_1:45
.= rng g by YELLOW_0:def_15 ;
dom (id (Image g)) = the carrier of (Image g) by RELAT_1:45;
hence id (Image g) is Function of (Image g),L2 by A1, RELSET_1:4; ::_thesis: verum
end;
end;
:: deftheorem defines inclusion WAYBEL_1:def_17_:_
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g = id (Image g);
Lm4: for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g is monotone
proof
let L1, L2 be non empty RelStr ; ::_thesis: for g being Function of L1,L2 holds inclusion g is monotone
let g be Function of L1,L2; ::_thesis: inclusion g is monotone
let s1, s2 be Element of (Image g); :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (inclusion g) . s1 <= (inclusion g) . s2 )
assume s1 <= s2 ; ::_thesis: (inclusion g) . s1 <= (inclusion g) . s2
then (id (Image g)) . s1 <= s2 by FUNCT_1:18;
then (id (Image g)) . s1 <= (id (Image g)) . s2 by FUNCT_1:18;
hence (inclusion g) . s1 <= (inclusion g) . s2 by YELLOW_0:59; ::_thesis: verum
end;
registration
let L1, L2 be non empty RelStr ;
let g be Function of L1,L2;
cluster inclusion g -> V13() monotone ;
coherence
( inclusion g is one-to-one & inclusion g is monotone ) by Lm4;
end;
theorem Th32: :: WAYBEL_1:32
for L being non empty RelStr
for f being Function of L,L holds (inclusion f) * (corestr f) = f
proof
let L be non empty RelStr ; ::_thesis: for f being Function of L,L holds (inclusion f) * (corestr f) = f
let f be Function of L,L; ::_thesis: (inclusion f) * (corestr f) = f
thus (inclusion f) * (corestr f) = (id the carrier of (Image f)) * f by Th30
.= (id (rng f)) * f by YELLOW_0:def_15
.= f by RELAT_1:54 ; ::_thesis: verum
end;
theorem Th33: :: WAYBEL_1:33
for L being non empty Poset
for f being Function of L,L st f is idempotent holds
(corestr f) * (inclusion f) = id (Image f)
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is idempotent holds
(corestr f) * (inclusion f) = id (Image f)
let f be Function of L,L; ::_thesis: ( f is idempotent implies (corestr f) * (inclusion f) = id (Image f) )
assume A1: f is idempotent ; ::_thesis: (corestr f) * (inclusion f) = id (Image f)
for s being Element of (Image f) holds ((corestr f) * (inclusion f)) . s = s
proof
let s be Element of (Image f); ::_thesis: ((corestr f) * (inclusion f)) . s = s
the carrier of (Image f) = rng (corestr f) by FUNCT_2:def_3;
then consider l being set such that
A2: l in the carrier of L and
A3: (corestr f) . l = s by FUNCT_2:11;
reconsider l = l as Element of L by A2;
A4: (corestr f) . l = f . l by Th30;
thus ((corestr f) * (inclusion f)) . s = (corestr f) . ((inclusion f) . s) by FUNCT_2:15
.= (corestr f) . s by FUNCT_1:18
.= f . (f . l) by A3, A4, Th30
.= s by A1, A3, A4, YELLOW_2:18 ; ::_thesis: verum
end;
hence (corestr f) * (inclusion f) = id (Image f) by FUNCT_2:124; ::_thesis: verum
end;
theorem :: WAYBEL_1:34
for L being non empty Poset
for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is projection holds
ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
let f be Function of L,L; ::_thesis: ( f is projection implies ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i ) )
reconsider T = Image f as non empty Poset ;
reconsider q = corestr f as Function of L,T ;
reconsider i = inclusion f as Function of T,L ;
assume f is projection ; ::_thesis: ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
then A1: ( f is monotone & f is idempotent ) by Def13;
take T ; ::_thesis: ex q being Function of L,T ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
take q ; ::_thesis: ex i being Function of T,L st
( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
take i ; ::_thesis: ( q is monotone & q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
thus q is monotone by A1, Th31; ::_thesis: ( q is onto & i is monotone & i is V13() & f = i * q & id T = q * i )
thus q is onto ; ::_thesis: ( i is monotone & i is V13() & f = i * q & id T = q * i )
thus ( i is monotone & i is V13() ) ; ::_thesis: ( f = i * q & id T = q * i )
thus f = i * q by Th32; ::_thesis: id T = q * i
thus id T = q * i by A1, Th33; ::_thesis: verum
end;
theorem :: WAYBEL_1:35
for L being non empty Poset
for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) holds
f is projection
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) holds
f is projection
let f be Function of L,L; ::_thesis: ( ex T being non empty Poset ex q being Function of L,T ex i being Function of T,L st
( q is monotone & i is monotone & f = i * q & id T = q * i ) implies f is projection )
given T being non empty Poset, q being Function of L,T, i being Function of T,L such that A1: ( q is monotone & i is monotone ) and
A2: f = i * q and
A3: id T = q * i ; ::_thesis: f is projection
(i * q) * i = i * (id the carrier of T) by A3, RELAT_1:36
.= i by FUNCT_2:17 ;
hence f is idempotent by A2, Th21; :: according to WAYBEL_1:def_13 ::_thesis: f is monotone
thus f is monotone by A1, A2, YELLOW_2:12; ::_thesis: verum
end;
theorem Th36: :: WAYBEL_1:36
for L being non empty Poset
for f being Function of L,L st f is closure holds
[(inclusion f),(corestr f)] is Galois
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is closure holds
[(inclusion f),(corestr f)] is Galois
let f be Function of L,L; ::_thesis: ( f is closure implies [(inclusion f),(corestr f)] is Galois )
assume that
A1: ( f is idempotent & f is monotone ) and
A2: id L <= f ; :: according to WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: [(inclusion f),(corestr f)] is Galois
set g = corestr f;
set d = inclusion f;
(corestr f) * (inclusion f) = id (Image f) by A1, Th33;
then A3: (corestr f) * (inclusion f) <= id (Image f) by Lm1;
( corestr f is monotone & id L <= (inclusion f) * (corestr f) ) by A1, A2, Th31, Th32;
hence [(inclusion f),(corestr f)] is Galois by A3, Th19; ::_thesis: verum
end;
theorem :: WAYBEL_1:37
for L being non empty Poset
for f being Function of L,L st f is closure holds
ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is closure holds
ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
let f be Function of L,L; ::_thesis: ( f is closure implies ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) )
assume A1: f is closure ; ::_thesis: ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
reconsider S = Image f as non empty Poset ;
reconsider g = inclusion f as Function of S,L ;
reconsider d = corestr f as Function of L,S ;
take S ; ::_thesis: ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
take g ; ::_thesis: ex d being Function of L,S st
( [g,d] is Galois & f = g * d )
take d ; ::_thesis: ( [g,d] is Galois & f = g * d )
thus [g,d] is Galois by A1, Th36; ::_thesis: f = g * d
thus f = g * d by Th32; ::_thesis: verum
end;
theorem Th38: :: WAYBEL_1:38
for L being non empty Poset
for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) holds
f is closure
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) holds
f is closure
let f be Function of L,L; ::_thesis: ( f is monotone & ex S being non empty Poset ex g being Function of S,L ex d being Function of L,S st
( [g,d] is Galois & f = g * d ) implies f is closure )
assume A1: f is monotone ; ::_thesis: ( for S being non empty Poset
for g being Function of S,L
for d being Function of L,S holds
( not [g,d] is Galois or not f = g * d ) or f is closure )
given S being non empty Poset, g being Function of S,L, d being Function of L,S such that A2: [g,d] is Galois and
A3: f = g * d ; ::_thesis: f is closure
A4: ( d is monotone & g is monotone ) by A2, Th8;
( d * g <= id S & id L <= g * d ) by A2, Th18;
then g = (g * d) * g by A4, Th20;
hence ( f is idempotent & f is monotone ) by A1, A3, Th21; :: according to WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: id L <= f
thus id L <= f by A2, A3, Th18; ::_thesis: verum
end;
theorem Th39: :: WAYBEL_1:39
for L being non empty Poset
for f being Function of L,L st f is kernel holds
[(corestr f),(inclusion f)] is Galois
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is kernel holds
[(corestr f),(inclusion f)] is Galois
let f be Function of L,L; ::_thesis: ( f is kernel implies [(corestr f),(inclusion f)] is Galois )
assume that
A1: ( f is idempotent & f is monotone ) and
A2: f <= id L ; :: according to WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: [(corestr f),(inclusion f)] is Galois
set g = corestr f;
set d = inclusion f;
(corestr f) * (inclusion f) = id (Image f) by A1, Th33;
then A3: id (Image f) <= (corestr f) * (inclusion f) by Lm1;
( corestr f is monotone & (inclusion f) * (corestr f) <= id L ) by A1, A2, Th31, Th32;
hence [(corestr f),(inclusion f)] is Galois by A3, Th19; ::_thesis: verum
end;
theorem :: WAYBEL_1:40
for L being non empty Poset
for f being Function of L,L st f is kernel holds
ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is kernel holds
ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
let f be Function of L,L; ::_thesis: ( f is kernel implies ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) )
assume A1: f is kernel ; ::_thesis: ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
reconsider T = Image f as non empty Poset ;
reconsider g = corestr f as Function of L,T ;
reconsider d = inclusion f as Function of T,L ;
take T ; ::_thesis: ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
take g ; ::_thesis: ex d being Function of T,L st
( [g,d] is Galois & f = d * g )
take d ; ::_thesis: ( [g,d] is Galois & f = d * g )
thus [g,d] is Galois by A1, Th39; ::_thesis: f = d * g
thus f = d * g by Th32; ::_thesis: verum
end;
theorem :: WAYBEL_1:41
for L being non empty Poset
for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) holds
f is kernel
proof
let L be non empty Poset; ::_thesis: for f being Function of L,L st f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) holds
f is kernel
let f be Function of L,L; ::_thesis: ( f is monotone & ex T being non empty Poset ex g being Function of L,T ex d being Function of T,L st
( [g,d] is Galois & f = d * g ) implies f is kernel )
assume A1: f is monotone ; ::_thesis: ( for T being non empty Poset
for g being Function of L,T
for d being Function of T,L holds
( not [g,d] is Galois or not f = d * g ) or f is kernel )
given T being non empty Poset, g being Function of L,T, d being Function of T,L such that A2: [g,d] is Galois and
A3: f = d * g ; ::_thesis: f is kernel
A4: ( d is monotone & g is monotone ) by A2, Th8;
( d * g <= id L & id T <= g * d ) by A2, Th18;
then d = (d * g) * d by A4, Th20;
hence ( f is idempotent & f is monotone ) by A1, A3, Th21; :: according to WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: f <= id L
thus f <= id L by A2, A3, Th18; ::_thesis: verum
end;
theorem Th42: :: WAYBEL_1:42
for L being non empty Poset
for p being Function of L,L st p is projection holds
rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
let p be Function of L,L; ::_thesis: ( p is projection implies rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } )
assume that
A1: p is idempotent and
p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
set Lk = { k where k is Element of L : p . k <= k } ;
set Lc = { c where c is Element of L : c <= p . c } ;
thus rng p c= { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } :: according to XBOOLE_0:def_10 ::_thesis: { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } c= rng p
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng p or x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } )
assume A2: x in rng p ; ::_thesis: x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k }
then reconsider x9 = x as Element of L ;
A3: ex l being set st
( l in dom p & p . l = x ) by A2, FUNCT_1:def_3;
then p . x9 <= x9 by A1, YELLOW_2:18;
then A4: x in { k where k is Element of L : p . k <= k } ;
x9 <= p . x9 by A1, A3, YELLOW_2:18;
then x in { c where c is Element of L : c <= p . c } ;
hence x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } or x in rng p )
assume A5: x in { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } ; ::_thesis: x in rng p
then x in { c where c is Element of L : c <= p . c } by XBOOLE_0:def_4;
then A6: ex lc being Element of L st
( x = lc & lc <= p . lc ) ;
x in { k where k is Element of L : p . k <= k } by A5, XBOOLE_0:def_4;
then ex lk being Element of L st
( x = lk & p . lk <= lk ) ;
then ( dom p = the carrier of L & x = p . x ) by A6, FUNCT_2:def_1, ORDERS_2:2;
hence x in rng p by A6, FUNCT_1:def_3; ::_thesis: verum
end;
theorem Th43: :: WAYBEL_1:43
for L being non empty Poset
for p being Function of L,L st p is projection holds
( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )
let p be Function of L,L; ::_thesis: ( p is projection implies ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L ) )
assume A1: p is projection ; ::_thesis: ( { c where c is Element of L : c <= p . c } is non empty Subset of L & { k where k is Element of L : p . k <= k } is non empty Subset of L )
defpred S1[ Element of L] means p . $1 <= $1;
defpred S2[ Element of L] means $1 <= p . $1;
set Lc = { c where c is Element of L : S2[c] } ;
set Lk = { k where k is Element of L : S1[k] } ;
A2: rng p = { c where c is Element of L : S2[c] } /\ { k where k is Element of L : S1[k] } by A1, Th42;
{ c where c is Element of L : S2[c] } is Subset of L from DOMAIN_1:sch_7();
hence { c where c is Element of L : S2[c] } is non empty Subset of L by A2; ::_thesis: { k where k is Element of L : p . k <= k } is non empty Subset of L
{ k where k is Element of L : S1[k] } is Subset of L from DOMAIN_1:sch_7();
hence { k where k is Element of L : p . k <= k } is non empty Subset of L by A2; ::_thesis: verum
end;
theorem Th44: :: WAYBEL_1:44
for L being non empty Poset
for p being Function of L,L st p is projection holds
( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )
let p be Function of L,L; ::_thesis: ( p is projection implies ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p ) )
assume A1: p is projection ; ::_thesis: ( rng (p | { c where c is Element of L : c <= p . c } ) = rng p & rng (p | { k where k is Element of L : p . k <= k } ) = rng p )
set Lk = { k where k is Element of L : p . k <= k } ;
set Lc = { c where c is Element of L : c <= p . c } ;
A2: rng p = { c where c is Element of L : c <= p . c } /\ { k where k is Element of L : p . k <= k } by A1, Th42;
A3: dom p = the carrier of L by FUNCT_2:def_1;
thus rng (p | { c where c is Element of L : c <= p . c } ) = rng p ::_thesis: rng (p | { k where k is Element of L : p . k <= k } ) = rng p
proof
thus rng (p | { c where c is Element of L : c <= p . c } ) c= rng p by RELAT_1:70; :: according to XBOOLE_0:def_10 ::_thesis: rng p c= rng (p | { c where c is Element of L : c <= p . c } )
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in rng (p | { c where c is Element of L : c <= p . c } ) )
assume A4: y in rng p ; ::_thesis: y in rng (p | { c where c is Element of L : c <= p . c } )
then A5: y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def_4;
then A6: ex lc being Element of L st
( y = lc & lc <= p . lc ) ;
y in { k where k is Element of L : p . k <= k } by A2, A4, XBOOLE_0:def_4;
then ex lk being Element of L st
( y = lk & p . lk <= lk ) ;
then y = p . y by A6, ORDERS_2:2;
hence y in rng (p | { c where c is Element of L : c <= p . c } ) by A3, A5, A6, FUNCT_1:50; ::_thesis: verum
end;
thus rng (p | { k where k is Element of L : p . k <= k } ) c= rng p by RELAT_1:70; :: according to XBOOLE_0:def_10 ::_thesis: rng p c= rng (p | { k where k is Element of L : p . k <= k } )
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in rng (p | { k where k is Element of L : p . k <= k } ) )
assume A7: y in rng p ; ::_thesis: y in rng (p | { k where k is Element of L : p . k <= k } )
then y in { c where c is Element of L : c <= p . c } by A2, XBOOLE_0:def_4;
then A8: ex lc being Element of L st
( y = lc & lc <= p . lc ) ;
A9: y in { k where k is Element of L : p . k <= k } by A2, A7, XBOOLE_0:def_4;
then ex lk being Element of L st
( y = lk & p . lk <= lk ) ;
then y = p . y by A8, ORDERS_2:2;
hence y in rng (p | { k where k is Element of L : p . k <= k } ) by A3, A9, A8, FUNCT_1:50; ::_thesis: verum
end;
theorem Th45: :: WAYBEL_1:45
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
let p be Function of L,L; ::_thesis: ( p is projection implies for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc) )
assume A1: p is projection ; ::_thesis: for Lc, Lk being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
let Lc, Lk be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies p | Lc is Function of (subrelstr Lc),(subrelstr Lc) )
assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: p | Lc is Function of (subrelstr Lc),(subrelstr Lc)
set Lk = { k where k is Element of L : p . k <= k } ;
rng p = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th42;
then rng (p | Lc) = Lc /\ { k where k is Element of L : p . k <= k } by A1, A2, Th44;
then A3: rng (p | Lc) c= Lc by XBOOLE_1:17;
( Lc = the carrier of (subrelstr Lc) & p | Lc is Function of Lc, the carrier of L ) by FUNCT_2:32, YELLOW_0:def_15;
hence p | Lc is Function of (subrelstr Lc),(subrelstr Lc) by A3, FUNCT_2:6; ::_thesis: verum
end;
theorem :: WAYBEL_1:46
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk) )
assume A1: p is projection ; ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
set Lc = { c where c is Element of L : c <= p . c } ;
let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies p | Lk is Function of (subrelstr Lk),(subrelstr Lk) )
assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: p | Lk is Function of (subrelstr Lk),(subrelstr Lk)
rng p = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th42;
then rng (p | Lk) = { c where c is Element of L : c <= p . c } /\ Lk by A1, A2, Th44;
then A3: rng (p | Lk) c= Lk by XBOOLE_1:17;
( Lk = the carrier of (subrelstr Lk) & p | Lk is Function of Lk, the carrier of L ) by FUNCT_2:32, YELLOW_0:def_15;
hence p | Lk is Function of (subrelstr Lk),(subrelstr Lk) by A3, FUNCT_2:6; ::_thesis: verum
end;
theorem Th47: :: WAYBEL_1:47
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let p be Function of L,L; ::_thesis: ( p is projection implies for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure )
assume that
A1: p is idempotent and
A2: p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let Lc be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure )
assume A3: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: for pc being Function of (subrelstr Lc),(subrelstr Lc) st pc = p | Lc holds
pc is closure
let pc be Function of (subrelstr Lc),(subrelstr Lc); ::_thesis: ( pc = p | Lc implies pc is closure )
assume A4: pc = p | Lc ; ::_thesis: pc is closure
A5: dom pc = the carrier of (subrelstr Lc) by FUNCT_2:def_1;
hereby :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_14 ::_thesis: id (subrelstr Lc) <= pc
now__::_thesis:_for_x_being_Element_of_(subrelstr_Lc)_holds_(pc_*_pc)_._x_=_pc_._x
let x be Element of (subrelstr Lc); ::_thesis: (pc * pc) . x = pc . x
A6: x is Element of L by YELLOW_0:58;
A7: pc . x = p . x by A4, A5, FUNCT_1:47;
then p . (p . x) = pc . (pc . x) by A4, A5, FUNCT_1:47
.= (pc * pc) . x by A5, FUNCT_1:13 ;
hence (pc * pc) . x = pc . x by A1, A7, A6, YELLOW_2:18; ::_thesis: verum
end;
hence pc * pc = pc by FUNCT_2:63; ::_thesis: pc is monotone
thus pc is monotone ::_thesis: verum
proof
let x1, x2 be Element of (subrelstr Lc); :: according to WAYBEL_1:def_2 ::_thesis: ( x1 <= x2 implies pc . x1 <= pc . x2 )
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2 ; ::_thesis: pc . x1 <= pc . x2
then x19 <= x29 by YELLOW_0:59;
then A8: p . x19 <= p . x29 by A2, Def2;
( pc . x1 = p . x19 & pc . x2 = p . x29 ) by A4, A5, FUNCT_1:47;
hence pc . x1 <= pc . x2 by A8, YELLOW_0:60; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_Element_of_(subrelstr_Lc)_holds_(id_(subrelstr_Lc))_._x_<=_pc_._x
let x be Element of (subrelstr Lc); ::_thesis: (id (subrelstr Lc)) . x <= pc . x
reconsider x9 = x as Element of L by YELLOW_0:58;
x in the carrier of (subrelstr Lc) ;
then x in Lc by YELLOW_0:def_15;
then A9: ex c being Element of L st
( x = c & c <= p . c ) by A3;
pc . x = p . x9 by A4, A5, FUNCT_1:47;
then x <= pc . x by A9, YELLOW_0:60;
hence (id (subrelstr Lc)) . x <= pc . x by FUNCT_1:18; ::_thesis: verum
end;
hence id (subrelstr Lc) <= pc by YELLOW_2:9; ::_thesis: verum
end;
theorem :: WAYBEL_1:48
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume that
A1: p is idempotent and
A2: p is monotone ; :: according to WAYBEL_1:def_13 ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel )
assume A3: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: for pk being Function of (subrelstr Lk),(subrelstr Lk) st pk = p | Lk holds
pk is kernel
let pk be Function of (subrelstr Lk),(subrelstr Lk); ::_thesis: ( pk = p | Lk implies pk is kernel )
assume A4: pk = p | Lk ; ::_thesis: pk is kernel
A5: dom pk = the carrier of (subrelstr Lk) by FUNCT_2:def_1;
hereby :: according to QUANTAL1:def_9,WAYBEL_1:def_13,WAYBEL_1:def_15 ::_thesis: pk <= id (subrelstr Lk)
now__::_thesis:_for_x_being_Element_of_(subrelstr_Lk)_holds_(pk_*_pk)_._x_=_pk_._x
let x be Element of (subrelstr Lk); ::_thesis: (pk * pk) . x = pk . x
A6: x is Element of L by YELLOW_0:58;
A7: pk . x = p . x by A4, A5, FUNCT_1:47;
then p . (p . x) = pk . (pk . x) by A4, A5, FUNCT_1:47
.= (pk * pk) . x by A5, FUNCT_1:13 ;
hence (pk * pk) . x = pk . x by A1, A7, A6, YELLOW_2:18; ::_thesis: verum
end;
hence pk * pk = pk by FUNCT_2:63; ::_thesis: pk is monotone
thus pk is monotone ::_thesis: verum
proof
let x1, x2 be Element of (subrelstr Lk); :: according to WAYBEL_1:def_2 ::_thesis: ( x1 <= x2 implies pk . x1 <= pk . x2 )
reconsider x19 = x1, x29 = x2 as Element of L by YELLOW_0:58;
assume x1 <= x2 ; ::_thesis: pk . x1 <= pk . x2
then x19 <= x29 by YELLOW_0:59;
then A8: p . x19 <= p . x29 by A2, Def2;
( pk . x1 = p . x19 & pk . x2 = p . x29 ) by A4, A5, FUNCT_1:47;
hence pk . x1 <= pk . x2 by A8, YELLOW_0:60; ::_thesis: verum
end;
end;
now__::_thesis:_for_x_being_Element_of_(subrelstr_Lk)_holds_pk_._x_<=_(id_(subrelstr_Lk))_._x
let x be Element of (subrelstr Lk); ::_thesis: pk . x <= (id (subrelstr Lk)) . x
reconsider x9 = x as Element of L by YELLOW_0:58;
x in the carrier of (subrelstr Lk) ;
then x in Lk by YELLOW_0:def_15;
then A9: ex c being Element of L st
( x = c & p . c <= c ) by A3;
pk . x = p . x9 by A4, A5, FUNCT_1:47;
then pk . x <= x by A9, YELLOW_0:60;
hence pk . x <= (id (subrelstr Lk)) . x by FUNCT_1:18; ::_thesis: verum
end;
hence pk <= id (subrelstr Lk) by YELLOW_2:9; ::_thesis: verum
end;
theorem Th49: :: WAYBEL_1:49
for L being non empty Poset
for p being Function of L,L st p is monotone holds
for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is monotone holds
for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting
let p be Function of L,L; ::_thesis: ( p is monotone implies for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting )
assume A1: p is monotone ; ::_thesis: for Lc being Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
subrelstr Lc is sups-inheriting
let Lc be Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies subrelstr Lc is sups-inheriting )
assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: subrelstr Lc is sups-inheriting
let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lc) )
assume A3: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lc)
p . ("\/" (X,L)) is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= p . ("\/" (X,L)) )
assume A4: x in X ; ::_thesis: x <= p . ("\/" (X,L))
then x in the carrier of (subrelstr Lc) ;
then x in Lc by YELLOW_0:def_15;
then A5: ex l being Element of L st
( x = l & l <= p . l ) by A2;
"\/" (X,L) is_>=_than X by A3, YELLOW_0:30;
then x <= "\/" (X,L) by A4, LATTICE3:def_9;
then p . x <= p . ("\/" (X,L)) by A1, Def2;
hence x <= p . ("\/" (X,L)) by A5, ORDERS_2:3; ::_thesis: verum
end;
then "\/" (X,L) <= p . ("\/" (X,L)) by A3, YELLOW_0:30;
then "\/" (X,L) in Lc by A2;
hence "\/" (X,L) in the carrier of (subrelstr Lc) by YELLOW_0:def_15; ::_thesis: verum
end;
theorem Th50: :: WAYBEL_1:50
for L being non empty Poset
for p being Function of L,L st p is monotone holds
for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
subrelstr Lk is infs-inheriting
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is monotone holds
for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
subrelstr Lk is infs-inheriting
let p be Function of L,L; ::_thesis: ( p is monotone implies for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
subrelstr Lk is infs-inheriting )
assume A1: p is monotone ; ::_thesis: for Lk being Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
subrelstr Lk is infs-inheriting
let Lk be Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies subrelstr Lk is infs-inheriting )
assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: subrelstr Lk is infs-inheriting
let X be Subset of (subrelstr Lk); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lk) )
assume A3: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lk)
p . ("/\" (X,L)) is_<=_than X
proof
let x be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not x in X or p . ("/\" (X,L)) <= x )
assume A4: x in X ; ::_thesis: p . ("/\" (X,L)) <= x
then x in the carrier of (subrelstr Lk) ;
then x in Lk by YELLOW_0:def_15;
then A5: ex l being Element of L st
( x = l & l >= p . l ) by A2;
"/\" (X,L) is_<=_than X by A3, YELLOW_0:31;
then x >= "/\" (X,L) by A4, LATTICE3:def_8;
then p . x >= p . ("/\" (X,L)) by A1, Def2;
hence p . ("/\" (X,L)) <= x by A5, ORDERS_2:3; ::_thesis: verum
end;
then "/\" (X,L) >= p . ("/\" (X,L)) by A3, YELLOW_0:31;
then "/\" (X,L) in Lk by A2;
hence "/\" (X,L) in the carrier of (subrelstr Lk) by YELLOW_0:def_15; ::_thesis: verum
end;
theorem :: WAYBEL_1:51
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )
let p be Function of L,L; ::_thesis: ( p is projection implies for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) )
assume A1: p is projection ; ::_thesis: for Lc being non empty Subset of L st Lc = { c where c is Element of L : c <= p . c } holds
( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )
then reconsider Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th43;
let Lc be non empty Subset of L; ::_thesis: ( Lc = { c where c is Element of L : c <= p . c } implies ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) ) )
assume A2: Lc = { c where c is Element of L : c <= p . c } ; ::_thesis: ( ( p is infs-preserving implies ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting ) ) & ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) ) )
A3: p is monotone by A1, Def13;
then A4: subrelstr Lk is infs-inheriting by Th50;
A5: Lc = the carrier of (subrelstr Lc) by YELLOW_0:def_15;
A6: the carrier of (Image p) = rng p by YELLOW_0:def_15
.= Lc /\ Lk by A1, A2, Th42 ;
then A7: the carrier of (Image p) c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def_15;
A9: the carrier of (Image p) c= Lc by A6, XBOOLE_1:17;
hereby ::_thesis: ( p is filtered-infs-preserving implies ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting ) )
assume A10: p is infs-preserving ; ::_thesis: ( subrelstr Lc is infs-inheriting & Image p is infs-inheriting )
thus A11: subrelstr Lc is infs-inheriting ::_thesis: Image p is infs-inheriting
proof
let X be Subset of (subrelstr Lc); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) )
the carrier of (subrelstr Lc) is Subset of L by YELLOW_0:def_15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume A12: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lc)
A13: inf X9 is_<=_than p .: X9
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in p .: X9 or inf X9 <= y )
assume y in p .: X9 ; ::_thesis: inf X9 <= y
then consider x being Element of L such that
A14: x in X9 and
A15: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lc by A5, A14;
then A16: ex x9 being Element of L st
( x9 = x & x9 <= p . x9 ) by A2;
inf X9 is_<=_than X9 by A12, YELLOW_0:31;
then inf X9 <= x by A14, LATTICE3:def_8;
hence inf X9 <= y by A15, A16, ORDERS_2:3; ::_thesis: verum
end;
p preserves_inf_of X9 by A10, WAYBEL_0:def_32;
then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A12, WAYBEL_0:def_30;
then inf X9 <= p . (inf X9) by A13, YELLOW_0:31;
hence "/\" (X,L) in the carrier of (subrelstr Lc) by A2, A5; ::_thesis: verum
end;
thus Image p is infs-inheriting ::_thesis: verum
proof
let X be Subset of (Image p); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) )
assume A17: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p)
X c= Lc by A9, XBOOLE_1:1;
then A18: "/\" (X,L) in the carrier of (subrelstr Lc) by A5, A11, A17, YELLOW_0:def_18;
( subrelstr Lk is infs-inheriting & X c= the carrier of (subrelstr Lk) ) by A3, A7, A8, Th50, XBOOLE_1:1;
then "/\" (X,L) in the carrier of (subrelstr Lk) by A17, YELLOW_0:def_18;
hence "/\" (X,L) in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A19: p is filtered-infs-preserving ; ::_thesis: ( subrelstr Lc is filtered-infs-inheriting & Image p is filtered-infs-inheriting )
thus A20: subrelstr Lc is filtered-infs-inheriting ::_thesis: Image p is filtered-infs-inheriting
proof
let X be filtered Subset of (subrelstr Lc); :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) )
assume X <> {} ; ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (subrelstr Lc) )
then reconsider X9 = X as non empty filtered Subset of L by YELLOW_2:7;
assume A21: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (subrelstr Lc)
A22: inf X9 is_<=_than p .: X9
proof
let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in p .: X9 or inf X9 <= y )
assume y in p .: X9 ; ::_thesis: inf X9 <= y
then consider x being Element of L such that
A23: x in X9 and
A24: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lc by A5, A23;
then A25: ex x9 being Element of L st
( x9 = x & x9 <= p . x9 ) by A2;
inf X9 is_<=_than X9 by A21, YELLOW_0:31;
then inf X9 <= x by A23, LATTICE3:def_8;
hence inf X9 <= y by A24, A25, ORDERS_2:3; ::_thesis: verum
end;
p preserves_inf_of X9 by A19, WAYBEL_0:def_36;
then ( ex_inf_of p .: X,L & inf (p .: X9) = p . (inf X9) ) by A21, WAYBEL_0:def_30;
then inf X9 <= p . (inf X9) by A22, YELLOW_0:31;
hence "/\" (X,L) in the carrier of (subrelstr Lc) by A2, A5; ::_thesis: verum
end;
let X be filtered Subset of (Image p); :: according to WAYBEL_0:def_3 ::_thesis: ( X = {} or not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) )
assume that
A26: X <> {} and
A27: ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p)
the carrier of (Image p) c= the carrier of (subrelstr Lc) by A9, YELLOW_0:def_15;
then X is filtered Subset of (subrelstr Lc) by YELLOW_2:8;
then A28: "/\" (X,L) in the carrier of (subrelstr Lc) by A20, A26, A27, WAYBEL_0:def_3;
X c= the carrier of (subrelstr Lk) by A7, A8, XBOOLE_1:1;
then "/\" (X,L) in the carrier of (subrelstr Lk) by A27, A4, YELLOW_0:def_18;
hence "/\" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: WAYBEL_1:52
for L being non empty Poset
for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L st p is projection holds
for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )
let p be Function of L,L; ::_thesis: ( p is projection implies for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) )
assume A1: p is projection ; ::_thesis: for Lk being non empty Subset of L st Lk = { k where k is Element of L : p . k <= k } holds
( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )
then reconsider Lc = { c where c is Element of L : c <= p . c } as non empty Subset of L by Th43;
let Lk be non empty Subset of L; ::_thesis: ( Lk = { k where k is Element of L : p . k <= k } implies ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) ) )
assume A2: Lk = { k where k is Element of L : p . k <= k } ; ::_thesis: ( ( p is sups-preserving implies ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting ) ) & ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) ) )
A3: p is monotone by A1, Def13;
then A4: subrelstr Lc is sups-inheriting by Th49;
A5: Lc = the carrier of (subrelstr Lc) by YELLOW_0:def_15;
A6: the carrier of (Image p) = rng p by YELLOW_0:def_15
.= Lc /\ Lk by A1, A2, Th42 ;
then A7: the carrier of (Image p) c= Lk by XBOOLE_1:17;
A8: Lk = the carrier of (subrelstr Lk) by YELLOW_0:def_15;
A9: the carrier of (Image p) c= Lc by A6, XBOOLE_1:17;
hereby ::_thesis: ( p is directed-sups-preserving implies ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting ) )
assume A10: p is sups-preserving ; ::_thesis: ( subrelstr Lk is sups-inheriting & Image p is sups-inheriting )
thus A11: subrelstr Lk is sups-inheriting ::_thesis: Image p is sups-inheriting
proof
let X be Subset of (subrelstr Lk); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) )
the carrier of (subrelstr Lk) is Subset of L by YELLOW_0:def_15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume A12: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lk)
A13: sup X9 is_>=_than p .: X9
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in p .: X9 or y <= sup X9 )
assume y in p .: X9 ; ::_thesis: y <= sup X9
then consider x being Element of L such that
A14: x in X9 and
A15: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lk by A8, A14;
then A16: ex x9 being Element of L st
( x9 = x & x9 >= p . x9 ) by A2;
sup X9 is_>=_than X9 by A12, YELLOW_0:30;
then sup X9 >= x by A14, LATTICE3:def_9;
hence y <= sup X9 by A15, A16, ORDERS_2:3; ::_thesis: verum
end;
p preserves_sup_of X9 by A10, WAYBEL_0:def_33;
then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A12, WAYBEL_0:def_31;
then sup X9 >= p . (sup X9) by A13, YELLOW_0:30;
hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; ::_thesis: verum
end;
thus Image p is sups-inheriting ::_thesis: verum
proof
let X be Subset of (Image p); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) )
assume A17: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p)
X c= Lk by A7, XBOOLE_1:1;
then A18: "\/" (X,L) in the carrier of (subrelstr Lk) by A8, A11, A17, YELLOW_0:def_19;
( subrelstr Lc is sups-inheriting & X c= the carrier of (subrelstr Lc) ) by A3, A9, A5, Th49, XBOOLE_1:1;
then "\/" (X,L) in the carrier of (subrelstr Lc) by A17, YELLOW_0:def_19;
hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A18, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
assume A19: p is directed-sups-preserving ; ::_thesis: ( subrelstr Lk is directed-sups-inheriting & Image p is directed-sups-inheriting )
thus A20: subrelstr Lk is directed-sups-inheriting ::_thesis: Image p is directed-sups-inheriting
proof
let X be directed Subset of (subrelstr Lk); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) )
assume X <> {} ; ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (subrelstr Lk) )
then reconsider X9 = X as non empty directed Subset of L by YELLOW_2:7;
assume A21: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (subrelstr Lk)
A22: sup X9 is_>=_than p .: X9
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in p .: X9 or y <= sup X9 )
assume y in p .: X9 ; ::_thesis: y <= sup X9
then consider x being Element of L such that
A23: x in X9 and
A24: y = p . x by FUNCT_2:65;
reconsider x = x as Element of L ;
x in Lk by A8, A23;
then A25: ex x9 being Element of L st
( x9 = x & x9 >= p . x9 ) by A2;
sup X9 is_>=_than X9 by A21, YELLOW_0:30;
then sup X9 >= x by A23, LATTICE3:def_9;
hence y <= sup X9 by A24, A25, ORDERS_2:3; ::_thesis: verum
end;
p preserves_sup_of X9 by A19, WAYBEL_0:def_37;
then ( ex_sup_of p .: X,L & sup (p .: X9) = p . (sup X9) ) by A21, WAYBEL_0:def_31;
then sup X9 >= p . (sup X9) by A22, YELLOW_0:30;
hence "\/" (X,L) in the carrier of (subrelstr Lk) by A2, A8; ::_thesis: verum
end;
let X be directed Subset of (Image p); :: according to WAYBEL_0:def_4 ::_thesis: ( X = {} or not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) )
assume that
A26: X <> {} and
A27: ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p)
the carrier of (Image p) c= the carrier of (subrelstr Lk) by A7, YELLOW_0:def_15;
then X is directed Subset of (subrelstr Lk) by YELLOW_2:8;
then A28: "\/" (X,L) in the carrier of (subrelstr Lk) by A20, A26, A27, WAYBEL_0:def_4;
X c= the carrier of (subrelstr Lc) by A9, A5, XBOOLE_1:1;
then "\/" (X,L) in the carrier of (subrelstr Lc) by A27, A4, YELLOW_0:def_19;
hence "\/" (X,L) in the carrier of (Image p) by A6, A5, A8, A28, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th53: :: WAYBEL_1:53
for L being non empty Poset
for p being Function of L,L holds
( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
proof
let L be non empty Poset; ::_thesis: for p being Function of L,L holds
( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
let p be Function of L,L; ::_thesis: ( ( p is closure implies Image p is infs-inheriting ) & ( p is kernel implies Image p is sups-inheriting ) )
hereby ::_thesis: ( p is kernel implies Image p is sups-inheriting )
assume A1: p is closure ; ::_thesis: Image p is infs-inheriting
thus Image p is infs-inheriting ::_thesis: verum
proof
let X be Subset of (Image p); :: according to YELLOW_0:def_18 ::_thesis: ( not ex_inf_of X,L or "/\" (X,L) in the carrier of (Image p) )
A2: the carrier of (Image p) = rng p by YELLOW_0:def_15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume ex_inf_of X,L ; ::_thesis: "/\" (X,L) in the carrier of (Image p)
then p . ("/\" (X9,L)) = "/\" (X9,L) by A1, A2, Th28;
hence "/\" (X,L) in the carrier of (Image p) by A2, FUNCT_2:4; ::_thesis: verum
end;
end;
assume A3: p is kernel ; ::_thesis: Image p is sups-inheriting
let X be Subset of (Image p); :: according to YELLOW_0:def_19 ::_thesis: ( not ex_sup_of X,L or "\/" (X,L) in the carrier of (Image p) )
A4: the carrier of (Image p) = rng p by YELLOW_0:def_15;
then reconsider X9 = X as Subset of L by XBOOLE_1:1;
assume ex_sup_of X,L ; ::_thesis: "\/" (X,L) in the carrier of (Image p)
then p . ("\/" (X9,L)) = "\/" (X9,L) by A3, A4, Th29;
hence "\/" (X,L) in the carrier of (Image p) by A4, FUNCT_2:4; ::_thesis: verum
end;
theorem :: WAYBEL_1:54
for L being non empty complete Poset
for p being Function of L,L st p is projection holds
Image p is complete
proof
let L be non empty complete Poset; ::_thesis: for p being Function of L,L st p is projection holds
Image p is complete
let p be Function of L,L; ::_thesis: ( p is projection implies Image p is complete )
A1: the carrier of (Image p) = rng p by YELLOW_0:def_15;
assume A2: p is projection ; ::_thesis: Image p is complete
then reconsider Lc = { c where c is Element of L : c <= p . c } , Lk = { k where k is Element of L : p . k <= k } as non empty Subset of L by Th43;
A3: ( the carrier of (subrelstr Lc) = Lc & rng p = Lc /\ Lk ) by A2, Th42, YELLOW_0:def_15;
p is monotone by A2, Def13;
then subrelstr Lc is sups-inheriting by Th49;
then A4: subrelstr Lc is complete LATTICE by YELLOW_2:31;
reconsider pc = p | Lc as Function of (subrelstr Lc),(subrelstr Lc) by A2, Th45;
A5: Image pc is infs-inheriting by A2, Th47, Th53;
A6: the carrier of (Image pc) = rng pc by YELLOW_0:def_15
.= the carrier of (Image p) by A2, A1, Th44 ;
then the InternalRel of (Image pc) = the InternalRel of (subrelstr Lc) |_2 the carrier of (Image p) by YELLOW_0:def_14
.= ( the InternalRel of L |_2 the carrier of (subrelstr Lc)) |_2 the carrier of (Image p) by YELLOW_0:def_14
.= the InternalRel of L |_2 the carrier of (Image p) by A1, A3, WELLORD1:22, XBOOLE_1:17
.= the InternalRel of (Image p) by YELLOW_0:def_14 ;
hence Image p is complete by A4, A5, A6, YELLOW_2:30; ::_thesis: verum
end;
theorem :: WAYBEL_1:55
for L being non empty Poset
for c being Function of L,L st c is closure holds
( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
proof
let L be non empty Poset; ::_thesis: for c being Function of L,L st c is closure holds
( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
let c be Function of L,L; ::_thesis: ( c is closure implies ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) ) )
A1: corestr c = c by Th30;
assume A2: c is closure ; ::_thesis: ( corestr c is sups-preserving & ( for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) ) )
then A3: c is idempotent by Def13;
[(inclusion c),(corestr c)] is Galois by A2, Th36;
then A4: corestr c is lower_adjoint by Def12;
hence corestr c is sups-preserving ; ::_thesis: for X being Subset of L st X c= the carrier of (Image c) & ex_sup_of X,L holds
( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) )
let X be Subset of L; ::_thesis: ( X c= the carrier of (Image c) & ex_sup_of X,L implies ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) )
assume that
A5: X c= the carrier of (Image c) and
A6: ex_sup_of X,L ; ::_thesis: ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) )
X c= rng c by A5, YELLOW_0:def_15;
then A7: c .: X = X by A3, YELLOW_2:20;
corestr c preserves_sup_of X by A4, WAYBEL_0:def_33;
hence ( ex_sup_of X, Image c & "\/" (X,(Image c)) = c . ("\/" (X,L)) ) by A6, A1, A7, WAYBEL_0:def_31; ::_thesis: verum
end;
theorem :: WAYBEL_1:56
for L being non empty Poset
for k being Function of L,L st k is kernel holds
( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) )
proof
let L be non empty Poset; ::_thesis: for k being Function of L,L st k is kernel holds
( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) )
let k be Function of L,L; ::_thesis: ( k is kernel implies ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) ) )
A1: corestr k = k by Th30;
assume A2: k is kernel ; ::_thesis: ( corestr k is infs-preserving & ( for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) ) )
then A3: k is idempotent by Def13;
[(corestr k),(inclusion k)] is Galois by A2, Th39;
then A4: corestr k is upper_adjoint by Def11;
hence corestr k is infs-preserving ; ::_thesis: for X being Subset of L st X c= the carrier of (Image k) & ex_inf_of X,L holds
( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) )
let X be Subset of L; ::_thesis: ( X c= the carrier of (Image k) & ex_inf_of X,L implies ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) )
assume that
A5: X c= the carrier of (Image k) and
A6: ex_inf_of X,L ; ::_thesis: ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) )
X c= rng k by A5, YELLOW_0:def_15;
then A7: k .: X = X by A3, YELLOW_2:20;
corestr k preserves_inf_of X by A4, WAYBEL_0:def_32;
hence ( ex_inf_of X, Image k & "/\" (X,(Image k)) = k . ("/\" (X,L)) ) by A6, A1, A7, WAYBEL_0:def_30; ::_thesis: verum
end;
begin
theorem Th57: :: WAYBEL_1:57
for L being non empty complete Poset holds
( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving )
proof
let L be non empty complete Poset; ::_thesis: ( [(IdsMap L),(SupMap L)] is Galois & SupMap L is sups-preserving )
set g = IdsMap L;
set d = SupMap L;
now__::_thesis:_for_I_being_Element_of_(InclPoset_(Ids_L))
for_x_being_Element_of_L_holds_
(_(_I_<=_(IdsMap_L)_._x_implies_(SupMap_L)_._I_<=_x_)_&_(_(SupMap_L)_._I_<=_x_implies_I_<=_(IdsMap_L)_._x_)_)
let I be Element of (InclPoset (Ids L)); ::_thesis: for x being Element of L holds
( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) )
let x be Element of L; ::_thesis: ( ( I <= (IdsMap L) . x implies (SupMap L) . I <= x ) & ( (SupMap L) . I <= x implies I <= (IdsMap L) . x ) )
reconsider I9 = I as Ideal of L by YELLOW_2:41;
hereby ::_thesis: ( (SupMap L) . I <= x implies I <= (IdsMap L) . x )
assume I <= (IdsMap L) . x ; ::_thesis: (SupMap L) . I <= x
then I c= (IdsMap L) . x by YELLOW_1:3;
then I9 c= downarrow x by YELLOW_2:def_4;
then x is_>=_than I9 by YELLOW_2:1;
then sup I9 <= x by YELLOW_0:32;
hence (SupMap L) . I <= x by YELLOW_2:def_3; ::_thesis: verum
end;
assume (SupMap L) . I <= x ; ::_thesis: I <= (IdsMap L) . x
then A1: sup I9 <= x by YELLOW_2:def_3;
sup I9 is_>=_than I9 by YELLOW_0:32;
then x is_>=_than I9 by A1, YELLOW_0:4;
then I9 c= downarrow x by YELLOW_2:1;
then I c= (IdsMap L) . x by YELLOW_2:def_4;
hence I <= (IdsMap L) . x by YELLOW_1:3; ::_thesis: verum
end;
hence [(IdsMap L),(SupMap L)] is Galois by Th8; ::_thesis: SupMap L is sups-preserving
then SupMap L is lower_adjoint by Th9;
hence SupMap L is sups-preserving ; ::_thesis: verum
end;
theorem :: WAYBEL_1:58
for L being non empty complete Poset holds
( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )
proof
let L be non empty complete Poset; ::_thesis: ( (IdsMap L) * (SupMap L) is closure & Image ((IdsMap L) * (SupMap L)),L are_isomorphic )
set i = (IdsMap L) * (SupMap L);
A1: now__::_thesis:_for_I_being_Ideal_of_L_holds_((IdsMap_L)_*_(SupMap_L))_._I_=_downarrow_(sup_I)
let I be Ideal of L; ::_thesis: ((IdsMap L) * (SupMap L)) . I = downarrow (sup I)
I is Element of (InclPoset (Ids L)) by YELLOW_2:41;
hence ((IdsMap L) * (SupMap L)) . I = (IdsMap L) . ((SupMap L) . I) by FUNCT_2:15
.= (IdsMap L) . (sup I) by YELLOW_2:def_3
.= downarrow (sup I) by YELLOW_2:def_4 ;
::_thesis: verum
end;
( (IdsMap L) * (SupMap L) is monotone & [(IdsMap L),(SupMap L)] is Galois ) by Th57, YELLOW_2:12;
hence (IdsMap L) * (SupMap L) is closure by Th38; ::_thesis: Image ((IdsMap L) * (SupMap L)),L are_isomorphic
take f = (SupMap L) * (inclusion ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def_8 ::_thesis: f is isomorphic
A2: now__::_thesis:_for_x_being_Element_of_(Image_((IdsMap_L)_*_(SupMap_L)))
for_I_being_Ideal_of_L_st_x_=_I_holds_
f_._I_=_sup_I
let x be Element of (Image ((IdsMap L) * (SupMap L))); ::_thesis: for I being Ideal of L st x = I holds
f . I = sup I
let I be Ideal of L; ::_thesis: ( x = I implies f . I = sup I )
assume A3: x = I ; ::_thesis: f . I = sup I
hence f . I = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . I) by FUNCT_2:15
.= (SupMap L) . I by A3, FUNCT_1:18
.= sup I by YELLOW_2:def_3 ;
::_thesis: verum
end;
A4: f is monotone by YELLOW_2:12;
A5: now__::_thesis:_for_x,_y_being_Element_of_(Image_((IdsMap_L)_*_(SupMap_L)))_holds_
(_(_x_<=_y_implies_f_._x_<=_f_._y_)_&_(_f_._x_<=_f_._y_implies_x_<=_y_)_)
let x, y be Element of (Image ((IdsMap L) * (SupMap L))); ::_thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
consider Ix being Element of (InclPoset (Ids L)) such that
A6: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10;
thus ( x <= y implies f . x <= f . y ) by A4, Def2; ::_thesis: ( f . x <= f . y implies x <= y )
assume A7: f . x <= f . y ; ::_thesis: x <= y
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58;
then reconsider x9 = x, y9 = y as Ideal of L by YELLOW_2:41;
consider Iy being Element of (InclPoset (Ids L)) such that
A8: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41;
reconsider i1 = downarrow (sup Ix), i2 = downarrow (sup Iy) as Element of (InclPoset (Ids L)) by YELLOW_2:41;
A9: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1;
A10: ( f . x9 = sup x9 & f . y9 = sup y9 ) by A2;
( sup (downarrow (sup Ix)) = sup Ix & sup (downarrow (sup Iy)) = sup Iy ) by WAYBEL_0:34;
then downarrow (sup Ix) c= downarrow (sup Iy) by A7, A6, A8, A9, A10, WAYBEL_0:21;
then i1 <= i2 by YELLOW_1:3;
hence x <= y by A6, A8, A9, YELLOW_0:60; ::_thesis: verum
end;
A11: rng f = the carrier of L
proof
thus rng f c= the carrier of L ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of L c= rng f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of L or x in rng f )
assume x in the carrier of L ; ::_thesis: x in rng f
then reconsider x = x as Element of L ;
A12: (SupMap L) . (downarrow x) = sup (downarrow x) by YELLOW_2:def_3
.= x by WAYBEL_0:34 ;
A13: downarrow x is Element of (InclPoset (Ids L)) by YELLOW_2:41;
then ((IdsMap L) * (SupMap L)) . (downarrow x) = (IdsMap L) . ((SupMap L) . (downarrow x)) by FUNCT_2:15
.= downarrow x by A12, YELLOW_2:def_4 ;
then downarrow x in rng ((IdsMap L) * (SupMap L)) by A13, FUNCT_2:4;
then A14: downarrow x in the carrier of (Image ((IdsMap L) * (SupMap L))) by YELLOW_0:def_15;
then f . (downarrow x) = (SupMap L) . ((inclusion ((IdsMap L) * (SupMap L))) . (downarrow x)) by FUNCT_2:15
.= (SupMap L) . (downarrow x) by A14, FUNCT_1:18 ;
hence x in rng f by A12, A14, FUNCT_2:4; ::_thesis: verum
end;
f is V13()
proof
let x, y be Element of (Image ((IdsMap L) * (SupMap L))); :: according to WAYBEL_1:def_1 ::_thesis: ( f . x = f . y implies x = y )
assume A15: f . x = f . y ; ::_thesis: x = y
consider Ix being Element of (InclPoset (Ids L)) such that
A16: ((IdsMap L) * (SupMap L)) . Ix = x by YELLOW_2:10;
consider Iy being Element of (InclPoset (Ids L)) such that
A17: ((IdsMap L) * (SupMap L)) . Iy = y by YELLOW_2:10;
( x is Element of (InclPoset (Ids L)) & y is Element of (InclPoset (Ids L)) ) by YELLOW_0:58;
then reconsider x = x, y = y as Ideal of L by YELLOW_2:41;
reconsider Ix = Ix, Iy = Iy as Ideal of L by YELLOW_2:41;
A18: sup (downarrow (sup Ix)) = sup Ix by WAYBEL_0:34;
A19: ( ((IdsMap L) * (SupMap L)) . Ix = downarrow (sup Ix) & ((IdsMap L) * (SupMap L)) . Iy = downarrow (sup Iy) ) by A1;
( f . x = sup x & f . y = sup y ) by A2;
hence x = y by A15, A16, A17, A19, A18, WAYBEL_0:34; ::_thesis: verum
end;
hence f is isomorphic by A11, A5, WAYBEL_0:66; ::_thesis: verum
end;
definition
let S be non empty RelStr ;
let x be Element of S;
funcx "/\" -> Function of S,S means :Def18: :: WAYBEL_1:def 18
for s being Element of S holds it . s = x "/\" s;
existence
ex b1 being Function of S,S st
for s being Element of S holds b1 . s = x "/\" s
proof
deffunc H1( Element of S) -> M2( the carrier of S) = x "/\" $1;
thus ex f being Function of S,S st
for x being Element of S holds f . x = H1(x) from FUNCT_2:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of S,S st ( for s being Element of S holds b1 . s = x "/\" s ) & ( for s being Element of S holds b2 . s = x "/\" s ) holds
b1 = b2
proof
let f1, f2 be Function of S,S; ::_thesis: ( ( for s being Element of S holds f1 . s = x "/\" s ) & ( for s being Element of S holds f2 . s = x "/\" s ) implies f1 = f2 )
assume that
A1: for s being Element of S holds f1 . s = x "/\" s and
A2: for s being Element of S holds f2 . s = x "/\" s ; ::_thesis: f1 = f2
now__::_thesis:_for_s_being_Element_of_S_holds_f1_._s_=_f2_._s
let s be Element of S; ::_thesis: f1 . s = f2 . s
thus f1 . s = x "/\" s by A1
.= f2 . s by A2 ; ::_thesis: verum
end;
hence f1 = f2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def18 defines "/\" WAYBEL_1:def_18_:_
for S being non empty RelStr
for x being Element of S
for b3 being Function of S,S holds
( b3 = x "/\" iff for s being Element of S holds b3 . s = x "/\" s );
theorem Th59: :: WAYBEL_1:59
for S being non empty RelStr
for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)
proof
let S be non empty RelStr ; ::_thesis: for x, t being Element of S holds { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)
let x, t be Element of S; ::_thesis: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (x "/\") " (downarrow t) c= { s where s is Element of S : x "/\" s <= t }
let a be set ; ::_thesis: ( a in { s where s is Element of S : x "/\" s <= t } implies a in (x "/\") " (downarrow t) )
assume a in { s where s is Element of S : x "/\" s <= t } ; ::_thesis: a in (x "/\") " (downarrow t)
then consider s being Element of S such that
A1: a = s and
A2: x "/\" s <= t ;
(x "/\") . s <= t by A2, Def18;
then (x "/\") . s in downarrow t by WAYBEL_0:17;
hence a in (x "/\") " (downarrow t) by A1, FUNCT_2:38; ::_thesis: verum
end;
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in (x "/\") " (downarrow t) or s in { s where s is Element of S : x "/\" s <= t } )
assume A3: s in (x "/\") " (downarrow t) ; ::_thesis: s in { s where s is Element of S : x "/\" s <= t }
then reconsider s = s as Element of S ;
(x "/\") . s in downarrow t by A3, FUNCT_2:38;
then x "/\" s in downarrow t by Def18;
then x "/\" s <= t by WAYBEL_0:17;
hence s in { s where s is Element of S : x "/\" s <= t } ; ::_thesis: verum
end;
theorem Th60: :: WAYBEL_1:60
for S being Semilattice
for x being Element of S holds x "/\" is monotone
proof
let S be Semilattice; ::_thesis: for x being Element of S holds x "/\" is monotone
let x be Element of S; ::_thesis: x "/\" is monotone
let s1, s2 be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( s1 <= s2 implies (x "/\") . s1 <= (x "/\") . s2 )
assume A1: s1 <= s2 ; ::_thesis: (x "/\") . s1 <= (x "/\") . s2
A2: ex_inf_of {x,s1},S by YELLOW_0:21;
then A3: x "/\" s1 <= x by YELLOW_0:19;
x "/\" s1 <= s1 by A2, YELLOW_0:19;
then ( ex_inf_of {x,s2},S & x "/\" s1 <= s2 ) by A1, ORDERS_2:3, YELLOW_0:21;
then x "/\" s1 <= x "/\" s2 by A3, YELLOW_0:19;
then (x "/\") . s1 <= x "/\" s2 by Def18;
hence (x "/\") . s1 <= (x "/\") . s2 by Def18; ::_thesis: verum
end;
registration
let S be Semilattice;
let x be Element of S;
clusterx "/\" -> monotone ;
coherence
x "/\" is monotone by Th60;
end;
theorem Th61: :: WAYBEL_1:61
for S being non empty RelStr
for x being Element of S
for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
proof
let S be non empty RelStr ; ::_thesis: for x being Element of S
for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
let x be Element of S; ::_thesis: for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
let X be Subset of S; ::_thesis: (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
set Y = { (x "/\" y) where y is Element of S : y in X } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (x "/\" y) where y is Element of S : y in X } c= (x "/\") .: X
let y be set ; ::_thesis: ( y in (x "/\") .: X implies y in { (x "/\" y) where y is Element of S : y in X } )
assume y in (x "/\") .: X ; ::_thesis: y in { (x "/\" y) where y is Element of S : y in X }
then consider z being set such that
A1: z in the carrier of S and
A2: z in X and
A3: y = (x "/\") . z by FUNCT_2:64;
reconsider z = z as Element of S by A1;
y = x "/\" z by A3, Def18;
hence y in { (x "/\" y) where y is Element of S : y in X } by A2; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { (x "/\" y) where y is Element of S : y in X } or y in (x "/\") .: X )
assume y in { (x "/\" y) where y is Element of S : y in X } ; ::_thesis: y in (x "/\") .: X
then consider z being Element of S such that
A4: y = x "/\" z and
A5: z in X ;
y = (x "/\") . z by A4, Def18;
hence y in (x "/\") .: X by A5, FUNCT_2:35; ::_thesis: verum
end;
theorem Th62: :: WAYBEL_1:62
for S being Semilattice holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S )
proof
let S be Semilattice; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S )
hereby ::_thesis: ( ( for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ) implies for x being Element of S holds x "/\" is lower_adjoint )
assume A1: for x being Element of S holds x "/\" is lower_adjoint ; ::_thesis: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S
let x, t be Element of S; ::_thesis: ex_max_of { s where s is Element of S : x "/\" s <= t } ,S
x "/\" is lower_adjoint by A1;
then consider g being Function of S,S such that
A2: [g,(x "/\")] is Galois by Def12;
set X = { s where s is Element of S : x "/\" s <= t } ;
A3: { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) by Th59;
g . t is_maximum_of (x "/\") " (downarrow t) by A2, Th11;
then ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" ( { s where s is Element of S : x "/\" s <= t } ,S) in { s where s is Element of S : x "/\" s <= t } ) by A3, Def7;
hence ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by Def5; ::_thesis: verum
end;
assume A4: for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S ; ::_thesis: for x being Element of S holds x "/\" is lower_adjoint
let x be Element of S; ::_thesis: x "/\" is lower_adjoint
deffunc H1( Element of S) -> M2( the carrier of S) = "\/" (((x "/\") " (downarrow $1)),S);
consider g being Function of S,S such that
A5: for s being Element of S holds g . s = H1(s) from FUNCT_2:sch_4();
now__::_thesis:_for_t_being_Element_of_S_holds_g_._t_is_maximum_of_(x_"/\")_"_(downarrow_t)
let t be Element of S; ::_thesis: g . t is_maximum_of (x "/\") " (downarrow t)
set X = { s where s is Element of S : x "/\" s <= t } ;
ex_max_of { s where s is Element of S : x "/\" s <= t } ,S by A4;
then A6: ( ex_sup_of { s where s is Element of S : x "/\" s <= t } ,S & "\/" ( { s where s is Element of S : x "/\" s <= t } ,S) in { s where s is Element of S : x "/\" s <= t } ) by Def5;
( { s where s is Element of S : x "/\" s <= t } = (x "/\") " (downarrow t) & g . t = "\/" (((x "/\") " (downarrow t)),S) ) by A5, Th59;
hence g . t is_maximum_of (x "/\") " (downarrow t) by A6, Def7; ::_thesis: verum
end;
then [g,(x "/\")] is Galois by Th11;
hence x "/\" is lower_adjoint by Def12; ::_thesis: verum
end;
theorem Th63: :: WAYBEL_1:63
for S being Semilattice st ( for x being Element of S holds x "/\" is lower_adjoint ) holds
for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
proof
let S be Semilattice; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
assume A1: for x being Element of S holds x "/\" is lower_adjoint ; ::_thesis: for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
let X be Subset of S; ::_thesis: ( ex_sup_of X,S implies for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
assume A2: ex_sup_of X,S ; ::_thesis: for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
let x be Element of S; ::_thesis: x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S)
x "/\" is sups-preserving by A1, Th13;
then x "/\" preserves_sup_of X by WAYBEL_0:def_33;
then sup ((x "/\") .: X) = (x "/\") . (sup X) by A2, WAYBEL_0:def_31;
hence x "/\" ("\/" (X,S)) = sup ((x "/\") .: X) by Def18
.= "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) by Th61 ;
::_thesis: verum
end;
theorem :: WAYBEL_1:64
for S being non empty complete Poset holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
proof
let S be non empty complete Poset; ::_thesis: ( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) )
thus ( ( for x being Element of S holds x "/\" is lower_adjoint ) implies for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) by Th63, YELLOW_0:17; ::_thesis: ( ( for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies for x being Element of S holds x "/\" is lower_adjoint )
assume A1: for X being Subset of S
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: for x being Element of S holds x "/\" is lower_adjoint
let x be Element of S; ::_thesis: x "/\" is lower_adjoint
x "/\" is sups-preserving
proof
let X be Subset of S; :: according to WAYBEL_0:def_33 ::_thesis: x "/\" preserves_sup_of X
assume ex_sup_of X,S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,S & "\/" (((x "/\") .: X),S) = (x "/\") . ("\/" (X,S)) )
thus ex_sup_of (x "/\") .: X,S by YELLOW_0:17; ::_thesis: "\/" (((x "/\") .: X),S) = (x "/\") . ("\/" (X,S))
thus (x "/\") . (sup X) = x "/\" ("\/" (X,S)) by Def18
.= "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) by A1
.= sup ((x "/\") .: X) by Th61 ; ::_thesis: verum
end;
hence x "/\" is lower_adjoint by Th17; ::_thesis: verum
end;
theorem Th65: :: WAYBEL_1:65
for S being LATTICE st ( for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) holds
S is distributive
proof
let S be LATTICE; ::_thesis: ( ( for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ) implies S is distributive )
assume A1: for X being Subset of S st ex_sup_of X,S holds
for x being Element of S holds x "/\" ("\/" (X,S)) = "\/" ( { (x "/\" y) where y is Element of S : y in X } ,S) ; ::_thesis: S is distributive
let x, y, z be Element of S; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
set Y = { (x "/\" s) where s is Element of S : s in {y,z} } ;
A2: ex_sup_of {y,z},S by YELLOW_0:20;
now__::_thesis:_for_t_being_set_holds_
(_(_not_t_in__{__(x_"/\"_s)_where_s_is_Element_of_S_:_s_in_{y,z}__}__or_t_=_x_"/\"_y_or_t_=_x_"/\"_z_)_&_(_(_t_=_x_"/\"_y_or_t_=_x_"/\"_z_)_implies_t_in__{__(x_"/\"_s)_where_s_is_Element_of_S_:_s_in_{y,z}__}__)_)
let t be set ; ::_thesis: ( ( not t in { (x "/\" s) where s is Element of S : s in {y,z} } or t = x "/\" y or t = x "/\" z ) & ( ( t = x "/\" y or t = x "/\" z ) implies b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } ) )
hereby ::_thesis: ( ( t = x "/\" y or t = x "/\" z ) implies b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} } )
assume t in { (x "/\" s) where s is Element of S : s in {y,z} } ; ::_thesis: ( t = x "/\" y or t = x "/\" z )
then ex s being Element of S st
( t = x "/\" s & s in {y,z} ) ;
hence ( t = x "/\" y or t = x "/\" z ) by TARSKI:def_2; ::_thesis: verum
end;
assume A3: ( t = x "/\" y or t = x "/\" z ) ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} }
percases ( t = x "/\" y or t = x "/\" z ) by A3;
supposeA4: t = x "/\" y ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} }
y in {y,z} by TARSKI:def_2;
hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A4; ::_thesis: verum
end;
supposeA5: t = x "/\" z ; ::_thesis: b1 in { (x "/\" b2) where s is Element of S : b2 in {y,z} }
z in {y,z} by TARSKI:def_2;
hence t in { (x "/\" s) where s is Element of S : s in {y,z} } by A5; ::_thesis: verum
end;
end;
end;
then A6: { (x "/\" s) where s is Element of S : s in {y,z} } = {(x "/\" y),(x "/\" z)} by TARSKI:def_2;
thus x "/\" (y "\/" z) = x "/\" (sup {y,z}) by YELLOW_0:41
.= "\/" ({(x "/\" y),(x "/\" z)},S) by A1, A6, A2
.= (x "/\" y) "\/" (x "/\" z) by YELLOW_0:41 ; ::_thesis: verum
end;
definition
let H be non empty RelStr ;
attrH is Heyting means :Def19: :: WAYBEL_1:def 19
( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) );
end;
:: deftheorem Def19 defines Heyting WAYBEL_1:def_19_:_
for H being non empty RelStr holds
( H is Heyting iff ( H is LATTICE & ( for x being Element of H holds x "/\" is lower_adjoint ) ) );
registration
cluster non empty Heyting -> non empty reflexive transitive antisymmetric with_suprema with_infima for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
( b1 is with_infima & b1 is with_suprema & b1 is reflexive & b1 is transitive & b1 is antisymmetric ) by Def19;
end;
definition
let H be non empty RelStr ;
let a be Element of H;
assume A1: H is Heyting ;
funca => -> Function of H,H means :Def20: :: WAYBEL_1:def 20
[it,(a "/\")] is Galois ;
existence
ex b1 being Function of H,H st [b1,(a "/\")] is Galois
proof
a "/\" is lower_adjoint by A1, Def19;
hence ex b1 being Function of H,H st [b1,(a "/\")] is Galois by Def12; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of H,H st [b1,(a "/\")] is Galois & [b2,(a "/\")] is Galois holds
b1 = b2
proof
let g1, g2 be Function of H,H; ::_thesis: ( [g1,(a "/\")] is Galois & [g2,(a "/\")] is Galois implies g1 = g2 )
assume that
A2: [g1,(a "/\")] is Galois and
A3: [g2,(a "/\")] is Galois ; ::_thesis: g1 = g2
now__::_thesis:_for_x_being_Element_of_H_holds_g1_._x_=_g2_._x
let x be Element of H; ::_thesis: g1 . x = g2 . x
g1 . x is_maximum_of (a "/\") " (downarrow x) by A1, A2, Th11;
then A4: g1 . x = "\/" (((a "/\") " (downarrow x)),H) by Def7;
g2 . x is_maximum_of (a "/\") " (downarrow x) by A1, A3, Th11;
hence g1 . x = g2 . x by A4, Def7; ::_thesis: verum
end;
hence g1 = g2 by FUNCT_2:63; ::_thesis: verum
end;
end;
:: deftheorem Def20 defines => WAYBEL_1:def_20_:_
for H being non empty RelStr
for a being Element of H st H is Heyting holds
for b3 being Function of H,H holds
( b3 = a => iff [b3,(a "/\")] is Galois );
theorem Th66: :: WAYBEL_1:66
for H being non empty RelStr st H is Heyting holds
H is distributive
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies H is distributive )
assume that
A1: H is LATTICE and
A2: for x being Element of H holds x "/\" is lower_adjoint ; :: according to WAYBEL_1:def_19 ::_thesis: H is distributive
for X being Subset of H st ex_sup_of X,H holds
for x being Element of H holds x "/\" ("\/" (X,H)) = "\/" ( { (x "/\" y) where y is Element of H : y in X } ,H) by A1, A2, Th63;
hence H is distributive by A1, Th65; ::_thesis: verum
end;
registration
cluster non empty Heyting -> non empty distributive for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
b1 is distributive by Th66;
end;
definition
let H be non empty RelStr ;
let a, y be Element of H;
funca => y -> Element of H equals :: WAYBEL_1:def 21
(a =>) . y;
correctness
coherence
(a =>) . y is Element of H;
;
end;
:: deftheorem defines => WAYBEL_1:def_21_:_
for H being non empty RelStr
for a, y being Element of H holds a => y = (a =>) . y;
theorem Th67: :: WAYBEL_1:67
for H being non empty RelStr st H is Heyting holds
for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y ) )
assume A1: H is Heyting ; ::_thesis: for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )
let x, a, y be Element of H; ::_thesis: ( x >= a "/\" y iff a => x >= y )
[(a =>),(a "/\")] is Galois by A1, Def20;
then ( x >= (a "/\") . y iff (a =>) . x >= y ) by A1, Th8;
hence ( x >= a "/\" y iff a => x >= y ) by Def18; ::_thesis: verum
end;
theorem Th68: :: WAYBEL_1:68
for H being non empty RelStr st H is Heyting holds
H is upper-bounded
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies H is upper-bounded )
assume A1: H is Heyting ; ::_thesis: H is upper-bounded
set a = the Element of H;
take the Element of H => the Element of H ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of H is_<=_than the Element of H => the Element of H
let y be Element of H; :: according to LATTICE3:def_9 ::_thesis: ( not y in the carrier of H or y <= the Element of H => the Element of H )
assume y in the carrier of H ; ::_thesis: y <= the Element of H => the Element of H
the Element of H >= the Element of H "/\" y by A1, YELLOW_0:23;
hence y <= the Element of H => the Element of H by A1, Th67; ::_thesis: verum
end;
registration
cluster non empty Heyting -> non empty upper-bounded for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Heyting holds
b1 is upper-bounded by Th68;
end;
theorem Th69: :: WAYBEL_1:69
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds
( Top H = a => b iff a <= b )
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds
( Top H = a => b iff a <= b ) )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds
( Top H = a => b iff a <= b )
let a, b be Element of H; ::_thesis: ( Top H = a => b iff a <= b )
A2: a "/\" (Top H) = (Top H) "/\" a by A1, LATTICE3:15
.= a by A1, Th4 ;
hereby ::_thesis: ( a <= b implies Top H = a => b )
assume Top H = a => b ; ::_thesis: a <= b
then a => b >= Top H by A1, ORDERS_2:1;
hence a <= b by A1, A2, Th67; ::_thesis: verum
end;
assume a <= b ; ::_thesis: Top H = a => b
then A3: a => b >= Top H by A1, A2, Th67;
a => b <= Top H by A1, YELLOW_0:45;
hence Top H = a => b by A1, A3, ORDERS_2:2; ::_thesis: verum
end;
theorem :: WAYBEL_1:70
for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => a
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a being Element of H holds Top H = a => a )
assume A1: H is Heyting ; ::_thesis: for a being Element of H holds Top H = a => a
let a be Element of H; ::_thesis: Top H = a => a
a >= a "/\" (Top H) by A1, YELLOW_0:23;
then A2: Top H <= a => a by A1, Th67;
Top H >= a => a by A1, YELLOW_0:45;
hence Top H = a => a by A1, A2, ORDERS_2:2; ::_thesis: verum
end;
theorem :: WAYBEL_1:71
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b
let a, b be Element of H; ::_thesis: ( Top H = a => b & Top H = b => a implies a = b )
assume A2: Top H = a => b ; ::_thesis: ( not Top H = b => a or a = b )
assume Top H = b => a ; ::_thesis: a = b
then A3: b <= a by A1, Th69;
a <= b by A1, A2, Th69;
hence a = b by A1, A3, ORDERS_2:2; ::_thesis: verum
end;
theorem Th72: :: WAYBEL_1:72
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds b <= a => b
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds b <= a => b )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds b <= a => b
let a, b be Element of H; ::_thesis: b <= a => b
a "/\" b <= b by A1, YELLOW_0:23;
hence b <= a => b by A1, Th67; ::_thesis: verum
end;
theorem :: WAYBEL_1:73
for H being non empty RelStr st H is Heyting holds
for a being Element of H holds Top H = a => (Top H)
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a being Element of H holds Top H = a => (Top H) )
assume A1: H is Heyting ; ::_thesis: for a being Element of H holds Top H = a => (Top H)
let a be Element of H; ::_thesis: Top H = a => (Top H)
a <= Top H by A1, YELLOW_0:45;
hence Top H = a => (Top H) by A1, Th69; ::_thesis: verum
end;
theorem :: WAYBEL_1:74
for H being non empty RelStr st H is Heyting holds
for b being Element of H holds b = (Top H) => b
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for b being Element of H holds b = (Top H) => b )
assume A1: H is Heyting ; ::_thesis: for b being Element of H holds b = (Top H) => b
let b be Element of H; ::_thesis: b = (Top H) => b
(Top H) => b <= (Top H) => b by A1, ORDERS_2:1;
then (Top H) "/\" ((Top H) => b) <= b by A1, Th67;
then A2: (Top H) => b <= b by A1, Th4;
(Top H) => b >= b by A1, Th72;
hence b = (Top H) => b by A1, A2, ORDERS_2:2; ::_thesis: verum
end;
Lm5: for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) <= b
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) <= b )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds a "/\" (a => b) <= b
let a, b be Element of H; ::_thesis: a "/\" (a => b) <= b
a => b <= a => b by A1, ORDERS_2:1;
hence a "/\" (a => b) <= b by A1, Th67; ::_thesis: verum
end;
theorem Th75: :: WAYBEL_1:75
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st a <= b holds
b => c <= a => c
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H st a <= b holds
b => c <= a => c )
assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H st a <= b holds
b => c <= a => c
let a, b, c be Element of H; ::_thesis: ( a <= b implies b => c <= a => c )
assume a <= b ; ::_thesis: b => c <= a => c
then A2: a "/\" (b => c) <= b "/\" (b => c) by A1, Th1;
b "/\" (b => c) <= c by A1, Lm5;
then a "/\" (b => c) <= c by A1, A2, ORDERS_2:3;
hence b => c <= a => c by A1, Th67; ::_thesis: verum
end;
theorem :: WAYBEL_1:76
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H st b <= c holds
a => b <= a => c
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H st b <= c holds
a => b <= a => c )
assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H st b <= c holds
a => b <= a => c
let a, b, c be Element of H; ::_thesis: ( b <= c implies a => b <= a => c )
assume A2: b <= c ; ::_thesis: a => b <= a => c
a "/\" (a => b) <= b by A1, Lm5;
then a "/\" (a => b) <= c by A1, A2, ORDERS_2:3;
hence a => b <= a => c by A1, Th67; ::_thesis: verum
end;
theorem Th77: :: WAYBEL_1:77
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) = a "/\" b
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds a "/\" (a => b) = a "/\" b )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds a "/\" (a => b) = a "/\" b
let a, b be Element of H; ::_thesis: a "/\" (a => b) = a "/\" b
(a "/\" (a => b)) "/\" a <= b "/\" a by A1, Lm5, Th1;
then a "/\" (a "/\" (a => b)) <= b "/\" a by A1, LATTICE3:15;
then a "/\" (a "/\" (a => b)) <= a "/\" b by A1, LATTICE3:15;
then (a "/\" a) "/\" (a => b) <= a "/\" b by A1, LATTICE3:16;
then A2: a "/\" (a => b) <= a "/\" b by A1, YELLOW_0:25;
b "/\" a <= (a => b) "/\" a by A1, Th1, Th72;
then a "/\" b <= (a => b) "/\" a by A1, LATTICE3:15;
then a "/\" b <= a "/\" (a => b) by A1, LATTICE3:15;
hence a "/\" (a => b) = a "/\" b by A1, A2, ORDERS_2:2; ::_thesis: verum
end;
theorem Th78: :: WAYBEL_1:78
for H being non empty RelStr st H is Heyting holds
for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting implies for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c) )
assume A1: H is Heyting ; ::_thesis: for a, b, c being Element of H holds (a "\/" b) => c = (a => c) "/\" (b => c)
let a, b, c be Element of H; ::_thesis: (a "\/" b) => c = (a => c) "/\" (b => c)
( (a "/\" c) "/\" (b => c) <= a "/\" c & a "/\" c <= c ) by A1, YELLOW_0:23;
then A2: (a "/\" c) "/\" (b => c) <= c by A1, ORDERS_2:3;
( (b "/\" c) "/\" (a => c) <= b "/\" c & b "/\" c <= c ) by A1, YELLOW_0:23;
then A3: (b "/\" c) "/\" (a => c) <= c by A1, ORDERS_2:3;
set d = (a => c) "/\" (b => c);
(a "\/" b) "/\" ((a => c) "/\" (b => c)) = ((a => c) "/\" (b => c)) "/\" (a "\/" b) by A1, LATTICE3:15
.= (((a => c) "/\" (b => c)) "/\" a) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, Def3
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (((a => c) "/\" (b => c)) "/\" b) by A1, LATTICE3:15
.= (a "/\" ((a => c) "/\" (b => c))) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((a => c) "/\" (b => c))) by A1, LATTICE3:16
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" (b "/\" ((b => c) "/\" (a => c))) by A1, LATTICE3:15
.= ((a "/\" (a => c)) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, LATTICE3:16
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" (b => c)) "/\" (a => c)) by A1, Th77
.= ((a "/\" c) "/\" (b => c)) "\/" ((b "/\" c) "/\" (a => c)) by A1, Th77 ;
then (a "\/" b) "/\" ((a => c) "/\" (b => c)) <= c by A1, A2, A3, YELLOW_0:22;
then A4: (a "\/" b) => c >= (a => c) "/\" (b => c) by A1, Th67;
b <= a "\/" b by A1, YELLOW_0:22;
then A5: (a "\/" b) => c <= b => c by A1, Th75;
a <= a "\/" b by A1, YELLOW_0:22;
then (a "\/" b) => c <= a => c by A1, Th75;
then (a "\/" b) => c <= (a => c) "/\" (b => c) by A1, A5, YELLOW_0:23;
hence (a "\/" b) => c = (a => c) "/\" (b => c) by A1, A4, ORDERS_2:2; ::_thesis: verum
end;
definition
let H be non empty RelStr ;
let a be Element of H;
func 'not' a -> Element of H equals :: WAYBEL_1:def 22
a => (Bottom H);
correctness
coherence
a => (Bottom H) is Element of H;
;
end;
:: deftheorem defines 'not' WAYBEL_1:def_22_:_
for H being non empty RelStr
for a being Element of H holds 'not' a = a => (Bottom H);
theorem :: WAYBEL_1:79
for H being non empty RelStr st H is Heyting & H is lower-bounded holds
for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting & H is lower-bounded implies for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } )
assume that
A1: H is Heyting and
A2: H is lower-bounded ; ::_thesis: for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
let a be Element of H; ::_thesis: 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
set X = { x where x is Element of H : a "/\" x = Bottom H } ;
set Y = { x where x is Element of H : a "/\" x <= Bottom H } ;
A3: { x where x is Element of H : a "/\" x = Bottom H } = { x where x is Element of H : a "/\" x <= Bottom H }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { x where x is Element of H : a "/\" x <= Bottom H } c= { x where x is Element of H : a "/\" x = Bottom H }
let y be set ; ::_thesis: ( y in { x where x is Element of H : a "/\" x = Bottom H } implies y in { x where x is Element of H : a "/\" x <= Bottom H } )
assume y in { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: y in { x where x is Element of H : a "/\" x <= Bottom H }
then consider x being Element of H such that
A4: y = x and
A5: a "/\" x = Bottom H ;
a "/\" x <= Bottom H by A1, A5, ORDERS_2:1;
hence y in { x where x is Element of H : a "/\" x <= Bottom H } by A4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { x where x is Element of H : a "/\" x <= Bottom H } or y in { x where x is Element of H : a "/\" x = Bottom H } )
assume y in { x where x is Element of H : a "/\" x <= Bottom H } ; ::_thesis: y in { x where x is Element of H : a "/\" x = Bottom H }
then consider x being Element of H such that
A6: y = x and
A7: a "/\" x <= Bottom H ;
Bottom H <= a "/\" x by A1, A2, YELLOW_0:44;
then Bottom H = a "/\" x by A1, A7, ORDERS_2:2;
hence y in { x where x is Element of H : a "/\" x = Bottom H } by A6; ::_thesis: verum
end;
A8: now__::_thesis:_for_b_being_Element_of_H_st_b_is_>=_than__{__x_where_x_is_Element_of_H_:_a_"/\"_x_=_Bottom_H__}__holds_
'not'_a_<=_b
a => (Bottom H) <= a => (Bottom H) by A1, ORDERS_2:1;
then a "/\" ('not' a) <= Bottom H by A1, Th67;
then A9: 'not' a in { x where x is Element of H : a "/\" x = Bottom H } by A3;
let b be Element of H; ::_thesis: ( b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } implies 'not' a <= b )
assume b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: 'not' a <= b
hence 'not' a <= b by A9, LATTICE3:def_9; ::_thesis: verum
end;
for x being Element of H holds x "/\" is lower_adjoint by A1, Def19;
then A10: ex_max_of { x where x is Element of H : a "/\" x = Bottom H } ,H by A1, A3, Th62;
hence ex_sup_of { x where x is Element of H : a "/\" x = Bottom H } ,H by Def5; :: according to WAYBEL_1:def_7 ::_thesis: ( 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) & "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } )
'not' a is_>=_than { x where x is Element of H : a "/\" x = Bottom H }
proof
let b be Element of H; :: according to LATTICE3:def_9 ::_thesis: ( not b in { x where x is Element of H : a "/\" x = Bottom H } or b <= 'not' a )
assume b in { x where x is Element of H : a "/\" x = Bottom H } ; ::_thesis: b <= 'not' a
then ex x being Element of H st
( x = b & a "/\" x <= Bottom H ) by A3;
hence b <= 'not' a by A1, Th67; ::_thesis: verum
end;
hence 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) by A1, A8, YELLOW_0:30; ::_thesis: "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H }
thus "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) in { x where x is Element of H : a "/\" x = Bottom H } by A10, Def5; ::_thesis: verum
end;
theorem Th80: :: WAYBEL_1:80
for H being non empty RelStr st H is Heyting & H is lower-bounded holds
( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )
proof
let H be non empty RelStr ; ::_thesis: ( H is Heyting & H is lower-bounded implies ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H ) )
assume that
A1: H is Heyting and
A2: H is lower-bounded ; ::_thesis: ( 'not' (Bottom H) = Top H & 'not' (Top H) = Bottom H )
(Top H) => (Bottom H) <= (Top H) => (Bottom H) by A1, ORDERS_2:1;
then A3: Bottom H >= (Top H) "/\" ('not' (Top H)) by A1, Th67;
Bottom H >= (Bottom H) "/\" (Top H) by A1, YELLOW_0:23;
then A4: Top H <= (Bottom H) => (Bottom H) by A1, Th67;
Bottom H <= (Top H) "/\" ('not' (Top H)) by A1, A2, YELLOW_0:44;
then A5: Bottom H = (Top H) "/\" ('not' (Top H)) by A1, A3, ORDERS_2:2;
'not' (Bottom H) <= Top H by A1, YELLOW_0:45;
hence Top H = 'not' (Bottom H) by A1, A4, ORDERS_2:2; ::_thesis: 'not' (Top H) = Bottom H
'not' (Top H) <= Top H by A1, YELLOW_0:45;
hence 'not' (Top H) = ('not' (Top H)) "/\" (Top H) by A1, YELLOW_0:25
.= Bottom H by A1, A5, LATTICE3:15 ;
::_thesis: verum
end;
theorem :: WAYBEL_1:81
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a )
proof
let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a ) )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds
( 'not' a >= b iff 'not' b >= a )
let a, b be Element of H; ::_thesis: ( 'not' a >= b iff 'not' b >= a )
A2: ( Bottom H >= a "/\" b iff a => (Bottom H) >= b ) by A1, Th67;
( Bottom H >= b "/\" a iff b => (Bottom H) >= a ) by A1, Th67;
hence ( 'not' a >= b iff 'not' b >= a ) by A1, A2, LATTICE3:15; ::_thesis: verum
end;
theorem Th82: :: WAYBEL_1:82
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H )
proof
let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H ) )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds
( 'not' a >= b iff a "/\" b = Bottom H )
let a, b be Element of H; ::_thesis: ( 'not' a >= b iff a "/\" b = Bottom H )
hereby ::_thesis: ( a "/\" b = Bottom H implies 'not' a >= b )
assume 'not' a >= b ; ::_thesis: a "/\" b = Bottom H
then A2: a "/\" b <= Bottom H by A1, Th67;
a "/\" b >= Bottom H by A1, YELLOW_0:44;
hence a "/\" b = Bottom H by A1, A2, ORDERS_2:2; ::_thesis: verum
end;
assume a "/\" b = Bottom H ; ::_thesis: 'not' a >= b
then a "/\" b <= Bottom H by A1, ORDERS_2:1;
hence 'not' a >= b by A1, Th67; ::_thesis: verum
end;
theorem :: WAYBEL_1:83
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H st a <= b holds
'not' b <= 'not' a
proof
let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H st a <= b holds
'not' b <= 'not' a )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H st a <= b holds
'not' b <= 'not' a
let a, b be Element of H; ::_thesis: ( a <= b implies 'not' b <= 'not' a )
A2: 'not' b >= 'not' b by A1, ORDERS_2:1;
assume a <= b ; ::_thesis: 'not' b <= 'not' a
then a "/\" ('not' b) = (a "/\" b) "/\" ('not' b) by A1, YELLOW_0:25
.= a "/\" (b "/\" ('not' b)) by A1, LATTICE3:16
.= a "/\" (Bottom H) by A1, A2, Th82
.= (Bottom H) "/\" a by A1, LATTICE3:15
.= Bottom H by A1, Th3 ;
hence 'not' b <= 'not' a by A1, Th82; ::_thesis: verum
end;
theorem :: WAYBEL_1:84
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds 'not' (a "\/" b) = ('not' a) "/\" ('not' b) by Th78;
theorem :: WAYBEL_1:85
for H being non empty lower-bounded RelStr st H is Heyting holds
for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
proof
let H be non empty lower-bounded RelStr ; ::_thesis: ( H is Heyting implies for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) )
assume A1: H is Heyting ; ::_thesis: for a, b being Element of H holds 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
then A2: Bottom H <= Bottom H by ORDERS_2:1;
let a, b be Element of H; ::_thesis: 'not' (a "/\" b) >= ('not' a) "\/" ('not' b)
A3: 'not' a <= 'not' a by A1, ORDERS_2:1;
A4: 'not' b <= 'not' b by A1, ORDERS_2:1;
(a "/\" b) "/\" (('not' a) "\/" ('not' b)) = ((a "/\" b) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, Def3
.= ((b "/\" a) "/\" ('not' a)) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:15
.= (b "/\" (a "/\" ('not' a))) "\/" ((a "/\" b) "/\" ('not' b)) by A1, LATTICE3:16
.= (b "/\" (a "/\" ('not' a))) "\/" (a "/\" (b "/\" ('not' b))) by A1, LATTICE3:16
.= (b "/\" (Bottom H)) "\/" (a "/\" (b "/\" ('not' b))) by A1, A3, Th82
.= (b "/\" (Bottom H)) "\/" (a "/\" (Bottom H)) by A1, A4, Th82
.= ((Bottom H) "/\" b) "\/" (a "/\" (Bottom H)) by A1, LATTICE3:15
.= ((Bottom H) "/\" b) "\/" ((Bottom H) "/\" a) by A1, LATTICE3:15
.= (Bottom H) "\/" ((Bottom H) "/\" a) by A1, Th3
.= (Bottom H) "\/" (Bottom H) by A1, Th3
.= Bottom H by A1, A2, YELLOW_0:24 ;
hence 'not' (a "/\" b) >= ('not' a) "\/" ('not' b) by A1, Th82; ::_thesis: verum
end;
definition
let L be non empty RelStr ;
let x, y be Element of L;
predy is_a_complement_of x means :Def23: :: WAYBEL_1:def 23
( x "\/" y = Top L & x "/\" y = Bottom L );
end;
:: deftheorem Def23 defines is_a_complement_of WAYBEL_1:def_23_:_
for L being non empty RelStr
for x, y being Element of L holds
( y is_a_complement_of x iff ( x "\/" y = Top L & x "/\" y = Bottom L ) );
definition
let L be non empty RelStr ;
attrL is complemented means :Def24: :: WAYBEL_1:def 24
for x being Element of L ex y being Element of L st y is_a_complement_of x;
end;
:: deftheorem Def24 defines complemented WAYBEL_1:def_24_:_
for L being non empty RelStr holds
( L is complemented iff for x being Element of L ex y being Element of L st y is_a_complement_of x );
registration
let X be set ;
cluster BoolePoset X -> complemented ;
coherence
BoolePoset X is complemented
proof
let x be Element of (BoolePoset X); :: according to WAYBEL_1:def_24 ::_thesis: ex y being Element of (BoolePoset X) st y is_a_complement_of x
A1: the carrier of (BoolePoset X) = the carrier of (LattPOSet (BooleLatt X)) by YELLOW_1:def_2
.= bool X by LATTICE3:def_1 ;
then reconsider y = X \ x as Element of (BoolePoset X) by XBOOLE_1:109;
take y ; ::_thesis: y is_a_complement_of x
thus x "\/" y = x \/ y by YELLOW_1:17
.= X \/ x by XBOOLE_1:39
.= X by A1, XBOOLE_1:12
.= Top (BoolePoset X) by YELLOW_1:19 ; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" y = Bottom (BoolePoset X)
A2: x misses y by XBOOLE_1:79;
thus x "/\" y = x /\ y by YELLOW_1:17
.= {} by A2, XBOOLE_0:def_7
.= Bottom (BoolePoset X) by YELLOW_1:18 ; ::_thesis: verum
end;
end;
Lm6: for L being bounded LATTICE st L is distributive & L is complemented holds
for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
proof
let L be bounded LATTICE; ::_thesis: ( L is distributive & L is complemented implies for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) )
assume that
A1: L is distributive and
A2: L is complemented ; ::_thesis: for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
let x be Element of L; ::_thesis: ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
consider x9 being Element of L such that
A3: x9 is_a_complement_of x by A2, Def24;
take x9 ; ::_thesis: for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
let y be Element of L; ::_thesis: ( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
(y "\/" x9) "/\" x = (x "/\" y) "\/" (x "/\" x9) by A1, Def3
.= (Bottom L) "\/" (x "/\" y) by A3, Def23
.= x "/\" y by Th3 ;
hence (y "\/" x9) "/\" x <= y by YELLOW_0:23; ::_thesis: y <= (y "/\" x) "\/" x9
(y "/\" x) "\/" x9 = (x9 "\/" y) "/\" (x9 "\/" x) by A1, Th5
.= (x9 "\/" y) "/\" (Top L) by A3, Def23
.= x9 "\/" y by Th4 ;
hence y <= (y "/\" x) "\/" x9 by YELLOW_0:22; ::_thesis: verum
end;
Lm7: for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
proof
let L be bounded LATTICE; ::_thesis: ( ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) implies ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )
defpred S1[ Element of L, Element of L] means for y being Element of L holds
( (y "\/" $2) "/\" $1 <= y & y <= (y "/\" $1) "\/" $2 );
assume A1: for x being Element of L ex x9 being Element of L st S1[x,x9] ; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
consider g9 being Function of L,L such that
A2: for x being Element of L holds S1[x,g9 . x] from FUNCT_2:sch_3(A1);
A3: now__::_thesis:_for_y_being_Element_of_L
for_g_being_Function_of_L,L_st_(_for_z_being_Element_of_L_holds_g_._z_=_(g9_._y)_"\/"_z_)_holds_
[g,(y_"/\")]_is_Galois
let y be Element of L; ::_thesis: for g being Function of L,L st ( for z being Element of L holds g . z = (g9 . y) "\/" z ) holds
[g,(y "/\")] is Galois
let g be Function of L,L; ::_thesis: ( ( for z being Element of L holds g . z = (g9 . y) "\/" z ) implies [g,(y "/\")] is Galois )
assume A4: for z being Element of L holds g . z = (g9 . y) "\/" z ; ::_thesis: [g,(y "/\")] is Galois
A5: now__::_thesis:_for_x,_z_being_Element_of_L_holds_
(_(_x_<=_g_._z_implies_(y_"/\")_._x_<=_z_)_&_(_(y_"/\")_._x_<=_z_implies_x_<=_g_._z_)_)
let x, z be Element of L; ::_thesis: ( ( x <= g . z implies (y "/\") . x <= z ) & ( (y "/\") . x <= z implies x <= g . z ) )
hereby ::_thesis: ( (y "/\") . x <= z implies x <= g . z )
assume x <= g . z ; ::_thesis: (y "/\") . x <= z
then x <= (g9 . y) "\/" z by A4;
then A6: x "/\" y <= ((g9 . y) "\/" z) "/\" y by Th1;
((g9 . y) "\/" z) "/\" y <= z by A2;
then x "/\" y <= z by A6, ORDERS_2:3;
hence (y "/\") . x <= z by Def18; ::_thesis: verum
end;
assume (y "/\") . x <= z ; ::_thesis: x <= g . z
then y "/\" x <= z by Def18;
then A7: (x "/\" y) "\/" (g9 . y) <= z "\/" (g9 . y) by Th2;
x <= (x "/\" y) "\/" (g9 . y) by A2;
then x <= z "\/" (g9 . y) by A7, ORDERS_2:3;
hence x <= g . z by A4; ::_thesis: verum
end;
g is monotone
proof
let z1, z2 be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( z1 <= z2 implies g . z1 <= g . z2 )
assume z1 <= z2 ; ::_thesis: g . z1 <= g . z2
then (g9 . y) "\/" z1 <= z2 "\/" (g9 . y) by Th2;
then g . z1 <= (g9 . y) "\/" z2 by A4;
hence g . z1 <= g . z2 by A4; ::_thesis: verum
end;
hence [g,(y "/\")] is Galois by A5, Th8; ::_thesis: verum
end;
thus A8: L is Heyting ::_thesis: for x being Element of L holds 'not' ('not' x) = x
proof
thus L is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for x being Element of L holds x "/\" is lower_adjoint
let y be Element of L; ::_thesis: y "/\" is lower_adjoint
deffunc H1( Element of L) -> M2( the carrier of L) = (g9 . y) "\/" $1;
consider g being Function of L,L such that
A9: for z being Element of L holds g . z = H1(z) from FUNCT_2:sch_4();
[g,(y "/\")] is Galois by A3, A9;
hence y "/\" is lower_adjoint by Def12; ::_thesis: verum
end;
A10: now__::_thesis:_for_x_being_Element_of_L_holds_'not'_x_=_g9_._x
let x be Element of L; ::_thesis: 'not' x = g9 . x
deffunc H1( Element of L) -> M2( the carrier of L) = (g9 . x) "\/" $1;
consider g being Function of L,L such that
A11: for z being Element of L holds g . z = H1(z) from FUNCT_2:sch_4();
[g,(x "/\")] is Galois by A3, A11;
then g = x => by A8, Def20;
hence 'not' x = (Bottom L) "\/" (g9 . x) by A11
.= g9 . x by Th3 ;
::_thesis: verum
end;
A12: now__::_thesis:_for_x_being_Element_of_L_holds_Bottom_L_=_x_"/\"_('not'_x)
let x be Element of L; ::_thesis: Bottom L = x "/\" ('not' x)
((Bottom L) "\/" (g9 . x)) "/\" x <= Bottom L by A2;
then (x "/\" (Bottom L)) "\/" (x "/\" (g9 . x)) <= Bottom L by A8, Def3;
then (Bottom L) "\/" (x "/\" (g9 . x)) <= Bottom L by Th3;
then A13: x "/\" (g9 . x) <= Bottom L by Th3;
Bottom L <= x "/\" (g9 . x) by YELLOW_0:44;
hence Bottom L = x "/\" (g9 . x) by A13, ORDERS_2:2
.= x "/\" ('not' x) by A10 ;
::_thesis: verum
end;
let x be Element of L; ::_thesis: 'not' ('not' x) = x
A14: now__::_thesis:_for_x_being_Element_of_L_holds_Top_L_=_x_"\/"_('not'_x)
let x be Element of L; ::_thesis: Top L = x "\/" ('not' x)
Top L <= ((Top L) "/\" x) "\/" (g9 . x) by A2;
then A15: Top L <= x "\/" (g9 . x) by Th4;
x "\/" (g9 . x) <= Top L by YELLOW_0:45;
hence Top L = x "\/" (g9 . x) by A15, ORDERS_2:2
.= x "\/" ('not' x) by A10 ;
::_thesis: verum
end;
then (('not' x) "\/" ('not' ('not' x))) "/\" x = (Top L) "/\" x ;
then x = x "/\" (('not' x) "\/" ('not' ('not' x))) by Th4
.= (x "/\" ('not' x)) "\/" (x "/\" ('not' ('not' x))) by A8, Def3
.= (Bottom L) "\/" (x "/\" ('not' ('not' x))) by A12
.= x "/\" ('not' ('not' x)) by Th3 ;
then A16: x <= 'not' ('not' x) by YELLOW_0:25;
(Bottom L) "\/" x = (('not' x) "/\" ('not' ('not' x))) "\/" x by A12;
then x = x "\/" (('not' x) "/\" ('not' ('not' x))) by Th3
.= (x "\/" ('not' x)) "/\" (x "\/" ('not' ('not' x))) by A8, Th5
.= (Top L) "/\" (x "\/" ('not' ('not' x))) by A14
.= x "\/" ('not' ('not' x)) by Th4 ;
hence 'not' ('not' x) = x by A16, YELLOW_0:24; ::_thesis: verum
end;
theorem Th86: :: WAYBEL_1:86
for L being bounded LATTICE st L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) holds
for x being Element of L holds 'not' x is_a_complement_of x
proof
let L be bounded LATTICE; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies for x being Element of L holds 'not' x is_a_complement_of x )
assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' ('not' x) = x ; ::_thesis: for x being Element of L holds 'not' x is_a_complement_of x
let x be Element of L; ::_thesis: 'not' x is_a_complement_of x
A3: 'not' (x "\/" ('not' x)) = ('not' x) "/\" ('not' ('not' x)) by A1, Th78
.= x "/\" ('not' x) by A2 ;
A4: 'not' x >= 'not' x by ORDERS_2:1;
then x "/\" ('not' x) = Bottom L by A1, Th82;
hence x "\/" ('not' x) = 'not' (Bottom L) by A2, A3
.= Top L by A1, Th80 ;
:: according to WAYBEL_1:def_23 ::_thesis: x "/\" ('not' x) = Bottom L
thus x "/\" ('not' x) = Bottom L by A1, A4, Th82; ::_thesis: verum
end;
theorem Th87: :: WAYBEL_1:87
for L being bounded LATTICE holds
( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )
proof
let L be bounded LATTICE; ::_thesis: ( L is distributive & L is complemented iff ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) )
hereby ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) implies ( L is distributive & L is complemented ) )
assume ( L is distributive & L is complemented ) ; ::_thesis: ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
then for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) by Lm6;
hence ( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) ) by Lm7; ::_thesis: verum
end;
assume that
A1: L is Heyting and
A2: for x being Element of L holds 'not' ('not' x) = x ; ::_thesis: ( L is distributive & L is complemented )
thus L is distributive by A1; ::_thesis: L is complemented
let x be Element of L; :: according to WAYBEL_1:def_24 ::_thesis: ex y being Element of L st y is_a_complement_of x
take 'not' x ; ::_thesis: 'not' x is_a_complement_of x
thus 'not' x is_a_complement_of x by A1, A2, Th86; ::_thesis: verum
end;
definition
let B be non empty RelStr ;
attrB is Boolean means :Def25: :: WAYBEL_1:def 25
( B is LATTICE & B is bounded & B is distributive & B is complemented );
end;
:: deftheorem Def25 defines Boolean WAYBEL_1:def_25_:_
for B being non empty RelStr holds
( B is Boolean iff ( B is LATTICE & B is bounded & B is distributive & B is complemented ) );
registration
cluster non empty Boolean -> non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Boolean holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented ) by Def25;
end;
registration
cluster non empty reflexive transitive antisymmetric with_suprema with_infima bounded distributive complemented -> non empty Boolean for RelStr ;
coherence
for b1 being non empty RelStr st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is with_infima & b1 is with_suprema & b1 is bounded & b1 is distributive & b1 is complemented holds
b1 is Boolean by Def25;
end;
registration
cluster non empty Boolean -> non empty Heyting for RelStr ;
coherence
for b1 being non empty RelStr st b1 is Boolean holds
b1 is Heyting by Th87;
end;
registration
cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Boolean for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is Boolean & not b1 is empty )
proof
take BoolePoset {} ; ::_thesis: ( BoolePoset {} is strict & BoolePoset {} is Boolean & not BoolePoset {} is empty )
thus ( BoolePoset {} is strict & BoolePoset {} is Boolean & not BoolePoset {} is empty ) ; ::_thesis: verum
end;
end;
registration
cluster non empty strict reflexive transitive antisymmetric with_suprema with_infima Heyting for RelStr ;
existence
ex b1 being LATTICE st
( b1 is strict & b1 is Heyting & not b1 is empty )
proof
set L = the non empty strict Boolean LATTICE;
take the non empty strict Boolean LATTICE ; ::_thesis: ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty )
thus ( the non empty strict Boolean LATTICE is strict & the non empty strict Boolean LATTICE is Heyting & not the non empty strict Boolean LATTICE is empty ) ; ::_thesis: verum
end;
end;