The abstract of the Mizar article:

The ``Way-Below'' Relation

by

Grzegorz Bancerek

Received October 11, 1996

MML identifier: WAYBEL_3

[ Mizar article, MML identifier index ]

environ

 vocabulary RELAT_2, ORDERS_1, QUANTAL1, ORDINAL2, COMPTS_1, LATTICE3,
      WAYBEL_0, YELLOW_0, LATTICES, BHSP_3, BOOLE, REALSET1, FINSET_1,
      FILTER_2, WAYBEL_2, FUNCT_1, RELAT_1, FUNCT_4, YELLOW_1, PBOOLE,
      FUNCOP_1, CARD_3, RLVECT_2, PRE_TOPC, SETFAM_1, TARSKI, WELLORD2,
      SUBSET_1, TOPS_1, PCOMPS_1, WAYBEL_3;
 notation TARSKI, XBOOLE_0, SUBSET_1, XREAL_0, NAT_1, RELAT_1, FINSET_1,
      DOMAIN_1, STRUCT_0, REALSET1, FUNCT_1, FUNCT_4, FUNCOP_1, PBOOLE, CARD_3,
      PRALG_1, FUNCT_7, GROUP_1, ORDERS_1, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1,
      PCOMPS_1, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_4, WAYBEL_2;
 constructors NAT_1, REALSET1, FUNCT_7, GROUP_1, DOMAIN_1, TOPS_1, TOPS_2,
      COMPTS_1, PCOMPS_1, YELLOW_4, WAYBEL_2, YELLOW_1, MEMBERED;
 clusters SUBSET_1, STRUCT_0, FUNCT_1, FINSET_1, ORDERS_1, LATTICE3, PCOMPS_1,
      CANTOR_1, YELLOW_0, WAYBEL_0, YELLOW_1, ARYTM_3, SETFAM_1, TOPS_1,
      MEMBERED, ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: 1. The "Way-Below" Relation

definition  :: 1.1, p. 38
 let L be non empty reflexive RelStr;
 let x,y be Element of L;
 pred x is_way_below y means
:: WAYBEL_3:def 1

  for D being non empty directed Subset of L st y <= sup D
   ex d being Element of L st d in D & x <= d;
 synonym x << y;
 synonym y >> x;
end;

definition  :: 1.1, p. 38
 let L be non empty reflexive RelStr;
 let x be Element of L;
 attr x is compact means
:: WAYBEL_3:def 2

  x is_way_below x;
 synonym x is isolated_from_below;
end;

theorem :: WAYBEL_3:1  :: 1.2(i), p. 39
 for L being non empty reflexive antisymmetric RelStr
 for x,y being Element of L st x << y holds x <= y;

theorem :: WAYBEL_3:2  :: 1.2(ii), p. 39
 for L being non empty reflexive transitive RelStr, u,x,y,z being Element of L
  st u <= x & x << y & y <= z holds u << z;

theorem :: WAYBEL_3:3  :: 1.2(iii), p. 39
 for L being non empty Poset st L is with_suprema or L is /\-complete
 for x,y,z being Element of L
  st x << z & y << z holds ex_sup_of {x,y}, L & x "\/" y << z;

theorem :: WAYBEL_3:4    :: 1.2(iv), p. 39
 for L being lower-bounded antisymmetric reflexive non empty RelStr
 for x being Element of L holds Bottom L << x;

theorem :: WAYBEL_3:5
   for L being non empty Poset, x,y,z being Element of L
  st x << y & y << z holds x << z;

theorem :: WAYBEL_3:6
   for L being non empty reflexive antisymmetric RelStr, x,y being Element of L
  st x << y & x >> y holds x = y;

definition  :: after 1.2, p. 39
 let L be non empty reflexive RelStr;
 let x be Element of L;
 func waybelow x -> Subset of L equals
:: WAYBEL_3:def 3

   {y where y is Element of L: y << x};
 func wayabove x -> Subset of L equals
:: WAYBEL_3:def 4

   {y where y is Element of L: y >> x};
end;

theorem :: WAYBEL_3:7
 for L being non empty reflexive RelStr, x,y being Element of L holds
  x in waybelow y iff x << y;

theorem :: WAYBEL_3:8
 for L being non empty reflexive RelStr, x,y being Element of L holds
  x in wayabove y iff x >> y;

theorem :: WAYBEL_3:9
 for L being non empty reflexive antisymmetric RelStr
 for x being Element of L holds x is_>=_than waybelow x;

theorem :: WAYBEL_3:10
   for L being non empty reflexive antisymmetric RelStr
 for x being Element of L holds x is_<=_than wayabove x;

theorem :: WAYBEL_3:11
 for L being non empty reflexive antisymmetric RelStr
 for x being Element of L holds
  waybelow x c= downarrow x & wayabove x c= uparrow x;

