The abstract of the Mizar article:

Meet -- Continuous Lattices

by

Artur Kornilowicz

Received October 10, 1996

MML identifier: WAYBEL_2

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, RELAT_2, LATTICE3, ORDERS_1, SUBSET_1, QUANTAL1,
      BOOLE, WAYBEL_0, YELLOW_0, LATTICES, ORDINAL2, FUNCT_5, TARSKI, MCART_1,
      PRE_TOPC, SEQM_3, REALSET1, BHSP_3, FINSET_1, WELLORD1, CAT_1, YELLOW_2,
      FINSUB_1, WELLORD2, YELLOW_1, FILTER_2, LATTICE2, WAYBEL_1, WAYBEL_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELSET_1, FINSUB_1, FUNCT_1,
      TOLER_1, FINSET_1, PARTFUN1, FUNCT_2, PRE_TOPC, STRUCT_0, REALSET1,
      ORDERS_1, ORDERS_3, LATTICE3, YELLOW_0, WAYBEL_0, YELLOW_1, YELLOW_2,
      WAYBEL_1, YELLOW_3, YELLOW_4;
 constructors FINSUB_1, ORDERS_3, YELLOW_3, YELLOW_4, WAYBEL_1, TOLER_1,
      MEMBERED, PRE_TOPC;
 clusters STRUCT_0, LATTICE3, FINSET_1, WAYBEL_0, YELLOW_0, YELLOW_2, YELLOW_3,
      YELLOW_4, WAYBEL_1, RELSET_1, FINSUB_1, SUBSET_1, RELAT_1, FUNCT_2,
      PARTFUN1;
 requirements SUBSET, BOOLE;


begin :: Preliminaries

definition let X, Y be non empty set,
               f be Function of X, Y,
               Z be non empty Subset of X;
 cluster f.:Z -> non empty;
end;

definition
 cluster reflexive connected -> with_infima with_suprema (non empty RelStr);
end;

