:: The "Way-Below" Relation :: by Grzegorz Bancerek :: :: Received October 11, 1996 :: Copyright (c) 1996-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, RELAT_2, ORDERS_2, SUBSET_1, WAYBEL_0, XXREAL_0, ORDINAL2, RCOMP_1, LATTICE3, YELLOW_0, EQREL_1, TARSKI, STRUCT_0, LATTICES, REWRITE1, TREES_2, ORDERS_1, ZFMISC_1, ARYTM_3, FINSET_1, CARD_FIL, WAYBEL_2, FUNCT_1, RELAT_1, FUNCT_7, NUMBERS, CARD_1, NAT_1, YELLOW_1, PBOOLE, FUNCOP_1, CARD_3, RLVECT_2, MONOID_0, FUNCT_4, PRE_TOPC, SETFAM_1, WELLORD2, TOPS_1, CARD_5, COMPTS_1, WAYBEL_3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FINSET_1, DOMAIN_1, ORDERS_1, SETFAM_1, STRUCT_0, FUNCT_1, FUNCT_4, PBOOLE, CARD_3, FUNCOP_1, PRALG_1, FUNCT_7, MONOID_0, ORDERS_2, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_4, WAYBEL_2, XXREAL_0; constructors SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, FUNCT_7, TOPS_1, TOPS_2, COMPTS_1, PCOMPS_1, MONOID_0, PRALG_1, YELLOW_1, YELLOW_4, WAYBEL_2, RELSET_1; registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, CARD_3, STRUCT_0, TOPS_1, COMPTS_1, ORDERS_2, LATTICE3, YELLOW_0, MONOID_0, WAYBEL_0, YELLOW_1, ORDINAL1, PRE_TOPC, FUNCT_7, NAT_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; end; notation :: 1.1, p. 38 let L be non empty reflexive RelStr; let x,y be Element of L; synonym x << y for x is_way_below y; synonym y >> x for x is_way_below y; 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; end; notation :: 1.1, p. 38 let L be non empty reflexive RelStr; let x be Element of L; synonym x is isolated_from_below for x is compact; 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; registration let L be lower-bounded non empty reflexive antisymmetric RelStr; let x be Element of L; cluster waybelow x -> non empty; end; registration let L be non empty reflexive transitive RelStr; let x be Element of L; cluster waybelow x -> lower; cluster wayabove x -> upper; end; registration let L be sup-Semilattice; let x be Element of L; cluster waybelow x -> directed; end; registration let L be /\-complete non empty Poset; let x be Element of L; cluster waybelow x -> directed; end; :: EXAMPLES, 1.3, p. 39 registration let L be connected non empty RelStr; cluster -> directed filtered for Subset of L; end; registration cluster up-complete lower-bounded -> complete for non empty Chain; end; registration cluster complete for 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 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; registration cluster -> satisfying_axiom_of_approximation for 1-element 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; registration cluster continuous -> up-complete satisfying_axiom_of_approximation for non empty reflexive RelStr; cluster up-complete satisfying_axiom_of_approximation -> continuous for lower-bounded sup-Semilattice; end; registration cluster continuous complete strict for LATTICE; end; registration 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; registration cluster complete -> satisfying_axiom_of_approximation for 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; registration let I be set; cluster RelStr-yielding non-Empty reflexive-yielding for ManySortedSet of I; end; registration 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 ManySortedSet of I; let i be Element of I; redefine func J.i -> RelStr; end; registration let I be non empty set; let J be RelStr-yielding non-Empty ManySortedSet of I; let i be Element of I; cluster J.i -> non empty for RelStr; end; registration let I be set; let J be RelStr-yielding non-Empty ManySortedSet of I; cluster product J -> constituted-Functions; 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; registration let I be non empty set; let J be RelStr-yielding reflexive-yielding ManySortedSet of I; let i be Element of I; cluster J.i -> reflexive for RelStr; end; registration let I be non empty set; let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; cluster product J -> reflexive; 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; registration cluster compact T_2 -> regular normal locally-compact for non empty TopSpace; end; registration cluster compact T_2 for non empty TopSpace; end; theorem :: WAYBEL_3:38 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:39 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:40 for T being non empty TopSpace st T is locally-compact & T is T_2 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:41 for X being non empty TopSpace st X is regular & InclPoset the topology of X is continuous holds X is locally-compact; theorem :: WAYBEL_3:42 for T being non empty TopSpace st T is locally-compact holds InclPoset the topology of T is continuous;