:: The "Way-Below" Relation
:: by Grzegorz Bancerek
::
:: Received October 11, 1996
:: Copyright (c) 1996-2026 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;
definitions TARSKI, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_2, COMPTS_1, YELLOW_0,
WAYBEL_0, WAYBEL_2, XBOOLE_0, STRUCT_0, SETFAM_1;
equalities WAYBEL_0, SUBSET_1, STRUCT_0;
expansions TARSKI, ORDERS_2, LATTICE3, PRE_TOPC, TOPS_2, COMPTS_1, YELLOW_0,
WAYBEL_2;
theorems TARSKI, ORDERS_2, ZFMISC_1, NAT_1, RELAT_1, FUNCT_1, FINSET_1,
FUNCT_4, FUNCOP_1, CARD_3, PRALG_1, FUNCT_7, PRE_TOPC, TOPS_1, TOPS_2,
COMPTS_1, URYSOHN1, YELLOW_0, YELLOW_1, WAYBEL_0, YELLOW_2, YELLOW_4,
XBOOLE_0, XBOOLE_1, MONOID_0, ORDINAL1, SETFAM_1, PARTFUN1;
schemes NAT_1, FINSET_1, SUBSET_1, CLASSES1, PBOOLE, FUNCT_1;
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
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
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 Th1: :: 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
proof
let L be non empty reflexive antisymmetric RelStr;
let x,y be Element of L such that
A1: 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;
A2: {y} is directed by WAYBEL_0:5;
sup {y} = y by YELLOW_0:39;
then ex d being Element of L st ( d in {y})&( x <= d) by A1,A2;
hence thesis by TARSKI:def 1;
end;
theorem Th2: :: 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
proof
let L be non empty reflexive transitive RelStr;
let u,x,y,z be Element of L such that
A1: u <= x and
A2: 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 and
A3: y <= z;
let D be non empty directed Subset of L;
assume z <= sup D;
then y <= sup D by A3,ORDERS_2:3;
then consider d being Element of L such that
A4: d in D and
A5: x <= d by A2;
take d;
thus thesis by A1,A4,A5,ORDERS_2:3;
end;
theorem Th3: :: 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
proof
let L be non empty Poset such that
A1: L is with_suprema or L is /\-complete;
let x,y,z be Element of L;
assume
A2: z >> x;
then
A3: z >= x by Th1;
assume
A4: z >> y;
then
A5: z >= y by Th1;
thus
A6: now per cases by A1;
suppose L is with_suprema;
hence ex_sup_of {x,y},L by YELLOW_0:20;
end;
suppose
A7: L is /\-complete;
set X = {a where a is Element of L: a >= x & a >= y};
X c= the carrier of L
proof
let a be object;
assume a in X;
then ex z being Element of L st a = z & z >= x & z >= y;
hence thesis;
end;
then reconsider X as Subset of L;
z in X by A3,A5;
then ex_inf_of X,L by A7,WAYBEL_0:76;
then consider c being Element of L such that
A8: c is_<=_than X and
A9: for d being Element of L st d is_<=_than X holds d <= c;
A10: c is_>=_than {x,y}
proof
let a be Element of L;
assume
A11: a in {x,y};
a is_<=_than X
proof
let b be Element of L;
assume b in X;
then ex z being Element of L st b = z & z >= x & z >= y;
hence thesis by A11,TARSKI:def 2;
end;
hence thesis by A9;
end;
now
let a be Element of L;
assume
A12: a is_>=_than {x,y};
then
A13: a >= x by YELLOW_0:8;
a >= y by A12,YELLOW_0:8;
then a in X by A13;
hence c <= a by A8;
end;
hence ex_sup_of {x,y},L by A10,YELLOW_0:15;
end;
end;
let D be non empty directed Subset of L;
assume
A14: z <= sup D;
then consider d1 being Element of L such that
A15: d1 in D and
A16: x <= d1 by A2;
consider d2 being Element of L such that
A17: d2 in D and
A18: y <= d2 by A4,A14;
consider d being Element of L such that
A19: d in D and
A20: d1 <= d and
A21: d2 <= d by A15,A17,WAYBEL_0:def 1;
A22: x <= d by A16,A20,ORDERS_2:3;
A23: y <= d by A18,A21,ORDERS_2:3;
take d;
thus thesis by A6,A19,A22,A23,YELLOW_0:18;
end;
theorem Th4: :: 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
proof
let L be lower-bounded antisymmetric reflexive non empty RelStr;
let x be Element of L;
let D be non empty directed Subset of L;
assume x <= sup D;
set d = the Element of D;
reconsider d as Element of L;
take d;
thus thesis by YELLOW_0:44;
end;
theorem
for L being non empty Poset, x,y,z being Element of L
st x << y & y << z holds x << z
proof
let L be non empty Poset, x,y,z be Element of L;
assume x << y;
then x <= y by Th1;
hence thesis by Th2;
end;
theorem
for L being non empty reflexive antisymmetric RelStr, x,y being Element of L
st x << y & x >> y holds x = y
proof
let L be non empty reflexive antisymmetric RelStr, x,y be Element of L;
assume that
A1: x << y and
A2: x >> y;
A3: x <= y by A1,Th1;
y <= x by A2,Th1;
hence thesis by A3,ORDERS_2:2;
end;
definition :: after 1.2, p. 39
let L be non empty reflexive RelStr;
let x be Element of L;
A1: {y where y is Element of L: y << x} c= the carrier of L
proof
let z be object;
assume z in {y where y is Element of L: y << x};
then ex y being Element of L st z = y & y << x;
hence thesis;
end;
func waybelow x -> Subset of L equals
{y where y is Element of L: y << x};
correctness by A1;
A2: {y where y is Element of L: y >> x} c= the carrier of L
proof
let z be object;
assume z in {y where y is Element of L: y >> x};
then ex y being Element of L st z = y & y >> x;
hence thesis;
end;
func wayabove x -> Subset of L equals
{y where y is Element of L: y >> x};
correctness by A2;
end;
theorem Th7:
for L being non empty reflexive RelStr, x,y being Element of L holds
x in waybelow y iff x << y
proof
let L be non empty reflexive RelStr, x,y be Element of L;
x in waybelow y iff ex z being Element of L st x = z & z << y;
hence thesis;
end;
theorem Th8:
for L being non empty reflexive RelStr, x,y being Element of L holds
x in wayabove y iff x >> y
proof
let L be non empty reflexive RelStr, x,y be Element of L;
x in wayabove y iff ex z being Element of L st x = z & z >> y;
hence thesis;
end;
theorem Th9:
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_>=_than waybelow x
by Th7,Th1;
theorem
for L being non empty reflexive antisymmetric RelStr
for x being Element of L holds x is_<=_than wayabove x
by Th8,Th1;
theorem Th11:
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
proof
let L be non empty reflexive antisymmetric RelStr, x be Element of L;
hereby
let a be object;
assume a in waybelow x;
then consider y being Element of L such that
A1: a = y and
A2: y << x;
y <= x by A2,Th1;
hence a in downarrow x by A1,WAYBEL_0:17;
end;
let a be object;
assume a in wayabove x;
then consider y being Element of L such that
A3: a = y and
A4: y >> x;
x <= y by A4,Th1;
hence thesis by A3,WAYBEL_0:18;
end;
theorem Th12:
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
proof
let L be non empty reflexive transitive RelStr, x,y be Element of L;
assume
A1: x <= y;
hereby
let z be object;
assume z in waybelow x;
then consider v being Element of L such that
A2: z = v and
A3: v << x;
v << y by A1,A3,Th2;
hence z in waybelow y by A2;
end;
let z be object;
assume z in wayabove y;
then consider v being Element of L such that
A4: z = v and
A5: v >> y;
v >> x by A1,A5,Th2;
hence thesis by A4;
end;
registration
let L be lower-bounded non empty reflexive antisymmetric RelStr;
let x be Element of L;
cluster waybelow x -> non empty;
coherence
proof Bottom L << x by Th4;
hence thesis by Th7;
end;
end;
registration
let L be non empty reflexive transitive RelStr;
let x be Element of L;
cluster waybelow x -> lower;
coherence
proof
let z,y be Element of L;
assume z in waybelow x;
then z << x by Th7;
then y <= z implies y << x by Th2;
hence y <= z implies y in waybelow x;
end;
cluster wayabove x -> upper;
coherence
proof
hereby
let z,y be Element of L;
assume z in wayabove x;
then z >> x by Th8;
then y >= z implies y >> x by Th2;
hence y >= z implies y in wayabove x;
end;
end;
end;
registration
let L be sup-Semilattice;
let x be Element of L;
cluster waybelow x -> directed;
coherence
proof
let v,y be Element of L;
assume that
A1: v in waybelow x and
A2: y in waybelow x;
A3: v << x by A1,Th7;
A4: y << x by A2,Th7;
then
A5: ex_sup_of {v,y},L by A3,Th3;
take z = v"\/"y;
z << x by A3,A4,Th3;
hence z in waybelow x;
thus v <= z & y <= z by A5,YELLOW_0:18;
end;
end;
registration
let L be /\-complete non empty Poset;
let x be Element of L;
cluster waybelow x -> directed;
coherence
proof
let v,y be Element of L;
assume that
A1: v in waybelow x and
A2: y in waybelow x;
A3: v << x by A1,Th7;
A4: y << x by A2,Th7;
then
A5: ex_sup_of {v,y},L by A3,Th3;
take z = v"\/"y;
z << x by A3,A4,Th3;
hence z in waybelow x;
thus v <= z & y <= z by A5,YELLOW_0:18;
end;
end;
:: EXAMPLES, 1.3, p. 39
registration
let L be connected non empty RelStr;
cluster -> directed filtered for Subset of L;
coherence
proof
let X be Subset of L;
thus X is directed
proof
let x,y be Element of L;
x <= y & y <= y or x >= x & x >= y by WAYBEL_0:def 29;
hence thesis;
end;
let x,y be Element of L;
x >= y & y <= y or x >= x & x <= y by WAYBEL_0:def 29;
hence thesis;
end;
end;
registration
cluster up-complete lower-bounded -> complete for non empty Chain;
coherence
proof
let L be non empty Chain such that
A1: L is up-complete lower-bounded;
now
let X be Subset of L;
X = {} or X <> {};
hence ex_sup_of X,L by A1,WAYBEL_0:75,YELLOW_0:42;
end;
hence thesis by YELLOW_0:53;
end;
end;
registration
cluster complete for non empty Chain;
existence
proof set x = the set,O = the Order of {x};
RelStr(#{x},O#) is 1-element RelStr;
hence thesis;
end;
end;
theorem Th13:
for L being up-complete non empty Chain
for x,y being Element of L st x < y holds x << y
proof
let L be up-complete Chain, x,y be Element of L such that
A1: x <= y and
A2: x <> y;
let D be non empty directed Subset of L such that
A3: y <= sup D and
A4: for d being Element of L st d in D holds not x <= d;
A5: ex_sup_of D,L by WAYBEL_0:75;
x is_>=_than D
proof
let z be Element of L;
assume z in D;
then not x <= z by A4;
hence thesis by WAYBEL_0:def 29;
end;
then x >= sup D by A5,YELLOW_0:def 9;
then x >= y by A3,ORDERS_2:3;
hence contradiction by A1,A2,ORDERS_2:2;
end;
theorem
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
by Th1;
theorem
for L being non empty lower-bounded reflexive antisymmetric RelStr
holds Bottom L is compact
by Th4;
theorem Th16:
for L being up-complete non empty Poset
for D being non empty finite directed Subset of L holds sup D in D
proof
let L be up-complete non empty Poset;
let D be non empty finite directed Subset of L;
D c= D;
then consider d being Element of L such that
A1: d in D and
A2: d is_>=_than D by WAYBEL_0:1;
A3: ex_sup_of D,L by WAYBEL_0:75;
then
A4: sup D is_>=_than D by YELLOW_0:30;
A5: sup D <= d by A2,A3,YELLOW_0:30;
sup D >= d by A1,A4;
hence thesis by A1,A5,ORDERS_2:2;
end;
theorem
for L being up-complete non empty Poset st L is finite
for x being Element of L holds x is isolated_from_below
proof
let L be up-complete non empty Poset such that
A1: the carrier of L is finite;
let x be Element of L, D be non empty directed Subset of L;
assume x <= sup D;
hence thesis by A1,Th16;
end;
begin :: The Way-Below Relation in Other Terms
theorem Th18:
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
proof
let L be complete LATTICE, x,y be Element of L;
assume
A1: x << y;
let X be Subset of L;
assume
A2: y <= sup X;
defpred P[set] means
ex Y being finite Subset of X st ex_sup_of Y,L & $1 = "\/"(Y,L);
consider F being Subset of L such that
A3: for a being Element of L holds a in F iff P[a] from SUBSET_1:sch 3;
A4: for Y being finite Subset of X st Y <> {} holds "\/"(Y,L) in F
by A3,YELLOW_0:17;
A5: for Y being finite Subset of X st Y <> {} holds ex_sup_of Y,L
by YELLOW_0:17;
A6: {} c= X;
ex_sup_of {},L by YELLOW_0:17;
then "\/"({},L) in F by A3,A6;
then reconsider F as directed non empty Subset of L by A3,A4,A5,WAYBEL_0:51;
ex_sup_of X,L by YELLOW_0:17;
then sup X = sup F by A3,A4,A5,WAYBEL_0:54;
then consider d being Element of L such that
A7: d in F and
A8: x <= d by A1,A2;
consider Y being finite Subset of X such that
ex_sup_of Y,L and
A9: d = "\/"(Y,L) by A3,A7;
reconsider Y as finite Subset of L by XBOOLE_1:1;
take Y;
thus thesis by A8,A9;
end;
theorem
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
proof
let L be complete LATTICE, x,y be Element of L such that
A1: for X being Subset of L st y <= sup X
ex A being finite Subset of L st A c= X & x <= sup A;
let D be non empty directed Subset of L;
assume y <= sup D;
then consider A being finite Subset of L such that
A2: A c= D and
A3: x <= sup A by A1;
reconsider B = A as finite Subset of D by A2;
consider a being Element of L such that
A4: a in D and
A5: a is_>=_than B by WAYBEL_0:1;
take a;
a >= sup A by A5,YELLOW_0:32;
hence thesis by A3,A4,YELLOW_0:def 2;
end;
theorem
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
proof
let L be non empty reflexive transitive RelStr;
let x,y be Element of L;
assume
A1: x << y;
let I be Ideal of L;
assume y <= sup I;
then ex d being Element of L st d in I & x <= d by A1;
hence thesis by WAYBEL_0:def 19;
end;
theorem Th21:
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
proof
let L be up-complete non empty Poset;
let x,y be Element of L;
assume
A1: for I being Ideal of L st y <= sup I holds x in I;
let D be non empty directed Subset of L;
assume
A2: y <= sup D;
ex_sup_of D,L by WAYBEL_0:75;
then sup D = sup downarrow D by WAYBEL_0:33;
then x in downarrow D by A1,A2;
then ex d being Element of L st x <= d & d in D by WAYBEL_0:def 15;
hence thesis;
end;
theorem :: 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
proof
let L be lower-bounded LATTICE;
assume
A1: L is up-complete satisfying_MC;
let x,y be Element of L;
hereby
assume
A2: x << y;
let I be Ideal of L;
assume y = sup I;
then ex d being Element of L st d in I & x <= d by A2;
hence x in I by WAYBEL_0:def 19;
end;
assume
A3: for I being Ideal of L st y = sup I holds x in I;
now
let I be Ideal of L;
A4: ex_sup_of finsups ({y}"/\"I), L by A1,WAYBEL_0:75;
assume y <= sup I;
then y "/\" sup I = y by YELLOW_0:25;
then y = sup ({y} "/\" I) by A1
.= sup finsups ({y}"/\"I) by A1,WAYBEL_0:55
.= sup downarrow finsups ({y}"/\"I) by A4,WAYBEL_0:33;
then x in downarrow finsups ({y} "/\" I) by A3;
then consider z being Element of L such that
A5: x <= z and
A6: z in finsups ({y}"/\"I) by WAYBEL_0:def 15;
consider Y being finite Subset of {y}"/\"I such that
A7: z = "\/"(Y,L) and ex_sup_of Y, L by A6;
set i = the Element of I;
reconsider i as Element of L;
A8: ex_sup_of {i}, L by YELLOW_0:38;
A9: sup {i} = i by YELLOW_0:39;
ex_sup_of {},L by A1,YELLOW_0:17;
then "\/"({},L) <= sup {i} by A8,XBOOLE_1:2,YELLOW_0:34;
then
A10: "\/"({},L) in I by A9,WAYBEL_0:def 19;
Y c= I
proof
let a be object;
assume a in Y;
then a in {y}"/\"I;
then a in {y"/\"j where j is Element of L: j in I} by YELLOW_4:42;
then consider j being Element of L such that
A11: a = y"/\"j and
A12: j in I;
y"/\"j <= j by YELLOW_0:23;
hence thesis by A11,A12,WAYBEL_0:def 19;
end;
then z in I by A7,A10,WAYBEL_0:42;
hence x in I by A5,WAYBEL_0:def 19;
end;
hence thesis by A1,Th21;
end;
theorem
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
proof
let L be complete LATTICE;
hereby
assume
A1: for x being Element of L holds x is compact;
given Y being non empty Subset of L such that
A2: for x being Element of L st x in Y
ex y being Element of L st y in Y & x < y;
defpred P[object,object] means
[$1,$2] in the InternalRel of L & $1 <> $2;
A3: now
let x be object;
assume
A4: x in Y;
then reconsider y = x as Element of L;
consider z being Element of L such that
A5: z in Y and
A6: y < z by A2,A4;
reconsider u = z as object;
take u;
y <= z by A6;
hence u in Y & P[x,u] by A5,A6;
end;
consider f being Function such that
A7: dom f = Y & rng f c= Y &
for x being object st x in Y holds P[x,f.x] from FUNCT_1:sch 6(A3);
set x = the Element of Y;
set x1 = x;
set Z = the set of all iter(f,n).x where n is Element of NAT;
f.x in rng f by A7,FUNCT_1:def 3;
then f.x in Y by A7;
then reconsider x, x9 = f.x1 as Element of L;
A8: [x,f.x] in the InternalRel of L by A7;
A9: x <> f.x by A7;
A10: x9 = iter(f,1).x by FUNCT_7:70;
A11: x <= x9 by A8;
A12: x9 in Z by A10;
A13: x < x9 by A9,A11;
A14: Z c= Y
proof
let a be object;
assume a in Z;
then consider n being Element of NAT such that
A15: a = iter(f,n).x;
dom iter(f,n) = Y by A7,FUNCT_7:74;
then
A16: a in rng iter(f,n) by A15,FUNCT_1:def 3;
rng iter(f,n) c= Y by A7,FUNCT_7:74;
hence thesis by A16;
end;
then reconsider Z as Subset of L by XBOOLE_1:1;
A17: now
let i be Element of NAT;
defpred P[Nat] means ex z,y being Element of L st
z = iter(f,i).x & y = iter(f,i+$1).x & z <= y;
iter(f,i).x in Z;
then
A18: P[ 0 ];
A19: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
given z,y being Element of L such that
A20: z = iter(f,i).x and
A21: y = iter(f,i+k).x and
A22: z <= y;
take z;
A23: rng iter(f,i+k) c= Y by A7,FUNCT_7:74;
A24: dom iter(f,i+k) = Y by A7,FUNCT_7:74;
then
A25: y in rng iter(f,i+k) by A21,FUNCT_1:def 3;
then f.y in rng f by A7,A23,FUNCT_1:def 3;
then f.y in Y by A7;
then reconsider yy = f.y as Element of L;
take yy;
thus z = iter(f,i).x by A20;
iter(f,k+i+1) = f*iter(f,k+i) by FUNCT_7:71;
hence yy = iter(f,i+(k+1)).x by A21,A24,FUNCT_1:13;
[y,yy] in the InternalRel of L by A7,A23,A25;
then y <= yy;
hence thesis by A22,ORDERS_2:3;
end;
A26: for k being Nat holds P[k] from NAT_1:sch 2(A18,A19);
let k be Element of NAT;
assume i <= k;
then consider n being Nat such that
A27: k = i+n by NAT_1:10;
reconsider n as Element of NAT by ORDINAL1:def 12;
A28: ex z,y being Element of L st
z = iter(f,i).x & y = iter(f,i+n).x & z <= y by A26;
let z,y be Element of L;
assume that
A29: z = iter(f,i).x and
A30: y = iter(f,k).x;
thus z <= y by A27,A28,A29,A30;
end;
A31: now
let z,y be Element of L;
assume z in Z;
then consider k1 being Element of NAT such that
A32: z = iter(f,k1).x;
assume y in Z;
then consider k2 being Element of NAT such that
A33: y = iter(f,k2).x;
k1 <= k2 or k2 <= k1;
hence z <= y or z >= y by A17,A32,A33;
end;
sup Z is compact by A1;
then sup Z << sup Z;
then consider A being finite Subset of L such that
A34: A c= Z and
A35: sup Z <= sup A by Th18;
A36: now
assume A = {};
then x is_>=_than A;
then sup A <= x by YELLOW_0:32;
then
A37: sup A < x9 by A13,ORDERS_2:7;
A38: Z is_<=_than sup Z by YELLOW_0:32;
A39: sup Z < x9 by A35,A37,ORDERS_2:7;
x9 <= sup Z by A12,A38;
hence contradiction by A39,ORDERS_2:6;
end;
A40: A is finite;
defpred P[set] means $1 <> {} implies "\/"($1,L) in $1;
A41: P[{}];
A42: now
let x, B be set;
assume that
A43: x in A and
A44: B c= A;
reconsider x9 = x as Element of L by A43;
assume
A45: P[B];
thus P[B \/ {x}]
proof
assume B \/ {x} <> {};
A46: ex_sup_of B,L by YELLOW_0:17;
A47: ex_sup_of {x},L by YELLOW_0:17;
ex_sup_of B \/ {x},L by YELLOW_0:17;
then
A48: "\/"(B \/ {x}, L) = "\/"(B,L) "\/" "\/"({x},L) by A46,A47,YELLOW_0:36;
A49: sup {x9} = x by YELLOW_0:39;
per cases;
suppose B = {};
hence thesis by A49,TARSKI:def 1;
end;
suppose B <> {};
then "\/"(B,L) in A by A44,A45;
then x9 <= "\/"(B,L) or x9 >= "\/"(B,L) by A31,A34,A43;
then "\/"(B,L) "\/" x9 = "\/"(B,L) or
"\/"(B,L) "\/" x9 = x9 "\/" "\/"(B,L) & x9 "\/" "\/"(B,L) = x9
by YELLOW_0:24;
then "\/"(B \/ {x}, L) in B or "\/"
(B \/ {x}, L) in {x} by A45,A48,A49,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
end;
P[A] from FINSET_1:sch 2(A40,A41,A42);
then
A50: sup A in Z by A34,A36;
then consider n being Element of NAT such that
A51: sup A = iter(f,n).x;
A52: [sup A, f.sup A] in the InternalRel of L by A7,A14,A50;
A53: sup A <> f.sup A by A7,A14,A50;
reconsider xSn = f.sup A as Element of L by A52,ZFMISC_1:87;
A54: iter(f,n+1) = f*iter(f,n) by FUNCT_7:71;
A55: dom iter(f,n) = Y by A7,FUNCT_7:74;
A56: sup A <= xSn by A52;
A57: f.sup A = iter(f,n+1).x by A51,A54,A55,FUNCT_1:13;
A58: sup A < xSn by A53,A56;
A59: xSn in Z by A57;
Z is_<=_than sup Z by YELLOW_0:32;
then
A60: xSn <= sup Z by A59;
sup Z < xSn by A35,A58,ORDERS_2:7;
hence contradiction by A60,ORDERS_2:6;
end;
assume
A61: 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;
let x be Element of L;
let D be directed non empty Subset of L;
consider y being Element of L such that
A62: y in D and
A63: for z being Element of L st z in D holds not y < z by A61;
D is_<=_than y
proof
let a be Element of L;
assume a in D;
then consider b being Element of L such that
A64: b in D and
A65: a <= b and
A66: y <= b by A62,WAYBEL_0:def 1;
not y < b by A63,A64;
hence thesis by A65,A66;
end;
then
A67: sup D <= y by YELLOW_0:32;
sup D is_>=_than D by YELLOW_0:32;
then y <= sup D by A62;
then sup D = y by A67,ORDERS_2:2;
hence thesis by A62;
end;
begin :: Continuous Lattices
definition
let L be non empty reflexive RelStr;
attr L is satisfying_axiom_of_approximation means
:
Def5: for x being Element of L holds x = sup waybelow x;
end;
registration
cluster -> satisfying_axiom_of_approximation
for 1-element reflexive RelStr;
coherence
by ZFMISC_1:def 10;
end;
definition
let L be non empty reflexive RelStr;
attr L is continuous means
:
Def6: (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;
coherence;
cluster up-complete satisfying_axiom_of_approximation -> continuous
for lower-bounded sup-Semilattice;
coherence;
end;
registration
cluster continuous complete strict for LATTICE;
existence
proof set x = the set,R = the Order of {x};
RelStr(#{x},R#) is 1-element RelStr;
hence thesis;
end;
end;
registration
let L be continuous non empty reflexive RelStr;
let x be Element of L;
cluster waybelow x -> non empty directed;
coherence by Def6;
end;
theorem
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
proof
let L be up-complete Semilattice such that
A1: for x being Element of L holds waybelow x is non empty directed;
hereby
assume
A2: L is satisfying_axiom_of_approximation;
let x,y be Element of L;
assume
A3: not x <= y;
A4: waybelow x is non empty directed by A1;
A5: x = sup waybelow x by A2;
ex_sup_of waybelow x,L by A4,WAYBEL_0:75;
then y is_>=_than waybelow x implies y >= x by A5,YELLOW_0:def 9;
then consider u being Element of L such that
A6: u in waybelow x and
A7: not u <= y by A3;
take u;
thus u << x & not u <= y by A6,A7,Th7;
end;
assume
A8: for x,y being Element of L st not x <= y
ex u being Element of L st u << x & not u <= y;
let x be Element of L;
waybelow x is non empty directed by A1;
then
A9: ex_sup_of waybelow x,L by WAYBEL_0:75;
A10: x is_>=_than waybelow x by Th9;
now
let y be Element of L;
assume that
A11: y is_>=_than waybelow x and
A12: not x <= y;
consider u being Element of L such that
A13: u << x and
A14: not u <= y by A8,A12;
u in waybelow x by A13;
hence contradiction by A11,A14;
end;
hence thesis by A9,A10,YELLOW_0:def 9;
end;
theorem
for L being continuous LATTICE, x,y being Element of L
holds x <= y iff waybelow x c= waybelow y
proof
let L be continuous LATTICE, x,y be Element of L;
thus x <= y implies waybelow x c= waybelow y by Th12;
assume
A1: waybelow x c= waybelow y;
A2: ex_sup_of waybelow x,L by WAYBEL_0:75;
ex_sup_of waybelow y,L by WAYBEL_0:75;
then sup waybelow x <= sup waybelow y by A1,A2,YELLOW_0:34;
then x <= sup waybelow y by Def5;
hence thesis by Def5;
end;
registration
cluster complete -> satisfying_axiom_of_approximation for non empty Chain;
coherence
proof
let L be non empty Chain;
assume L is complete;
then reconsider S = L as complete non empty Chain;
S is satisfying_axiom_of_approximation
proof
let x be Element of S;
A1: ex_sup_of waybelow x,S by YELLOW_0:17;
A2: x is_>=_than waybelow x by Th9;
now
let y be Element of S;
assume that
A3: y is_>=_than waybelow x and
A4: not x <= y;
x >= y by A4,WAYBEL_0:def 29;
then x > y by A4;
then x >> y by Th13;
then y in waybelow x;
then for z being Element of S st z is_>=_than waybelow x holds z >= y;
then
A5: sup waybelow x = y by A1,A3,YELLOW_0:def 9;
x << x
proof
let D be non empty directed Subset of S;
assume
A6: x <= sup D;
assume
A7: for d being Element of S st d in D holds not x <= d;
A8: D c= waybelow x
proof
let a be object;
assume
A9: a in D;
then reconsider a as Element of S;
A10: not x <= a by A7,A9;
then a <= x by WAYBEL_0:def 29;
then a < x by A10;
then a << x by Th13;
hence thesis;
end;
ex_sup_of D,S by YELLOW_0:17;
then sup D <= sup waybelow x by A1,A8,YELLOW_0:34;
hence contradiction by A4,A5,A6,ORDERS_2:3;
end;
then x in waybelow x;
hence contradiction by A3,A4;
end;
hence thesis by A1,A2,YELLOW_0:def 9;
end;
hence thesis;
end;
end;
theorem
for L being complete LATTICE st for x being Element of L holds x is compact
holds L is satisfying_axiom_of_approximation
proof
let L be complete LATTICE such that
A1: for x being Element of L holds x is compact;
let x be Element of L;
x is compact by A1;
then x << x;
then
A2: x in waybelow x;
waybelow x is_<=_than sup waybelow x by YELLOW_0:32;
then
A3: x <= sup waybelow x by A2;
A4: ex_sup_of waybelow x, L by YELLOW_0:17;
A5: ex_sup_of downarrow x, L by WAYBEL_0:34;
sup downarrow x = x by WAYBEL_0:34;
then x >= sup waybelow x by A4,A5,Th11,YELLOW_0:34;
hence thesis by A3,ORDERS_2:2;
end;
begin :: The Way-Below Relation in Directed Powers
definition
let f be Relation;
attr f is non-Empty means
:Def7:
for S being 1-sorted st S in rng f holds S is non empty;
attr f is reflexive-yielding means
:Def8:
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;
existence
proof set R = the reflexive non empty RelStr;
set J = I --> R;
A1: rng J c= {R} by FUNCOP_1:13;
reconsider J as ManySortedSet of I;
take J;
thus J is RelStr-yielding;
thus J is non-Empty
by A1,TARSKI:def 1;
let S be RelStr;
assume S in rng J;
hence thesis by A1,TARSKI:def 1;
end;
end;
registration
let I be set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J -> non empty;
coherence
proof
A1: the carrier of product J = product Carrier J by YELLOW_1:def 4;
now
assume {} in rng Carrier J;
then consider i being object such that
A2: i in dom Carrier J and
A3: {} = (Carrier J).i by FUNCT_1:def 3;
A4: dom Carrier J = I by PARTFUN1:def 2;
A5: dom J = I by PARTFUN1:def 2;
consider R being 1-sorted such that
A6: R = J.i and
A7: {} = the carrier of R by A2,A3,A4,PRALG_1:def 15;
R in rng J by A2,A4,A5,A6,FUNCT_1:def 3;
then reconsider R as non empty RelStr by Def7,YELLOW_1:def 3;
the carrier of R = {} by A7;
hence contradiction;
end;
then the carrier of product J <> {} by A1,CARD_3:26;
hence thesis;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence thesis;
end;
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;
coherence
proof dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence thesis by Def7;
end;
end;
registration
let I be set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
cluster product J -> constituted-Functions;
coherence
proof
the carrier of product J = product Carrier J by YELLOW_1:def 4;
hence thesis by MONOID_0:80;
end;
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; :: redefines . (FUNCT_1, definition)
coherence
proof
A1: ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R
by PRALG_1:def 15;
A2: the carrier of product J = product Carrier J by YELLOW_1:def 4;
dom Carrier J = I by PARTFUN1:def 2;
hence thesis by A1,A2,CARD_3:9;
end;
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; :: redefines pi (CARD_3, definition)
coherence
proof
set Y = the carrier of product J;
A1: Y = product Carrier J by YELLOW_1:def 4;
A2: dom Carrier J = I by PARTFUN1:def 2;
X \/ Y = Y by XBOOLE_1:12;
then pi(Y,i) = pi(X,i) \/ pi(Y,i) by CARD_3:16;
then
A3: pi(X,i) c= pi(Y,i) by XBOOLE_1:7;
ex R being 1-sorted st R = J.i & (Carrier J).i = the carrier of R
by PRALG_1:def 15;
hence thesis by A1,A2,A3,CARD_3:12;
end;
end;
theorem Th27:
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
proof
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
let x be Function;
A1: the carrier of product J = product Carrier J by YELLOW_1:def 4;
A2: dom Carrier J = I by PARTFUN1:def 2;
hereby
assume
A3: x is Element of product J;
hence dom x = I by A1,A2,CARD_3:9;
let i be Element of I;
reconsider y = x as Element of product J by A3;
y.i is Element of J.i;
hence x.i is Element of J.i;
end;
assume that
A4: dom x = I and
A5: for i being Element of I holds x.i is Element of J.i;
now
let i be object;
assume i in dom Carrier J;
then reconsider j = i as Element of I by PARTFUN1:def 2;
A6: x.j is Element of J.j by A5;
ex R being 1-sorted st R = J.j & (Carrier J).j = the carrier of R by
PRALG_1:def 15;
hence x.i in (Carrier J).i by A6;
end;
hence thesis by A1,A2,A4,CARD_3:9;
end;
theorem Th28:
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
proof
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I;
set L = product J;
let x,y be Element of L;
A1: the carrier of L = product Carrier J by YELLOW_1:def 4;
hereby
assume
A2: x <= y;
let i be Element of I;
ex f,g being Function st f = x & g = y &
for i be object st i in I
ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = f.i & yi = g.i & xi <= yi by A1,A2,YELLOW_1:def 4;
then ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = x.i & yi = y.i & xi <= yi;
hence x.i <= y.i;
end;
assume
A3: for i being Element of I holds x.i <= y.i;
ex f,g being Function st f = x & g = y &
for i be object st i in I
ex R being RelStr, xi,yi being Element of R
st R = J.i & xi = f.i & yi = g.i & xi <= yi
proof
take f = x, g = y;
thus f = x & g = y;
let i be object;
assume i in I;
then reconsider j = i as Element of I;
take J.j, x.j, y.j;
thus thesis by A3;
end;
hence thesis by A1,YELLOW_1:def 4;
end;
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;
coherence
proof dom J = I by PARTFUN1:def 2;
then J.i in rng J by FUNCT_1:def 3;
hence thesis by Def8;
end;
end;
registration
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
cluster product J -> reflexive;
coherence
proof
thus product J is reflexive
proof
let x be Element of product J;
for i being Element of I holds x.i <= x.i;
hence thesis by Th28;
end;
end;
end;
theorem Th29:
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
proof
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is transitive;
let x,y,z be Element of product J such that
A2: x <= y and
A3: y <= z;
now
let i be Element of I;
A4: x.i <= y.i by A2,Th28;
A5: y.i <= z.i by A3,Th28;
J.i is transitive by A1;
hence x.i <= z.i by A4,A5;
end;
hence thesis by Th28;
end;
theorem Th30:
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
proof
let I be non empty set;
let J be RelStr-yielding non-Empty ManySortedSet of I such that
A1: for i being Element of I holds J.i is antisymmetric;
let x,y be Element of product J such that
A2: x <= y and
A3: y <= x;
A4: dom x = I by Th27;
A5: dom y = I by Th27;
now
let j be object;
assume j in I;
then reconsider i = j as Element of I;
A6: x.i <= y.i by A2,Th28;
A7: y.i <= x.i by A3,Th28;
J.i is antisymmetric by A1;
hence x.j = y.j by A6,A7;
end;
hence thesis by A4,A5,FUNCT_1:2;
end;
theorem Th31:
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
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is complete LATTICE;
then
A2: for i being Element of I holds J.i is transitive;
for i being Element of I holds J.i is antisymmetric by A1;
then reconsider L = product J as non empty Poset by A2,Th29,Th30;
now
let X be Subset of product J;
deffunc F(Element of I) = sup pi(X,$1);
consider f being ManySortedSet of I such that
A3: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A4: dom f = I by PARTFUN1:def 2;
now
let i be Element of I;
f.i = sup pi(X,i) by A3;
hence f.i is Element of J.i;
end;
then reconsider f as Element of product J by A4,Th27;
A5: f is_>=_than X
proof
let x be Element of product J such that
A6: x in X;
now
let i be Element of I;
A7: x.i in pi(X,i) by A6,CARD_3:def 6;
A8: J.i is complete LATTICE by A1;
f.i = sup pi(X,i) by A3;
hence x.i <= f.i by A7,A8,YELLOW_2:22;
end;
hence thesis by Th28;
end;
now
let g be Element of product J;
assume
A9: X is_<=_than g;
now
thus L = L;
let i be Element of I;
A10: f.i = sup pi(X,i) by A3;
A11: J.i is complete LATTICE by A1;
g.i is_>=_than pi(X,i)
proof
let a be Element of J.i;
assume a in pi(X,i);
then consider h being Function such that
A12: h in X and
A13: a = h.i by CARD_3:def 6;
reconsider h as Element of product J by A12;
h <= g by A9,A12;
hence a <= g.i by A13,Th28;
end;
hence f.i <= g.i by A10,A11,YELLOW_0:32;
end;
hence f <= g by Th28;
end;
then ex_sup_of X, L by A5,YELLOW_0:15;
hence ex_sup_of X, product J;
end;
then L is complete non empty Poset by YELLOW_0:53;
hence thesis;
end;
theorem Th32:
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)
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
assume
A1: for i being Element of I holds J.i is complete LATTICE;
then reconsider L = product J as complete LATTICE by Th31;
A2: L is complete;
let X be Subset of product J, i be Element of I;
A3: sup X is_>=_than X by A2,YELLOW_0:32;
A4: (sup X).i is_>=_than pi(X,i)
proof
let a be Element of J.i;
assume a in pi(X,i);
then consider f being Function such that
A5: f in X and
A6: a = f.i by CARD_3:def 6;
reconsider f as Element of product J by A5;
sup X >= f by A3,A5;
hence thesis by A6,Th28;
end;
A7: J.i is complete LATTICE by A1;
now
let a be Element of J.i;
assume
A8: a is_>=_than pi(X,i);
set f = (sup X)+*(i,a);
A9: dom f = dom sup X by FUNCT_7:30;
A10: dom sup X = I by Th27;
now
let j be Element of I;
j = i or j <> i;
then f.j = (sup X).j or f.j = a & j = i by A10,FUNCT_7:31,32;
hence f.j is Element of J.j;
end;
then reconsider f as Element of product J by A9,Th27;
f is_>=_than X
proof
let g be Element of product J;
assume
A11: g in X;
then
A12: g <= sup X by A2,YELLOW_2:22;
A13: g.i in pi(X,i) by A11,CARD_3:def 6;
now
let j be Element of I;
j = i or j <> i;
then f.j = (sup X).j or f.j = a & j = i by A10,FUNCT_7:31,32;
hence f.j >= g.j by A8,A12,A13,Th28;
end;
hence thesis by Th28;
end;
then
A14: f >= sup X by A2,YELLOW_0:32;
f.i = a by A10,FUNCT_7:31;
hence (sup X).i <= a by A14,Th28;
end;
hence thesis by A4,A7,YELLOW_0:32;
end;
theorem
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)
proof
let I be non empty set;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;
set L = product J;
assume
A1: for i being Element of I holds J.i is complete LATTICE;
then reconsider L9 = L as complete LATTICE by Th31;
let x,y be Element of L;
hereby
assume
A2: x << y;
hereby
let i be Element of I;
thus x.i << y.i
proof
let Di be non empty directed Subset of J.i such that
A3: y.i <= sup Di;
A4: dom y = I by Th27;
set D = {y+*(i,z) where z is Element of J.i: z in Di};
D c= the carrier of L
proof
let a be object;
assume a in D;
then consider z being Element of J.i such that
A5: a = y+*(i,z) and z in Di;
A6: dom (y+*(i,z)) = I by A4,FUNCT_7:30;
now
let j be Element of I;
i = j or i <> j;
then (y+*(i,z)).j = z & i = j or (y+*(i,z)).j = y.j by A4,
FUNCT_7:31,32;
hence (y+*(i,z)).j is Element of J.j;
end;
then a is Element of L by A5,A6,Th27;
hence thesis;
end;
then reconsider D as Subset of L;
set di = the Element of Di;
reconsider di as Element of J.i;
A7: y+*(i,di) in D;
A8: dom y = I by Th27;
reconsider D as non empty Subset of L by A7;
D is directed
proof
let z1,z2 be Element of L;
assume z1 in D;
then consider a1 being Element of J.i such that
A9: z1 = y+*(i,a1) and
A10: a1 in Di;
assume z2 in D;
then consider a2 being Element of J.i such that
A11: z2 = y+*(i,a2) and
A12: a2 in Di;
consider a being Element of J.i such that
A13: a in Di and
A14: a >= a1 and
A15: a >= a2 by A10,A12,WAYBEL_0:def 1;
y+*(i,a) in D by A13;
then reconsider z = y+*(i,a) as Element of L;
take z;
thus z in D by A13;
A16: dom y = I by Th27;
now
let j be Element of I;
i = j or i <> j;
then z.j = a & z1.j = a1 & i = j or z.j = y.j & z1.j = y.j
by A9,A16,FUNCT_7:31,32;
hence z.j >= z1.j by A14,YELLOW_0:def 1;
end;
hence z >= z1 by Th28;
now
let j be Element of I;
i = j or i <> j;
then z.j = a & z2.j = a2 & i = j or z.j = y.j & z2.j = y.j
by A11,A16,FUNCT_7:31,32;
hence z.j >= z2.j by A15,YELLOW_0:def 1;
end;
hence thesis by Th28;
end;
then reconsider D as non empty directed Subset of L;
now
let j be Element of I;
A17: J.i is complete LATTICE by A1;
A18: J.j is complete LATTICE by A1;
A19: ex_sup_of Di,J.i by A17,YELLOW_0:17;
A20: ex_sup_of pi(D,i),J.i by A17,YELLOW_0:17;
Di c= pi(D,i)
proof
let a be object;
assume
A21: a in Di;
then reconsider a as Element of J.i;
y+*(i,a) in D by A21;
then (y+*(i,a)).i in pi(D,i) by CARD_3:def 6;
hence thesis by A8,FUNCT_7:31;
end;
then
A22: sup Di <= sup pi(D,i) by A19,A20,YELLOW_0:34;
A23: (sup D).j = sup pi(D,j) by A1,Th32;
now
assume j <> i;
then (y+*(i,di)).j = y.j by FUNCT_7:32;
hence y.j in pi(D,j) by A7,CARD_3:def 6;
end;
hence (sup D).j >= y.j by A3,A18,A22,A23,YELLOW_0:def 2,YELLOW_2:22;
end;
then sup D >= y by Th28;
then consider d being Element of L such that
A24: d in D and
A25: d >= x by A2;
consider z being Element of J.i such that
A26: d = y+*(i,z) and
A27: z in Di by A24;
take z;
d.i = z by A4,A26,FUNCT_7:31;
hence thesis by A25,A27,Th28;
end;
end;
set K = {i where i is Element of I: x.i <> Bottom (J.i)};
K c= I
proof
let a be object;
assume a in K;
then ex i being Element of I st a = i & x.i <> Bottom (J.i);
hence thesis;
end;
then reconsider K as Subset of I;
deffunc F(Element of I) = Bottom (J.$1);
consider f being ManySortedSet of I such that
A28: for i being Element of I holds f.i = F(i) from PBOOLE:sch 5;
A29: dom f = I by PARTFUN1:def 2;
now
let i be Element of I;
f.i = Bottom (J.i) by A28;
hence f.i is Element of J.i;
end;
then reconsider f as Element of product J by A29,Th27;
set X = the set of all f+*(y|a) where a is finite Subset of I;
X c= the carrier of L
proof
let a be object;
assume a in X;
then consider b being finite Subset of I such that
A30: a = f+*(y|b);
dom y = I by Th27;
then
A31: dom (y|b) = b by RELAT_1:62;
then
A32: I = I \/ dom (y|b) by XBOOLE_1:12
.= dom (f+*(y|b)) by A29,FUNCT_4:def 1;
now
let i be Element of I;
(f+*(y|b)).i = f.i or (f+*(y|b)).i = (y|b).i & (y|b).i = y.i
by A31,FUNCT_1:47,FUNCT_4:11,13;
hence (f+*(y|b)).i is Element of J.i;
end;
then a is Element of L by A30,A32,Th27;
hence thesis;
end;
then reconsider X as Subset of L;
f+*(y|{}I) in X;
then reconsider X as non empty Subset of L;
X is directed
proof
let z1,z2 be Element of L;
assume z1 in X;
then consider a1 being finite Subset of I such that
A33: z1 = f+*(y|a1);
assume z2 in X;
then consider a2 being finite Subset of I such that
A34: z2 = f+*(y|a2);
reconsider a = a1 \/ a2 as finite Subset of I;
f+*(y|a) in X;
then reconsider z = f+*(y|a) as Element of L;
take z;
thus z in X;
A35: dom y = I by Th27;
then
A36: dom (y|a) = a by RELAT_1:62;
A37: dom (y|a1) = a1 by A35,RELAT_1:62;
A38: dom (y|a2) = a2 by A35,RELAT_1:62;
now
let i be Element of I;
J.i is complete LATTICE by A1;
then
A39: Bottom (J.i) <= y.i by YELLOW_0:44;
A40: f.i = Bottom (J.i) by A28;
per cases by XBOOLE_0:def 3;
suppose
A41: not i in a1 & i in a;
then
A42: z.i = (y|a).i by A36,FUNCT_4:13;
(y|a).i = y.i by A36,A41,FUNCT_1:47;
hence z.i >= z1.i by A33,A37,A39,A40,A41,A42,FUNCT_4:11;
end;
suppose
A43: not i in a & not i in a1;
then
A44: z.i = f.i by A36,FUNCT_4:11;
z1.i = f.i by A33,A37,A43,FUNCT_4:11;
hence z.i >= z1.i by A44,YELLOW_0:def 1;
end;
suppose
A45: i in a1 & i in a;
then
A46: z.i = (y|a).i by A36,FUNCT_4:13;
A47: (y|a).i = y.i by A36,A45,FUNCT_1:47;
A48: z1.i = (y|a1).i by A33,A37,A45,FUNCT_4:13;
(y|a1).i = y. i by A37,A45,FUNCT_1:47;
hence z.i >= z1.i by A46,A47,A48,YELLOW_0:def 1;
end;
end;
hence z >= z1 by Th28;
now
let i be Element of I;
J.i is complete LATTICE by A1;
then
A49: Bottom (J.i) <= y.i by YELLOW_0:44;
A50: f.i = Bottom (J.i) by A28;
per cases by XBOOLE_0:def 3;
suppose
A51: not i in a2 & i in a;
then
A52: z.i = (y|a).i by A36,FUNCT_4:13;
(y|a).i = y.i by A36,A51,FUNCT_1:47;
hence z.i >= z2.i by A34,A38,A49,A50,A51,A52,FUNCT_4:11;
end;
suppose
A53: not i in a & not i in a2;
then
A54: z.i = f.i by A36,FUNCT_4:11;
z2.i = f.i by A34,A38,A53,FUNCT_4:11;
hence z.i >= z2.i by A54,YELLOW_0:def 1;
end;
suppose
A55: i in a2 & i in a;
then
A56: z.i = (y|a).i by A36,FUNCT_4:13;
A57: (y|a).i = y.i by A36,A55,FUNCT_1:47;
A58: z2.i = (y|a2).i by A34,A38,A55,FUNCT_4:13;
(y|a2).i = y. i by A38,A55,FUNCT_1:47;
hence z.i >= z2.i by A56,A57,A58,YELLOW_0:def 1;
end;
end;
hence thesis by Th28;
end;
then reconsider X as non empty directed Subset of L;
now
let i be Element of I;
reconsider a = {i} as finite Subset of I;
A59: f+*(y|a) in X;
A60: L = L9;
reconsider z = f+*(y|a) as Element of L by A59;
A61: dom y = I by Th27;
A62: i in a by TARSKI:def 1;
then
A63: (y|a).i = y.i by FUNCT_1:49;
A64: dom (y|a) = a by A61,RELAT_1:62;
A65: z <= sup X by A59,A60,YELLOW_2:22;
z.i = y.i by A62,A63,A64,FUNCT_4:13;
hence (sup X).i >= y.i by A65,Th28;
end;
then y <= sup X by Th28;
then consider d being Element of L such that
A66: d in X and
A67: x <= d by A2;
consider a being finite Subset of I such that
A68: d = f+*(y|a) by A66;
K c= a
proof
let j be object;
assume j in K;
then consider i being Element of I such that
A69: j = i and
A70: x.i <> Bottom (J.i);
assume
A71: not j in a;
dom y = I by Th27;
then dom (y|a) = a by RELAT_1:62;
then
A72: d.i = f.i by A68,A69,A71,FUNCT_4:11
.= Bottom (J.i) by A28;
A73: J.i is complete LATTICE by A1;
A74: x.i <= d.i by A67,Th28;
x.i >= Bottom (J.i) by A73,YELLOW_0:44;
hence contradiction by A70,A72,A73,A74,ORDERS_2:2;
end;
then reconsider K as finite Subset of I;
take K;
thus for i be Element of I st not i in K &
x.i <> Bottom (J.i) holds contradiction;
end;
assume
A75: for i being Element of I holds x.i << y.i;
given K being finite Subset of I such that
A76: for i being Element of I st not i in K holds x.i = Bottom (J.i);
let D be non empty directed Subset of L such that
A77: y <= sup D;
defpred P[object,object] means
ex i being Element of I, z being Element of L st $1 = i & $2 = z &
z.i >= x.i;
A78: now
let k be object;
assume k in K;
then reconsider i = k as Element of I;
A79: pi(D,i) is directed
proof
let a,b be Element of J.i;
assume a in pi(D,i);
then consider f being Function such that
A80: f in D and
A81: a = f.i by CARD_3:def 6;
assume b in pi(D,i);
then consider g being Function such that
A82: g in D and
A83: b = g.i by CARD_3:def 6;
reconsider f,g as Element of L by A80,A82;
consider h being Element of L such that
A84: h in D and
A85: h >= f and
A86: h >= g by A80,A82,WAYBEL_0:def 1;
take h.i;
thus thesis by A81,A83,A84,A85,A86,Th28,CARD_3:def 6;
end;
set dd = the Element of D;
reconsider dd as Element of L;
A87: dd.i in pi(D,i) by CARD_3:def 6;
A88: x.i << y.i by A75;
A89: y.i <= (sup D).i by A77,Th28;
(sup D).i = sup pi(D,i) by A1,Th32;
then consider zi being Element of J.i such that
A90: zi in pi(D,i) and
A91: zi >= x.i by A79,A87,A88,A89;
consider a being Function such that
A92: a in D and
A93: zi = a.i by A90,CARD_3:def 6;
reconsider a as object;
take a;
thus a in D by A92;
thus P[k,a] by A91,A92,A93;
end;
consider F being Function such that
A94: dom F = K & rng F c= D and
A95: for k being object st k in K holds P[k,F.k] from FUNCT_1:sch 6(A78);
reconsider Y = rng F as finite Subset of D by A94,FINSET_1:8;
L = L9;
then consider d being Element of L such that
A96: d in D and
A97: d is_>=_than Y by WAYBEL_0:1;
take d;
thus d in D by A96;
now
let i be Element of I;
A98: J.i is complete LATTICE by A1;
per cases;
suppose
A99: i in K;
then consider j being Element of I, z being Element of L such that
A100: i = j and
A101: F.i = z and
A102: z.j >= x.j by A95;
z in Y by A94,A99,A101,FUNCT_1:def 3;
then d >= z by A97;
then d.i >= z.i by Th28;
hence d.i >= x.i by A98,A100,A102,YELLOW_0:def 2;
end;
suppose not i in K;
then x.i = Bottom (J.i) by A76;
hence d.i >= x.i by A98,YELLOW_0:44;
end;
end;
hence thesis by Th28;
end;
begin :: The Way-Below Relation in Topological Spaces
theorem Th34:
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
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
let x,y be Element of L such that
A1: x << y;
let F be Subset-Family of T;
assume that
A2: F is open and
A3: y c= union F;
reconsider A = F as Subset of L by A2,YELLOW_1:25;
sup A = union F by YELLOW_1:22;
then y <= sup A by A3,YELLOW_1:3;
then consider B being finite Subset of L such that
A4: B c= A and
A5: x <= sup B by A1,Th18;
reconsider G = B as finite Subset of F by A4;
take G;
sup B = union G by YELLOW_1:22;
hence thesis by A5,YELLOW_1:3;
end;
theorem Th35:
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
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
A1: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
let x,y be Element of L such that
A2: 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;
now
let I be Ideal of L;
reconsider F = I as Subset-Family of T by A1,XBOOLE_1:1;
assume y <= sup I;
then y c= sup I by YELLOW_1:3;
then
A3: y c= union F by YELLOW_1:22;
F is open by YELLOW_1:25;
then consider G being finite Subset of F such that
A4: x c= union G by A2,A3;
reconsider G as finite Subset of L by XBOOLE_1:1;
consider z being Element of L such that
A5: z in I and
A6: z is_>=_than G by WAYBEL_0:1;
A7: union G = sup G by YELLOW_1:22;
A8: z >= sup G by A6,YELLOW_0:32;
A9: x <= sup G by A4,A7,YELLOW_1:3;
sup G in I by A5,A8,WAYBEL_0:def 19;
hence x in I by A9,WAYBEL_0:def 19;
end;
hence thesis by Th21;
end;
theorem Th36:
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
proof
let T be non empty TopSpace;
let x be Element of InclPoset the topology of T, X be Subset of T such that
A1: x = X;
hereby
assume x is compact;
then
A2: x << x;
thus X is compact
proof
let F be Subset-Family of T such that
A3: X c= union F and
A4: F is open;
consider G being finite Subset of F such that
A5: x c= union G by A1,A2,A3,A4,Th34;
reconsider G as Subset-Family of T by XBOOLE_1:1;
take G;
thus G c= F & X c= union G & G is finite by A1,A5;
end;
end;
assume
A6: for F being Subset-Family of T st F is Cover of X & F is open
ex G being Subset-Family of T st G c= F & G is Cover of X & G is finite;
now
let F be Subset-Family of T;
assume that
A7: F is open and
A8: x c= union F;
F is Cover of X by A1,A8,SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A9: G c= F and
A10: G is Cover of X and
A11: G is finite by A6,A7;
x c= union G by A1,A10,SETFAM_1:def 11;
hence ex G being finite Subset of F st x c= union G by A9,A11;
end;
hence x << x by Th35;
end;
theorem
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
proof
let T be non empty TopSpace;
let x be Element of InclPoset the topology of T;
assume
A1: x = the carrier of T;
T is compact iff [#]T is compact;
hence thesis by A1,Th36;
end;
definition
let T be non empty TopSpace;
attr T is locally-compact means
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;
coherence
proof
let T be non empty TopSpace;
assume
A1: T is compact T_2;
hence
A2: T is regular & T is normal by COMPTS_1:12,13;
A3: [#]T is compact by A1;
let x be Point of T, X be Subset of T;
assume that
A4: x in X and
A5: X is open;
consider Y being open Subset of T such that
A6: x in Y and
A7: Cl Y c= X by A2,A4,A5,URYSOHN1:21;
take Z = Cl Y;
Y c= Int Z by PRE_TOPC:18,TOPS_1:24;
hence thesis by A3,A6,A7,COMPTS_1:9;
end;
end;
registration
cluster compact T_2 for non empty TopSpace;
existence
proof
take 1TopSp {0};
thus thesis;
end;
end;
theorem Th38:
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
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
let x,y be Element of L;
given Z be Subset of T such that
A1: x c= Z and
A2: Z c= y and
A3: Z is compact;
A4: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
then
A5: x in the topology of T;
y in the topology of T by A4;
then reconsider X = x, Y = y as Subset of T by A5;
let D be non empty directed Subset of L;
A6: sup D = union D by YELLOW_1:22;
reconsider F = D as Subset-Family of T by A4,XBOOLE_1:1;
reconsider F as Subset-Family of T;
A7: F is open
proof
let a be Subset of T;
assume a in F;
hence a in the topology of T by A4;
end;
assume y <= sup D;
then Y c= union F by A6,YELLOW_1:3;
then Z c= union F by A2;
then F is Cover of Z by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A8: G c= F and
A9: G is Cover of Z and
A10: G is finite by A3,A7;
consider d being Element of L such that
A11: d in D and
A12: d is_>=_than G by A8,A10,WAYBEL_0:1;
take d;
thus d in D by A11;
A13: now
let B be set;
assume
A14: B in G;
then B in D by A8;
then reconsider e = B as Element of L;
d >= e by A12,A14;
hence B c= d by YELLOW_1:3;
end;
A15: Z c= union G by A9,SETFAM_1:def 11;
union G c= d by A13,ZFMISC_1:76;
then Z c= d by A15;
then X c= d by A1;
hence thesis by YELLOW_1:3;
end;
theorem Th39:
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
proof
let T be non empty TopSpace such that
A1: 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;
set L = InclPoset the topology of T;
A2: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
let x,y be Element of L such that
A3: x << y;
A4: x in the topology of T by A2;
y in the topology of T by A2;
then reconsider X = x, Y = y as Subset of T by A4;
A5: Y is open by A2;
set VV = {Int Z where Z is Subset of T: Z c= Y & Z is compact};
reconsider e = {}T as Subset of T;
A6: {} c= Y;
Int {}T = {};
then
A7: e in VV by A6;
VV c= bool the carrier of T
proof
let a be object;
assume a in VV;
then ex Z being Subset of T st a = Int Z & Z c= Y & Z is compact;
hence thesis;
end;
then reconsider VV as non empty Subset-Family of T by A7;
set V = union VV;
VV is open
proof
let a be Subset of T;
assume a in VV;
then ex Z being Subset of T st a = Int Z & Z c= Y & Z is compact;
hence thesis;
end;
then reconsider A = VV as Subset of L by YELLOW_1:25;
A8: sup A = V by YELLOW_1:22;
Y c= V
proof
let a be object;
assume
A9: a in Y;
then reconsider a as Point of T;
consider Z being Subset of T such that
A10: a in Int Z and
A11: Z c= Y and
A12: Z is compact by A1,A5,A9;
Int Z in VV by A11,A12;
hence thesis by A10,TARSKI:def 4;
end;
then y <= sup A by A8,YELLOW_1:3;
then consider B being finite Subset of L such that
A13: B c= A and
A14: x <= sup B by A3,Th18;
defpred P[object,object] means
ex Z being Subset of T st $2 = Z & $1 = Int Z & Z c= Y & Z is compact;
A15: now
let z be object;
assume z in B;
then z in A by A13;
then consider Z being Subset of T such that
A16: z = Int Z and
A17: Z c= Y and
A18: Z is compact;
reconsider s = Z as object;
take s;
thus P[z,s] by A16,A17,A18;
end;
consider f being Function such that
A19: dom f = B and
A20: for z being object st z in B holds P[z, f.z] from CLASSES1:sch 1(A15);
reconsider W = B as Subset-Family of T by A2,XBOOLE_1:1;
sup B = union W by YELLOW_1:22;
then
A21: X c= union W by A14,YELLOW_1:3;
now
let z be set;
assume z in rng f;
then consider a being object such that
A22: a in B and
A23: z = f.a by A19,FUNCT_1:def 3;
ex Z being Subset of T st z = Z & a = Int Z & Z c= Y & Z is compact
by A20,A22,A23;
hence z c= the carrier of T;
end;
then reconsider Z = union rng f as Subset of T by ZFMISC_1:76;
take Z;
thus x c= Z
proof
let z be object;
assume z in x;
then consider a being set such that
A24: z in a and
A25: a in W by A21,TARSKI:def 4;
consider Z being Subset of T such that
A26: f.a = Z and
A27: a = Int Z and Z c= Y
and Z is compact by A20,A25;
A28: Int Z c= Z by TOPS_1:16;
Z in rng f by A19,A25,A26,FUNCT_1:def 3;
hence thesis by A24,A27,A28,TARSKI:def 4;
end;
thus Z c= y
proof
let z be object;
assume z in Z;
then consider a being set such that
A29: z in a and
A30: a in rng f by TARSKI:def 4;
consider Z being object such that
A31: Z in W and
A32: a = f.Z by A19,A30,FUNCT_1:def 3;
ex S being Subset of T st a = S & Z = Int S & S c= Y & S is compact
by A20,A31,A32;
hence thesis by A29;
end;
A33: rng f is finite by A19,FINSET_1:8;
defpred P[set] means ex A being Subset of T st A = union $1 & A is compact;
union {} = {}T by ZFMISC_1:2;
then
A34: P[{}];
A35: now
let x,B be set;
assume that
A36: x in rng f and B c= rng f;
assume P[B];
then consider A being Subset of T such that
A37: A = union B and
A38: A is compact;
thus P[B \/ {x}]
proof
consider Z being object such that
A39: Z in W and
A40: x = f.Z by A19,A36,FUNCT_1:def 3;
consider S being Subset of T such that
A41: x = S and Z = Int S
and S c= Y and
A42: S is compact by A20,A39,A40;
reconsider Bx = A \/ S as Subset of T;
take Bx;
thus Bx = union B \/ union {x} by A37,A41,ZFMISC_1:25
.= union (B \/ {x}) by ZFMISC_1:78;
thus thesis by A38,A42,COMPTS_1:10;
end;
end;
P[rng f] from FINSET_1:sch 2(A33,A34,A35);
hence thesis;
end;
theorem
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
proof
let T be non empty TopSpace such that
A1: T is locally-compact and
A2: T is T_2;
set L = InclPoset the topology of T;
A3: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
let x,y be Element of L;
assume x << y;
then consider Z being Subset of T such that
A4: x c= Z and
A5: Z c= y and
A6: Z is compact by A1,Th39;
x in the topology of T by A3;
then reconsider X = x as Subset of T;
take X;
thus X = x;
Cl X c= Z by A2,A4,A6,TOPS_1:5;
hence thesis by A5,A6,COMPTS_1:9;
end;
theorem
for X being non empty TopSpace st X is regular &
InclPoset the topology of X is continuous holds X is locally-compact
proof
let T be non empty TopSpace;
set L = InclPoset the topology of T;
A1: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
assume that
A2: T is regular and
A3: L is continuous;
let x be Point of T, X be Subset of T;
assume that
A4: x in X and
A5: X is open;
reconsider a = X as Element of L by A1,A5;
a = sup waybelow a by A3,Def5
.= union waybelow a by YELLOW_1:22;
then consider Y being set such that
A6: x in Y and
A7: Y in waybelow a by A4,TARSKI:def 4;
Y in the carrier of L by A7;
then reconsider Y as Subset of T by A1;
consider y being Element of L such that
A8: Y = y and
A9: y << a by A7;
Y is open by A1,A7;
then consider W being open Subset of T such that
A10: x in W and
A11: Cl W c= Y by A2,A6,URYSOHN1:21;
take Z = Cl W;
W c= Z by PRE_TOPC:18;
hence x in Int Z by A10,TOPS_1:22;
y <= a by A9,Th1;
then Y c= X by A8,YELLOW_1:3;
hence Z c= X by A11;
let F be Subset-Family of T such that
A12: F is Cover of Z and
A13: F is open;
reconsider ZZ = {Z`} as Subset-Family of T;
reconsider ZZ as Subset-Family of T;
reconsider FZ = F \/ ZZ as Subset-Family of T;
for x being Subset of T st x in ZZ holds x is open by TARSKI:def 1;
then ZZ is open;
then FZ is open by A13,TOPS_2:13;
then reconsider FF = FZ as Subset of L by YELLOW_1:25;
A14: sup FF = union FZ by YELLOW_1:22
.= union F \/ union ZZ by ZFMISC_1:78
.= union F \/ Z` by ZFMISC_1:25;
Z c= union F by A12,SETFAM_1:def 11;
then Z \/ Z` c= sup FF by A14,XBOOLE_1:9;
then [#]T c= sup FF by PRE_TOPC:2;
then X c= sup FF;
then a <= sup FF by YELLOW_1:3;
then consider A being finite Subset of L such that
A15: A c= FF and
A16: y <= sup A by A9,Th18;
A17: sup A = union A by YELLOW_1:22;
reconsider G = A \ ZZ as Subset-Family of T by A1,XBOOLE_1:1;
take G;
thus G c= F by A15,XBOOLE_1:43;
thus Z c= union G
proof
let z be object;
assume
A18: z in Z;
then
A19: z in Y by A11;
A20: Y c= union A by A8,A16,A17,YELLOW_1:3;
A21: not z in Z` by A18,XBOOLE_0:def 5;
consider B being set such that
A22: z in B and
A23: B in A by A19,A20,TARSKI:def 4;
not B in ZZ by A21,A22,TARSKI:def 1;
then B in G by A23,XBOOLE_0:def 5;
hence thesis by A22,TARSKI:def 4;
end;
thus thesis;
end;
theorem
for T being non empty TopSpace st T is locally-compact
holds InclPoset the topology of T is continuous
proof
let T be non empty TopSpace such that
A1: T is locally-compact;
set L = InclPoset the topology of T;
A2: L = RelStr(#the topology of T, RelIncl the topology of T#)
by YELLOW_1:def 1;
thus for x being Element of L holds waybelow x is non empty directed;
thus L is up-complete;
let x be Element of L;
x in the topology of T by A2;
then reconsider X = x as Subset of T;
thus x c= sup waybelow x
proof
let a be object;
assume
A3: a in x;
X is open by A2;
then consider Y being Subset of T such that
A4: a in Int Y and
A5: Y c= X and
A6: Y is compact by A1,A3;
reconsider iY = Int Y as Subset of T;
reconsider y = iY as Element of L by A2,PRE_TOPC:def 2;
y << x by A5,A6,Th38,TOPS_1:16;
then y in waybelow x;
then y c= union waybelow x by ZFMISC_1:74;
then y c= sup waybelow x by YELLOW_1:22;
hence thesis by A4;
end;
let a be object;
assume a in sup waybelow x;
then a in union waybelow x by YELLOW_1:22;
then consider Y being set such that
A7: a in Y and
A8: Y in waybelow x by TARSKI:def 4;
consider y being Element of L such that
A9: Y = y and
A10: y << x by A8;
y <= x by A10,Th1;
then Y c= x by A9,YELLOW_1:3;
hence thesis by A7;
end;