definition let C be Chain;
 cluster [#]C -> directed;
end;

theorem :: WAYBEL_2:1
for L being up-complete Semilattice
 for D being non empty directed Subset of L, x being Element of L
  holds ex_sup_of {x} "/\" D,L;

theorem :: WAYBEL_2:2
  for L being up-complete sup-Semilattice
 for D being non empty directed Subset of L, x being Element of L
  holds ex_sup_of {x} "\/" D,L;

theorem :: WAYBEL_2:3
for L being up-complete sup-Semilattice
 for A, B being non empty directed Subset of L
  holds A is_<=_than sup (A "\/" B);

theorem :: WAYBEL_2:4
for L being up-complete sup-Semilattice
 for A, B being non empty directed Subset of L
  holds sup (A "\/" B) = sup A "\/" sup B;

theorem :: WAYBEL_2:5
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  { sup ({x} "/\" proj2 D) where x is Element of L : x in proj1 D }
    = { sup X where X is non empty directed Subset of L:
         ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D };

theorem :: WAYBEL_2:6
for L being Semilattice, D being non empty directed Subset of [:L,L:] holds
 union {X where X is non empty directed Subset of L:
  ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D}
   = proj1 D "/\" proj2 D;

theorem :: WAYBEL_2:7
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  ex_sup_of union {X where X is non empty directed Subset of L:
   ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L;

theorem :: WAYBEL_2:8
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  ex_sup_of {sup X where X is non empty directed Subset of L:
   ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L;

theorem :: WAYBEL_2:9
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  "\/" ({ sup X where X is non empty directed Subset of L:
   ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D },L)
    <= "\/" (union {X where X is non empty directed Subset of L:
     ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L);

theorem :: WAYBEL_2:10
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  "\/" ({ sup X where X is non empty directed Subset of L:
   ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L)
    = "\/" (union {X where X is non empty directed Subset of L:
     ex x being Element of L st X = {x} "/\" proj2 D & x in proj1 D},L);

definition let S, T be up-complete (non empty reflexive RelStr);
 cluster [:S,T:] -> up-complete;
end;

theorem :: WAYBEL_2:11
  for S, T being non empty reflexive antisymmetric RelStr
 st [:S,T:] is up-complete holds S is up-complete & T is up-complete;

theorem :: WAYBEL_2:12
for L being up-complete antisymmetric (non empty reflexive RelStr)
 for D being non empty directed Subset of [:L,L:]
  holds sup D = [sup proj1 D,sup proj2 D];

theorem :: WAYBEL_2:13
for S1, S2 being RelStr, D being Subset of S1
 for f being map of S1,S2 st f is monotone holds
  f.:(downarrow D) c= downarrow (f.:D);

theorem :: WAYBEL_2:14
for S1, S2 being RelStr, D being Subset of S1
 for f being map of S1,S2 st f is monotone holds
  f.:(uparrow D) c= uparrow (f.:D);

definition
 cluster trivial -> distributive complemented (non empty reflexive RelStr);
end;

definition
 cluster strict non empty trivial LATTICE;
end;

theorem :: WAYBEL_2:15
for H being distributive complete LATTICE
 for a being Element of H, X being finite Subset of H
  holds sup ({a} "/\" X) = a "/\" sup X;

theorem :: WAYBEL_2:16
  for H being distributive complete LATTICE
 for a being Element of H, X being finite Subset of H
  holds inf ({a} "\/" X) = a "\/" inf X;

theorem :: WAYBEL_2:17
for H being complete distributive LATTICE, a being Element of H
 for X being finite Subset of H holds a "/\" preserves_sup_of X;


begin :: The Properties of Nets

scheme ExNet { L() -> non empty RelStr,
               N() -> prenet of L(),
               F(set) -> Element of L()} :
 ex M being prenet of L() st the RelStr of M = the RelStr of N() &
  for i being Element of M holds
   (the mapping of M).i = F((the mapping of N()).i);

theorem :: WAYBEL_2:18
for L being non empty RelStr
 for N being prenet of L st N is eventually-directed
  holds rng netmap (N,L) is directed;

theorem :: WAYBEL_2:19
for L being non empty reflexive RelStr, D being non empty directed Subset of L
 for n being Function of D, the carrier of L holds
  NetStr (#D,(the InternalRel of L)|_2 D,n#) is prenet of L;

theorem :: WAYBEL_2:20
for L being non empty reflexive RelStr, D being non empty directed Subset of L
 for n being Function of D, the carrier of L, N being prenet of L st n = id D &
  N = NetStr (#D,(the InternalRel of L)|_2 D,n#) holds N is eventually-directed
;

definition let L be non empty RelStr,
               N be NetStr over L;
 func sup N -> Element of L equals
:: WAYBEL_2:def 1
   Sup the mapping of N;
end;

definition let L be non empty RelStr,
               J be set,
               f be Function of J,the carrier of L;
 func FinSups f -> prenet of L means
:: WAYBEL_2:def 2
  ex g being Function of Fin J, the carrier of L st
   for x being Element of Fin J holds g.x = sup (f.:x) &
    it = NetStr (# Fin J, RelIncl Fin J, g #);
end;

theorem :: WAYBEL_2:21
  for L being non empty RelStr, J, x being set
 for f being Function of J,the carrier of L holds
  x is Element of FinSups f iff x is Element of Fin J;

definition let L be complete antisymmetric (non empty reflexive RelStr),
               J be set,
               f be Function of J,the carrier of L;
 cluster FinSups f -> monotone;
end;

definition let L be non empty RelStr,
               x be Element of L,
               N be non empty NetStr over L;
 func x "/\" N -> strict NetStr over L means
:: WAYBEL_2:def 3
  the RelStr of it = the RelStr of N &
  for i being Element of it ex y being Element of L st
   y = (the mapping of N).i & (the mapping of it).i = x "/\" y;
end;

theorem :: WAYBEL_2:22
for L being non empty RelStr, N being non empty NetStr over L
 for x being Element of L, y being set holds
  y is Element of N iff y is Element of x "/\" N;

definition let L be non empty RelStr,
               x be Element of L,
               N be non empty NetStr over L;
 cluster x "/\" N -> non empty;
end;

definition let L be non empty RelStr,
               x be Element of L,
               N be prenet of L;
 cluster x "/\" N -> directed;
end;

theorem :: WAYBEL_2:23
for L being non empty RelStr, x being Element of L
 for F being non empty NetStr over L
  holds rng (the mapping of x "/\" F) = {x} "/\" rng the mapping of F;

theorem :: WAYBEL_2:24
for L being non empty RelStr, J being set
 for f being Function of J,the carrier of L
  st for x being set holds ex_sup_of f.:x,L
 holds rng netmap(FinSups f,L) c= finsups rng f;

theorem :: WAYBEL_2:25
for L being non empty reflexive antisymmetric RelStr, J being set
 for f being Function of J,the carrier of L
  holds rng f c= rng netmap (FinSups f,L);

theorem :: WAYBEL_2:26
for L being non empty reflexive antisymmetric RelStr, J being set
 for f being Function of J,the carrier of L st
  ex_sup_of rng f,L & ex_sup_of rng netmap (FinSups f,L),L &
   for x being Element of Fin J holds ex_sup_of f.:x,L
 holds Sup f = sup FinSups f;

theorem :: WAYBEL_2:27
for L being with_infima antisymmetric transitive RelStr, N being prenet of L
 for x being Element of L st N is eventually-directed
  holds x "/\" N is eventually-directed;

theorem :: WAYBEL_2:28
for L being up-complete Semilattice st
 for x being Element of L, E being non empty directed Subset of L
   st x <= sup E holds x <= sup ({x} "/\" E) holds
 for D being non empty directed Subset of L, x being Element of L
   holds x "/\" sup D = sup ({x} "/\" D);

theorem :: WAYBEL_2:29
  for L being with_suprema Poset st
 for X being directed Subset of L, x being Element of L
  holds x "/\" sup X = sup ({x} "/\" X) holds
 for X being Subset of L, x being Element of L st ex_sup_of X,L holds
  x "/\" sup X = sup ({x} "/\" finsups X);

theorem :: WAYBEL_2:30
  for L being up-complete LATTICE st
 for X being Subset of L, x being Element of L holds
  x "/\" sup X = sup ({x} "/\" finsups X) holds
 for X being non empty directed Subset of L, x being Element of L
  holds x "/\" sup X = sup ({x} "/\" X);


begin :: On the inf and sup operation

definition let L be non empty RelStr;
 func inf_op L -> map of [:L,L:], L means
:: WAYBEL_2:def 4
  for x, y being Element of L holds it.[x,y] = x "/\" y;
end;

theorem :: WAYBEL_2:31
for L being non empty RelStr, x being Element of [:L,L:] holds
 (inf_op L).x = x`1 "/\" x`2;

definition let L be with_infima transitive antisymmetric RelStr;
 cluster inf_op L -> monotone;
end;

theorem :: WAYBEL_2:32
for S being non empty RelStr, D1, D2 being Subset of S holds
 (inf_op S).:[:D1,D2:] = D1 "/\" D2;

theorem :: WAYBEL_2:33
for L being up-complete Semilattice
 for D being non empty directed Subset of [:L,L:] holds
  sup ((inf_op L).:D) = sup (proj1 D "/\" proj2 D);

definition let L be non empty RelStr;
 func sup_op L -> map of [:L,L:], L means
:: WAYBEL_2:def 5
  for x, y being Element of L holds it.[x,y] = x "\/" y;
end;

theorem :: WAYBEL_2:34
for L being non empty RelStr, x being Element of [:L,L:] holds
 (sup_op L).x = x`1 "\/" x`2;

definition let L be with_suprema transitive antisymmetric RelStr;
 cluster sup_op L -> monotone;
end;

theorem :: WAYBEL_2:35
for S being non empty RelStr, D1, D2 being Subset of S holds
 (sup_op S).:[:D1,D2:] = D1 "\/" D2;

theorem :: WAYBEL_2:36
  for L being complete (non empty Poset)
 for D being non empty filtered Subset of [:L,L:] holds
  inf ((sup_op L).:D) = inf (proj1 D "\/" proj2 D);


begin :: Meet-continuous lattices

:: Def 4.1, s.30
definition let R be non empty reflexive RelStr;
 attr R is satisfying_MC means
:: WAYBEL_2:def 6
  for x being Element of R, D being non empty directed Subset of R holds
    x "/\" sup D = sup ({x} "/\" D);
end;

definition let R be non empty reflexive RelStr;
 attr R is meet-continuous means
:: WAYBEL_2:def 7
  R is up-complete satisfying_MC;
end;

definition
 cluster trivial -> satisfying_MC (non empty reflexive RelStr);
end;

definition
 cluster meet-continuous ->
              up-complete satisfying_MC (non empty reflexive RelStr);
 cluster up-complete satisfying_MC ->
              meet-continuous (non empty reflexive RelStr);
end;

definition
 cluster strict non empty trivial LATTICE;
end;

theorem :: WAYBEL_2:37
for S being non empty reflexive RelStr st
 for X being Subset of S, x being Element of S holds
  x "/\" sup X = "\/"({x"/\"y where y is Element of S: y in X},S) holds
   S is satisfying_MC;

:: Th 4.2, s.30, 1 => 2
theorem :: WAYBEL_2:38
for L being up-complete Semilattice st SupMap L is meet-preserving holds
 for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2);

definition let L be up-complete sup-Semilattice;
 cluster SupMap L -> join-preserving;
end;

:: Th 4.2, s.30, 2 => 1
theorem :: WAYBEL_2:39
for L being up-complete Semilattice st
 for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
 I2) holds
  SupMap L is meet-preserving;

:: Th 4.2, s.30, 2 => 3
theorem :: WAYBEL_2:40
for L being up-complete Semilattice st
 for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\"
 I2) holds
  for D1, D2 be directed non empty Subset of L holds
   (sup D1) "/\" (sup D2) = sup (D1 "/\" D2);

:: Th 4.2, s.30, 4 => 7
theorem :: WAYBEL_2:41
for L being non empty reflexive RelStr st L is satisfying_MC holds
 for x being Element of L, N being non empty prenet of L st
  N is eventually-directed holds
 x "/\" sup N = sup ({x} "/\" rng netmap (N,L));

:: Th 4.2, s.30, 7 => 4
theorem :: WAYBEL_2:42
for L being non empty reflexive RelStr st
 for x being Element of L, N being prenet of L st N is eventually-directed
  holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds
 L is satisfying_MC;

:: Th 4.2, s.30, 6 => 3
theorem :: WAYBEL_2:43
for L being up-complete antisymmetric (non empty reflexive RelStr) st
 inf_op L is directed-sups-preserving holds
  for D1, D2 being non empty directed Subset of L holds
   (sup D1) "/\" (sup D2) = sup (D1 "/\" D2);

:: Th 4.2, s.30, 3 => 4
theorem :: WAYBEL_2:44
for L being non empty reflexive antisymmetric RelStr st
 for D1, D2 being non empty directed Subset of L
  holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)
 holds L is satisfying_MC;

:: Th 4.2, s.30, MC => 5
theorem :: WAYBEL_2:45
for L being satisfying_MC with_infima antisymmetric
 (non empty reflexive RelStr) holds
   for x being Element of L, D being non empty directed Subset of L
    st x <= sup D holds x = sup ({x} "/\" D);

:: Th 4.2, s.30, 5 => 6
theorem :: WAYBEL_2:46
for L being up-complete Semilattice st
 for x being Element of L, E being non empty directed Subset of L
   st x <= sup E holds x <= sup ({x} "/\" E) holds
  inf_op L is directed-sups-preserving;

:: Th 4.2, s.30, 7 => 8
theorem :: WAYBEL_2:47
for L being complete antisymmetric (non empty reflexive RelStr) st
 for x being Element of L, N being prenet of L st N is eventually-directed
  holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L)) holds
 for x being Element of L, J being set, f being Function of J,the carrier of L
  holds x "/\" Sup f = sup(x "/\" FinSups f);

:: Th 4.2, s.30, 8 => 7
theorem :: WAYBEL_2:48
for L being complete Semilattice st
 for x being Element of L, J being set, f being Function of J,the carrier of L
  holds x "/\" Sup f = sup (x "/\" FinSups f) holds
 for x being Element of L, N being prenet of L st N is eventually-directed
  holds x "/\" sup N = sup ({x} "/\" rng netmap (N,L));

:: Th 4.2, s.30, 4 <=> 1
theorem :: WAYBEL_2:49
for L being up-complete LATTICE
 holds L is meet-continuous iff
  SupMap L is meet-preserving join-preserving;

definition let L be meet-continuous LATTICE;
 cluster SupMap L -> meet-preserving join-preserving;
end;

:: Th 4.2, s.30, 4 <=> 2
theorem :: WAYBEL_2:50
for L being up-complete LATTICE
 holds L is meet-continuous iff
  for I1, I2 being Ideal of L holds (sup I1) "/\" (sup I2) = sup (I1 "/\" I2);

:: Th 4.2, s.30, 4 <=> 3
theorem :: WAYBEL_2:51
for L being up-complete LATTICE holds
 L is meet-continuous iff
  for D1, D2 being non empty directed Subset of L holds
   (sup D1) "/\" (sup D2) = sup (D1 "/\" D2);

:: Th 4.2, s.30, 4 <=> 5
theorem :: WAYBEL_2:52
  for L being up-complete LATTICE holds
 L is meet-continuous iff
  for x being Element of L, D being non empty directed Subset of L
   st x <= sup D holds x = sup ({x} "/\" D);

:: Th 4.2, s.30, 4 <=> 6
theorem :: WAYBEL_2:53
for L being up-complete Semilattice holds
 L is meet-continuous iff inf_op L is directed-sups-preserving;

definition let L be meet-continuous Semilattice;
 cluster inf_op L -> directed-sups-preserving;
end;

:: Th 4.2, s.30, 4 <=> 7
theorem :: WAYBEL_2:54
for L being up-complete Semilattice holds
 L is meet-continuous iff
  for x being Element of L, N being non empty prenet of L st
   N is eventually-directed holds
  x "/\" sup N = sup ({x} "/\" rng netmap (N,L));

:: Th 4.2, s.30, 4 <=> 8
theorem :: WAYBEL_2:55
  for L being complete Semilattice holds
 L is meet-continuous iff
  for x being Element of L, J being set
   for f being Function of J,the carrier of L
  holds x "/\" Sup f = sup(x "/\" FinSups f);

definition let L be meet-continuous Semilattice,
               x be Element of L;
 cluster x "/\" -> directed-sups-preserving;
end;

:: Remark 4.3 s.31
theorem :: WAYBEL_2:56
for H being complete (non empty Poset) holds
  H is Heyting iff H is meet-continuous distributive;

definition
 cluster complete Heyting -> meet-continuous distributive (non empty Poset);
 cluster complete meet-continuous distributive -> Heyting (non empty Poset);
end;