theorem :: WAYBEL_3:12
 for L being non empty reflexive transitive RelStr
 for x,y being Element of L st x <= y
  holds waybelow x c= waybelow y & wayabove y c= wayabove x;

definition
 let L be lower-bounded (non empty reflexive antisymmetric RelStr);
 let x be Element of L;
 cluster waybelow x -> non empty;
end;

definition
 let L be non empty reflexive transitive RelStr;
 let x be Element of L;
 cluster waybelow x -> lower;
 cluster wayabove x -> upper;
end;

definition
 let L be sup-Semilattice;
 let x be Element of L;
 cluster waybelow x -> directed;
end;

definition
 let L be /\-complete (non empty Poset);
 let x be Element of L;
 cluster waybelow x -> directed;
end;


:: EXAMPLES, 1.3, p. 39

definition
 let L be connected (non empty RelStr);
 cluster -> directed filtered Subset of L;
end;

definition
 cluster up-complete lower-bounded -> complete (non empty Chain);
end;

definition
 cluster complete (non empty Chain);
end;

theorem :: WAYBEL_3:13
 for L being up-complete (non empty Chain)
 for x,y being Element of L st x < y holds x << y;

theorem :: WAYBEL_3:14
   for L being non empty reflexive antisymmetric RelStr
 for x,y being Element of L st x is not compact & x << y
  holds x < y;

theorem :: WAYBEL_3:15
   for L being non empty lower-bounded reflexive antisymmetric RelStr
   holds Bottom L is compact;

theorem :: WAYBEL_3:16
 for L being up-complete (non empty Poset)
 for D being non empty finite directed Subset of L holds sup D in D;

theorem :: WAYBEL_3:17
   for L being up-complete (non empty Poset) st L is finite
 for x being Element of L holds x is isolated_from_below;

begin :: The Way-Below Relation in Other Terms

scheme SSubsetEx {S() -> non empty RelStr, P[set]}:
 ex X being Subset of S() st
  for x being Element of S() holds x in X iff P[x];

theorem :: WAYBEL_3:18
 for L being complete LATTICE, x,y being Element of L st x << y
  for X being Subset of L st y <= sup X
   ex A being finite Subset of L st A c= X & x <= sup A;

theorem :: WAYBEL_3:19
   for L being complete LATTICE, x,y being Element of L
  st for X being Subset of L st y <= sup X
    ex A being finite Subset of L st A c= X & x <= sup A
  holds x << y;

theorem :: WAYBEL_3:20
   for L being non empty reflexive transitive RelStr
 for x,y being Element of L st x << y
  for I being Ideal of L st y <= sup I holds x in I;

theorem :: WAYBEL_3:21
 for L being up-complete (non empty Poset), x,y being Element of L st
  for I being Ideal of L st y <= sup I holds x in I
 holds x << y;

theorem :: WAYBEL_3:22  :: Remark 1.5 (ii)
   for L being lower-bounded LATTICE st L is meet-continuous
 for x,y being Element of L holds
  x << y iff for I being Ideal of L st y = sup I holds x in I;

theorem :: WAYBEL_3:23
   for L being complete LATTICE holds
  (for x being Element of L holds x is compact)
 iff
  (for X being non empty Subset of L ex x being Element of L st x in X &
    for y being Element of L st y in X holds not x < y);

begin :: Continuous Lattices

definition
 let L be non empty reflexive RelStr;
 attr L is satisfying_axiom_of_approximation means
:: WAYBEL_3:def 5

  for x being Element of L holds x = sup waybelow x;
end;

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

definition
 let L be non empty reflexive RelStr;
 attr L is continuous means
:: WAYBEL_3:def 6

  (for x being Element of L holds waybelow x is non empty directed) &
  L is up-complete satisfying_axiom_of_approximation;
end;

definition
 cluster continuous -> up-complete satisfying_axiom_of_approximation
  (non empty reflexive RelStr);
 cluster up-complete satisfying_axiom_of_approximation -> continuous
  (lower-bounded sup-Semilattice);
end;

definition
 cluster continuous complete strict LATTICE;
end;

definition
 let L be continuous (non empty reflexive RelStr);
 let x be Element of L;
 cluster waybelow x -> non empty directed;
end;

theorem :: WAYBEL_3:24
   for L being up-complete Semilattice
  st for x being Element of L holds waybelow x is non empty directed
  holds
   L is satisfying_axiom_of_approximation
  iff
   for x,y being Element of L st not x <= y
    ex u being Element of L st u << x & not u <= y;

theorem :: WAYBEL_3:25
   for L being continuous LATTICE, x,y being Element of L
  holds x <= y iff waybelow x c= waybelow y;

definition
 cluster complete -> satisfying_axiom_of_approximation (non empty Chain);
end;

theorem :: WAYBEL_3:26
   for L being complete LATTICE st
  for x being Element of L holds x is compact
 holds L is satisfying_axiom_of_approximation;

begin :: The Way-Below Relation in Directed Powers

definition
 let f be Relation;
 attr f is non-Empty means
