The abstract of the Mizar article:

Lawson Topology in Continuous Lattices

by

Grzegorz Bancerek

Received July 12, 1998

MML identifier: WAYBEL21

[ Mizar article, MML identifier index ]

environ

 vocabulary WAYBEL_0, LATTICES, PRE_TOPC, FINSET_1, FUNCOP_1, YELLOW_0, BOOLE,
      RELAT_1, FUNCT_1, ORDINAL2, SEQM_3, LATTICE3, ORDERS_1, QUANTAL1, BHSP_3,
      CAT_1, FUNCT_3, WELLORD1, WAYBEL_5, CONNSP_2, TOPS_1, RELAT_2, WAYBEL_9,
      OPPCAT_1, SUBSET_1, WAYBEL19, YELLOW_6, WAYBEL11, CANTOR_1, YELLOW_9,
      PROB_1, YELLOW_2, PRELAMB, COMPTS_1, WAYBEL21;
 notation TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
      TOLER_1, STRUCT_0, PRE_TOPC, TOPS_1, CONNSP_2, COMPTS_1, CANTOR_1,
      ORDERS_1, LATTICE3, ORDERS_3, YELLOW_0, YELLOW_2, WAYBEL_0, WAYBEL_3,
      WAYBEL_5, YELLOW_6, YELLOW_7, BORSUK_1, WAYBEL_9, YELLOW_9, WAYBEL11,
      WAYBEL17, WAYBEL19;
 constructors TOLER_1, ORDERS_3, WAYBEL_1, CANTOR_1, TOPS_1, WAYBEL_3,
      NATTRA_1, URYSOHN1, YELLOW_9, WAYBEL19, WAYBEL17, MEMBERED, PARTFUN1;
 clusters STRUCT_0, YELLOW_0, RELSET_1, LATTICE3, WAYBEL_0, FINSET_1, PUA2MSS1,
      YELLOW_6, WAYBEL_2, WAYBEL_9, WAYBEL10, WAYBEL17, YELLOW_9, WAYBEL19,
      SUBSET_1, MEMBERED, RELAT_1, ZFMISC_1, FUNCT_2, PARTFUN1;
 requirements SUBSET, BOOLE;


begin :: Semilattice homomorphism and inheritance

definition
 let S,T be Semilattice such that
   S is upper-bounded implies T is upper-bounded;
 mode SemilatticeHomomorphism of S,T -> map of S,T means
:: WAYBEL21:def 1

  for X being finite Subset of S holds it preserves_inf_of X;
end;

definition
 let S,T be Semilattice;
 cluster meet-preserving -> monotone map of S,T;
end;

definition
 let S be Semilattice, T be upper-bounded Semilattice;
 cluster -> meet-preserving SemilatticeHomomorphism of S,T;
end;

theorem :: WAYBEL21:1
   for S,T being upper-bounded Semilattice
 for f being SemilatticeHomomorphism of S,T
  holds f.Top S = Top T;

theorem :: WAYBEL21:2
 for S,T being Semilattice, f being map of S,T st f is meet-preserving
 for X being finite non empty Subset of S holds f preserves_inf_of X;

theorem :: WAYBEL21:3
   for S,T being upper-bounded Semilattice, f being meet-preserving map of S,T
  st f.Top S = Top T
  holds f is SemilatticeHomomorphism of S,T;

theorem :: WAYBEL21:4
 for S,T being Semilattice, f being map of S,T
  st f is meet-preserving &
     for X being filtered non empty Subset of S holds f preserves_inf_of X
 for X being non empty Subset of S holds f preserves_inf_of X;


theorem :: WAYBEL21:5
 for S,T being Semilattice, f being map of S,T st f is infs-preserving
  holds f is SemilatticeHomomorphism of S,T;

theorem :: WAYBEL21:6
 for S1,T1,S2,T2 being non empty RelStr
  st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
 for f1 being map of S1,T1, f2 being map of S2,T2 st f1 = f2 holds
  (f1 is infs-preserving implies f2 is infs-preserving) &
  (f1 is directed-sups-preserving implies f2 is directed-sups-preserving);

