:: 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;