let S, T be complete LATTICE; :: thesis: ( T is algebraic implies for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ) )
assume A1: T is algebraic ; :: thesis: for g being infs-preserving Function of S,T holds
( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
let g be infs-preserving Function of S,T; :: thesis: ( g is directed-sups-preserving iff (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) )
hereby :: thesis: ( (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) implies g is directed-sups-preserving )
assume g is directed-sups-preserving ; :: thesis: (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S)
then LowerAdj g is waybelow-preserving by Th22;
then LowerAdj g is compact-preserving by Th56;
hence (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) by Th66; :: thesis: verum
end;
assume (LowerAdj g) | the carrier of (CompactSublatt T) is finite-sups-preserving Function of (CompactSublatt T),(CompactSublatt S) ; :: thesis: g is directed-sups-preserving
then LowerAdj g is compact-preserving by Th66;
then LowerAdj g is waybelow-preserving by A1, Th57;
hence g is directed-sups-preserving by A1, Th23; :: thesis: verum