theorem :: WAYBEL21:7
   for S1,T1,S2,T2 being non empty RelStr
  st the RelStr of S1 = the RelStr of S2 & the RelStr of T1 = the RelStr of T2
 for f1 being map of S1,T1, f2 being map of S2,T2 st f1 = f2 holds
  (f1 is sups-preserving implies f2 is sups-preserving) &
  (f1 is filtered-infs-preserving implies f2 is filtered-infs-preserving);

theorem :: WAYBEL21:8
 for T being complete LATTICE
 for S being infs-inheriting full non empty SubRelStr of T
  holds incl(S,T) is infs-preserving;

theorem :: WAYBEL21:9
   for T being complete LATTICE
 for S being sups-inheriting full non empty SubRelStr of T
  holds incl(S,T) is sups-preserving;

theorem :: WAYBEL21:10
 for T being up-complete (non empty Poset)
 for S being directed-sups-inheriting full non empty SubRelStr of T
  holds incl(S,T) is directed-sups-preserving;

theorem :: WAYBEL21:11
   for T being complete LATTICE
 for S being filtered-infs-inheriting full non empty SubRelStr of T
  holds incl(S,T) is filtered-infs-preserving;

theorem :: WAYBEL21:12
 for T1,T2,R being RelStr, S being SubRelStr of T1
  st the RelStr of T1 = the RelStr of T2 & the RelStr of S = the RelStr of R
  holds R is SubRelStr of T2 &
    (S is full implies R is full SubRelStr of T2);

theorem :: WAYBEL21:13
 for T being non empty RelStr holds
  T is infs-inheriting sups-inheriting full SubRelStr of T;

definition
 let T be complete LATTICE;
 cluster complete CLSubFrame of T;
end;

theorem :: WAYBEL21:14
 for T being Semilattice
 for S being full non empty SubRelStr of T
  holds S is meet-inheriting iff
   for X being finite non empty Subset of S holds "/\"
(X, T) in the carrier of S;

theorem :: WAYBEL21:15
 for T being sup-Semilattice
 for S being full non empty SubRelStr of T
  holds S is join-inheriting iff
   for X being finite non empty Subset of S holds "\/"
(X, T) in the carrier of S;

theorem :: WAYBEL21:16
 for T being upper-bounded Semilattice
 for S being meet-inheriting full non empty SubRelStr of T
  st Top T in the carrier of S & S is filtered-infs-inheriting
  holds S is infs-inheriting;

theorem :: WAYBEL21:17
   for T being lower-bounded sup-Semilattice
 for S being join-inheriting full non empty SubRelStr of T
  st Bottom T in the carrier of S & S is directed-sups-inheriting
  holds S is sups-inheriting;

theorem :: WAYBEL21:18
 for T being complete LATTICE, S being full non empty SubRelStr of T
  st S is infs-inheriting
  holds S is complete;

theorem :: WAYBEL21:19
   for T being complete LATTICE, S being full non empty SubRelStr of T
  st S is sups-inheriting
  holds S is complete;

theorem :: WAYBEL21:20
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being non empty full SubRelStr of T2
  st the RelStr of T1 = the RelStr of T2 &
     the carrier of S1 = the carrier of S2
  holds S1 is infs-inheriting implies S2 is infs-inheriting;

theorem :: WAYBEL21:21
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being non empty full SubRelStr of T2
  st the RelStr of T1 = the RelStr of T2 &
     the carrier of S1 = the carrier of S2
  holds S1 is sups-inheriting implies S2 is sups-inheriting;

theorem :: WAYBEL21:22
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being non empty full SubRelStr of T2
  st the RelStr of T1 = the RelStr of T2 &
     the carrier of S1 = the carrier of S2
  holds S1 is directed-sups-inheriting implies S2 is directed-sups-inheriting;

theorem :: WAYBEL21:23
   for T1,T2 being non empty RelStr
 for S1 being non empty full SubRelStr of T1
 for S2 being non empty full SubRelStr of T2
  st the RelStr of T1 = the RelStr of T2 &
     the carrier of S1 = the carrier of S2
  holds S1 is filtered-infs-inheriting implies S2 is filtered-infs-inheriting;

begin :: Nets and limits

theorem :: WAYBEL21:24
 for S,T being non empty TopSpace, N being net of S
 for f being map of S,T st f is continuous
  holds f.:Lim N c= Lim (f*N);

definition
 let T be non empty RelStr;
 let N be non empty NetStr over T;
 redefine attr N is antitone means