:: WAYBEL_3:def 7

  for S being 1-sorted st S in rng f holds S is non empty;
 attr f is reflexive-yielding means
:: WAYBEL_3:def 8

  for S being RelStr st S in rng f holds S is reflexive;
end;

definition
 let I be set;
 cluster RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
end;

definition
 let I be set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 cluster product J -> non empty;
end;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 let i be Element of I;
 redefine func J.i -> non empty RelStr;
end;

definition
 let I be set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 cluster -> Function-like Relation-like (Element of product J);
end;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 let x be Element of product J;
 let i be Element of I;
 redefine func x.i -> Element of J.i;
end;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty ManySortedSet of I;
 let i be Element of I;
 let X be Subset of product J;
 redefine func pi(X,i) -> Subset of J.i;
end;

theorem :: WAYBEL_3:27
 for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
 for x being Function holds
  x is Element of product J iff dom x = I &
    for i being Element of I holds x.i is Element of J.i;

theorem :: WAYBEL_3:28
 for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
 for x,y being Element of product J holds
   x <= y iff for i being Element of I holds x.i <= y.i;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
 cluster product J -> reflexive;
 let i be Element of I;
 redefine func J.i -> non empty reflexive RelStr;
end;

definition
 let I be non empty set;
 let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
 let x be Element of product J;
 let i be Element of I;
 redefine func x.i -> Element of J.i;
end;

theorem :: WAYBEL_3:29
 for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is transitive
 holds product J is transitive;

theorem :: WAYBEL_3:30
 for I being non empty set
 for J being RelStr-yielding non-Empty ManySortedSet of I
  st for i being Element of I holds J.i is antisymmetric
 holds product J is antisymmetric;

theorem :: WAYBEL_3:31
 for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  st for i being Element of I holds J.i is complete LATTICE
 holds product J is complete LATTICE;

theorem :: WAYBEL_3:32
 for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  st for i being Element of I holds J.i is complete LATTICE
 for X being Subset of product J, i being Element of I holds
   (sup X).i = sup pi(X,i);

theorem :: WAYBEL_3:33
   for I being non empty set
 for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I
  st for i being Element of I holds J.i is complete LATTICE
 for x,y being Element of product J holds
   x << y
  iff
   (for i being Element of I holds x.i << y.i) &
   (ex K being finite Subset of I st
      for i being Element of I st not i in K holds x.i = Bottom (J.i));

begin :: The Way-Below Relation in Topological Spaces

theorem :: WAYBEL_3:34
 for T being non empty TopSpace
 for x,y being Element of InclPoset the topology of T
  st x is_way_below y
 for F being Subset-Family of T st F is open & y c= union F
  ex G being finite Subset of F st x c= union G;

theorem :: WAYBEL_3:35
 for T being non empty TopSpace
 for x,y being Element of InclPoset the topology of T
  st for F being Subset-Family of T st F is open & y c= union F
       ex G being finite Subset of F st x c= union G
  holds x is_way_below y;

theorem :: WAYBEL_3:36
 for T being non empty TopSpace
 for x being Element of InclPoset the topology of T
 for X being Subset of T st x = X
 holds x is compact iff X is compact;

theorem :: WAYBEL_3:37
   for T being non empty TopSpace
 for x being Element of InclPoset the topology of T
  st x = the carrier of T
 holds x is compact iff T is compact;

definition
 let T be non empty TopSpace;
 attr T is locally-compact means
:: WAYBEL_3:def 9

  for x being Point of T, X being Subset of T st x in X & X is open
   ex Y being Subset of T st x in Int Y & Y c= X & Y is compact;
end;

definition
 cluster compact being_T2 -> being_T3 being_T4 locally-compact
   (non empty TopSpace);
end;

theorem :: WAYBEL_3:38
 for x being set holds 1TopSp {x} is being_T2;

definition
 cluster compact being_T2 (non empty TopSpace);
end;

theorem :: WAYBEL_3:39
 for T being non empty TopSpace
 for x,y being Element of InclPoset the topology of T
   st ex Z being Subset of T st x c= Z & Z c= y & Z is compact
   holds x << y;

theorem :: WAYBEL_3:40
 for T being non empty TopSpace st T is locally-compact
 for x,y being Element of InclPoset the topology of T st x << y
  ex Z being Subset of T st x c= Z & Z c= y & Z is compact;

theorem :: WAYBEL_3:41
   for T being non empty TopSpace st T is locally-compact & T is_T2
 for x,y being Element of InclPoset the topology of T st x << y
  ex Z being Subset of T st Z = x & Cl Z c= y & Cl Z is compact;

theorem :: WAYBEL_3:42
   for X being non empty TopSpace st X is_T3 &
   InclPoset the topology of X is continuous
  holds X is locally-compact;

theorem :: WAYBEL_3:43
   for T being non empty TopSpace st T is locally-compact
  holds InclPoset the topology of T is continuous;