:: WAYBEL21:def 2

  for i,j being Element of N st i <= j holds N.i >= N.j;
end;

definition
 let T be non empty reflexive RelStr;
 let x be Element of T;
 cluster {x} opp+id -> transitive directed monotone antitone;
end;

definition
 let T be non empty reflexive RelStr;
 cluster monotone antitone reflexive strict net of T;
end;

definition
 let T be non empty RelStr;
 let F be non empty Subset of T;
 cluster F opp+id -> antitone;
end;

definition
 let S,T be non empty reflexive RelStr;
 let f be monotone map of S,T;
 let N be antitone (non empty NetStr over S);
 cluster f*N -> antitone;
end;

theorem :: WAYBEL21:25
 for S being complete LATTICE, N be net of S holds
   {"/\"({N.i where i is Element of N:i >= j},S)
       where j is Element of N: not contradiction}
    is directed non empty Subset of S;

theorem :: WAYBEL21:26
   for S being non empty Poset, N be monotone reflexive net of S holds
   {"/\"({N.i where i is Element of N: i >= j}, S)
       where j is Element of N: not contradiction}
    is directed non empty Subset of S;

theorem :: WAYBEL21:27
 for S being non empty 1-sorted, N being non empty NetStr over S, X being set
  st rng the mapping of N c= X
  holds N is_eventually_in X;

theorem :: WAYBEL21:28
 for R being /\-complete (non empty Poset)
 for F being non empty filtered Subset of R
  holds lim_inf (F opp+id) = inf F;

theorem :: WAYBEL21:29
 for S,T being /\-complete (non empty Poset)
 for X being non empty filtered Subset of S
 for f being monotone map of S,T
  holds lim_inf (f*(X opp+id)) = inf (f.:X);

theorem :: WAYBEL21:30
 for S,T being non empty TopPoset
 for X being non empty filtered Subset of S
 for f being monotone map of S,T
 for Y being non empty filtered Subset of T
  st Y = f.:X
  holds f*(X opp+id) is subnet of Y opp+id;

theorem :: WAYBEL21:31
   for S,T being non empty TopPoset
 for X being non empty filtered Subset of S
 for f being monotone map of S,T
 for Y being non empty filtered Subset of T
  st Y = f.:X
  holds Lim (Y opp+id) c= Lim (f*(X opp+id));

theorem :: WAYBEL21:32
 for S being non empty reflexive RelStr, D being non empty Subset of S
  holds the mapping of Net-Str D = id D & the carrier of Net-Str D = D &
    Net-Str D is full SubRelStr of S;

theorem :: WAYBEL21:33
 for S,T being up-complete (non empty Poset)
 for f being monotone map of S,T
 for D being non empty directed Subset of S
  holds lim_inf (f*Net-Str D) = sup (f.:D);

theorem :: WAYBEL21:34
 for S being non empty reflexive RelStr
 for D being non empty directed Subset of S
 for i,j being Element of Net-Str D
  holds i <= j iff (Net-Str D).i <= (Net-Str D).j;

theorem :: WAYBEL21:35
 for T being Lawson (complete TopLattice)
 for D being directed non empty Subset of T
  holds sup D in Lim Net-Str D;

definition
 let T be non empty 1-sorted;
 let N be net of T, M be non empty NetStr over T such that
      M is subnet of N;
 mode Embedding of M,N -> map of M,N means
:: WAYBEL21:def 3

  the mapping of M = (the mapping of N)*it &
  for m being Element of N ex n being Element of M st
   for p being Element of M st n <= p holds m <= it.p;
end;

theorem :: WAYBEL21:36
 for T being non empty 1-sorted
 for N being net of T, M being non empty subnet of N
 for e being Embedding of M,N, i being Element of M
  holds M.i = N.(e.i);

theorem :: WAYBEL21:37
 for T being complete LATTICE
 for N being net of T, M being subnet of N
  holds lim_inf N <= lim_inf M;

theorem :: WAYBEL21:38
 for T being complete LATTICE
 for N being net of T, M being subnet of N
 for e being Embedding of M, N
  st for i being Element of N, j being Element of M st e.j <= i
       ex j' being Element of M st j' >= j & N.i >= M.j'
  holds lim_inf N = lim_inf M;

theorem :: WAYBEL21:39
   for T being non empty RelStr
 for N being net of T, M being non empty full SubNetStr of N
  st for i being Element of N
      ex j being Element of N st j >= i & j in the carrier of M
  holds M is subnet of N & incl(M,N) is Embedding of M,N;

theorem :: WAYBEL21:40
 for T being non empty RelStr, N being net of T
 for i being Element of N holds
   N|i is subnet of N & incl(N|i,N) is Embedding of N|i, N;

theorem :: WAYBEL21:41
 for T being complete LATTICE, N being net of T
 for i being Element of N holds lim_inf (N|i) = lim_inf N;

theorem :: WAYBEL21:42
 for T being non empty RelStr, N being net of T, X being set
  st N is_eventually_in X
 ex i be Element of N st N.i in X & rng the mapping of N|i c= X;

theorem :: WAYBEL21:43   :: see WAYBEL_2:18, for eventually-directed
 for T being Lawson (complete TopLattice)
 for N being eventually-filtered net of T
  holds rng the mapping of N is filtered non empty Subset of T;

theorem :: WAYBEL21:44
:: 1.7. LEMMA, -- WAYBEL19:44 revised
 for T being Lawson (complete TopLattice)
 for N being eventually-filtered net of T
  holds Lim N = {inf N};

begin :: Lawson topology revisited

theorem :: WAYBEL21:45
:: 1.8. THEOREM, (1) <=> (2), generalized, p. 145
 for S,T being Lawson (complete TopLattice)
 for f being meet-preserving map of S,T holds
   f is continuous iff f is directed-sups-preserving &
     for X being non empty Subset of S holds f preserves_inf_of X;

theorem :: WAYBEL21:46
:: 1.8. THEOREM, (1) <=> (2), p. 145
 for S,T being Lawson (complete TopLattice)
 for f being SemilatticeHomomorphism of S,T holds
   f is continuous iff f is infs-preserving directed-sups-preserving;

definition
 let S,T be non empty RelStr;
 let f be map of S,T;
 attr f is lim_infs-preserving means
:: WAYBEL21:def 4
     for N being net of S holds f.lim_inf N = lim_inf (f*N);
end;

theorem :: WAYBEL21:47
:: 1.8. THEOREM, (1) <=> (3), p. 145
   for S,T being Lawson (complete TopLattice)
 for f being SemilatticeHomomorphism of S,T holds
   f is continuous iff f is lim_infs-preserving;

theorem :: WAYBEL21:48
:: 1.11. THEOREM, (1) => (2a), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
  st Top T in the carrier of S &
     ex X being Subset of T st X = the carrier of S & X is closed
  holds S is infs-inheriting;

theorem :: WAYBEL21:49
:: 1.11. THEOREM, (1) => (2b), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being full non empty SubRelStr of T
  st ex X being Subset of T st X = the carrier of S & X is closed
  holds S is directed-sups-inheriting;

theorem :: WAYBEL21:50
:: 1.11. THEOREM, (2) => (1), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being infs-inheriting directed-sups-inheriting full non empty
             SubRelStr of T
 ex X being Subset of T st
    X = the carrier of S & X is closed;

theorem :: WAYBEL21:51
:: 1.11. THEOREM, (2) => (3+), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being infs-inheriting directed-sups-inheriting full non empty
             SubRelStr of T
 for N being net of T st N is_eventually_in the carrier of S
   holds lim_inf N in the carrier of S;

theorem :: WAYBEL21:52
:: 1.11. THEOREM, (3) => (2a), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
  st Top T in the carrier of S &
     for N being net of T st rng the mapping of N c= the carrier of S
      holds lim_inf N in the carrier of S
  holds S is infs-inheriting;

theorem :: WAYBEL21:53
:: 1.11. THEOREM, (3) => (2b), p. 147
 for T being Lawson (complete continuous TopLattice)
 for S being full non empty SubRelStr of T
  st for N being net of T st rng the mapping of N c= the carrier of S
      holds lim_inf N in the carrier of S
  holds S is directed-sups-inheriting;

theorem :: WAYBEL21:54
:: 1.11. THEOREM, (1) <=> (3+), p. 147
   for T being Lawson (complete continuous TopLattice)
 for S being meet-inheriting full non empty SubRelStr of T
 for X being Subset of T st X = the carrier of S & Top T in X
  holds
   X is closed iff
    for N being net of T st N is_eventually_in X holds lim_inf N in X;