:: On the Baire Category Theorem
:: by Artur Korni{\l}owicz
::
:: Received February 5, 1997
:: Copyright (c) 1997-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, ORDERS_2, FUNCT_1, NUMBERS, STRUCT_0, SUBSET_1,
XXREAL_0, FINSET_1, TARSKI, CARD_1, FINSEQ_1, PRE_TOPC, RCOMP_1,
SETFAM_1, TOPS_1, CARD_3, ORDINAL1, RELAT_2, WAYBEL_0, YELLOW_0,
ORDINAL2, LATTICE3, LATTICES, EQREL_1, WAYBEL_6, WAYBEL_3, FINSUB_1,
CARD_FIL, MSAFREE, RELAT_1, ARYTM_3, YELLOW_8, ORDERS_1, ZFMISC_1,
XXREAL_2, YELLOW_1, TOPS_3, NAT_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS,
XCMPLX_0, NAT_1, SETFAM_1, FUNCT_1, RELSET_1, FINSEQ_1, FINSET_1,
FINSUB_1, DOMAIN_1, XXREAL_0, FUNCT_2, STRUCT_0, CARD_3, PRE_TOPC,
ORDERS_2, TOPS_1, TOPS_2, TOPS_3, LATTICE3, YELLOW_0, YELLOW_1, WAYBEL_0,
YELLOW_4, WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_8;
constructors SETFAM_1, DOMAIN_1, SETWISEO, XXREAL_0, NAT_1, NAT_D, TOPS_1,
TOPS_2, TOPS_3, WAYBEL_1, YELLOW_3, YELLOW_4, WAYBEL_3, WAYBEL_4,
WAYBEL_6, YELLOW_8, RELSET_1, FINSEQ_1;
registrations SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, FINSUB_1, XREAL_0,
CARD_1, FINSEQ_1, STRUCT_0, LATTICE3, YELLOW_0, PRE_TOPC, WAYBEL_0,
YELLOW_1, WAYBEL_1, YELLOW_4, WAYBEL_3, YELLOW_6, WAYBEL_6, WAYBEL_7,
YELLOW_8, SETWISEO, CARD_3, TOPS_1, RELAT_1;
requirements NUMERALS, BOOLE, SUBSET;
definitions TARSKI, WAYBEL_0, YELLOW_4, WAYBEL_6, YELLOW_8, CARD_3, LATTICE3,
XBOOLE_0;
equalities WAYBEL_0, YELLOW_4, XBOOLE_0, SUBSET_1, STRUCT_0;
expansions TARSKI, WAYBEL_0, PRE_TOPC, TOPS_2, YELLOW_4, WAYBEL_6, YELLOW_8,
LATTICE3, XBOOLE_0;
theorems CARD_1, FUNCT_2, LATTICE3, ORDERS_2, TARSKI, WAYBEL_0, WAYBEL_1,
WAYBEL_3, WAYBEL_4, WAYBEL_6, YELLOW_0, YELLOW_1, YELLOW_3, YELLOW_4,
ZFMISC_1, PRE_TOPC, WAYBEL_7, FUNCT_1, TOPS_1, TOPS_3, YELLOW_8,
MSSUBFAM, NAT_1, FINSEQ_1, FINSUB_1, RELAT_1, YELLOW_2, SETFAM_1,
XBOOLE_0, XBOOLE_1, SUBSET_1, CARD_3, ORDINAL1;
schemes FUNCT_2, TREES_2, SETWISEO, NAT_1, RECDEF_1;
begin :: Preliminaries
Lm1: for L being non empty RelStr, f being sequence of the carrier of L
for n being Element of NAT holds {f.k where k is Element of NAT: k <= n} is non
empty finite Subset of L
proof
let L be non empty RelStr, f be sequence of the carrier of L, n be
Element of NAT;
set A = {f.m where m is Element of NAT: m <= n};
A1: A c= {f.m where m is Element of NAT: m in {0} \/ Seg n}
proof
let q be object;
assume q in A;
then consider m being Element of NAT such that
A2: q = f.m and
A3: m <= n;
A4: m = 0 or m in Seg m by FINSEQ_1:3;
Seg m c= Seg n by A3,FINSEQ_1:5;
then m in {0} or m in Seg n by A4,TARSKI:def 1;
then m in {0} \/ Seg n by XBOOLE_0:def 3;
hence thesis by A2;
end;
deffunc F(set) = f.$1;
A5: A c= the carrier of L
proof
let q be object;
assume q in A;
then ex m being Element of NAT st q = f.m & m <= n;
hence thesis;
end;
card {F(m) where m is Element of NAT: m in {0} \/ Seg n} c= card ({0}
\/ Seg n) from TREES_2:sch 2;
then
A6: {f.m where m is Element of NAT: m in {0} \/ Seg n} is finite;
0 <= n by NAT_1:2;
then f.0 in A;
hence thesis by A1,A6,A5;
end;
definition
let T be TopStruct, P be Subset of T;
redefine attr P is closed means :: redefines closed (PRE_TOPC, definition)
P` is open;
compatibility;
end;
definition
let T be TopStruct, F be Subset-Family of T;
attr F is dense means
for X being Subset of T st X in F holds X is dense;
end;
theorem Th1:
for X, Y being set st card X c= card Y & Y is countable holds X is countable
proof
let X, Y be set such that
A1: card X c= card Y;
assume card Y c= omega;
hence card X c= omega by A1;
end;
theorem
for A being denumerable set holds NAT,A are_equipotent
proof
let A be denumerable set;
not card A in omega;
then
A1: omega c= card A by CARD_1:4;
card A c= omega by CARD_3:def 14;
then card NAT = card A by A1;
hence thesis by CARD_1:5;
end;
theorem
for L being non empty transitive RelStr, A, B being Subset of L st A
is_finer_than B holds downarrow A c= downarrow B
proof
let L be non empty transitive RelStr, A, B be Subset of L such that
A1: for a being Element of L st a in A ex b being Element of L st b in B
& b >= a;
let q be object;
assume
A2: q in downarrow A;
then reconsider q1 = q as Element of L;
consider a being Element of L such that
A3: a >= q1 and
A4: a in A by A2,WAYBEL_0:def 15;
consider b being Element of L such that
A5: b in B and
A6: b >= a by A1,A4;
b >= q1 by A3,A6,ORDERS_2:3;
hence thesis by A5,WAYBEL_0:def 15;
end;
theorem Th4:
for L being non empty transitive RelStr, A, B being Subset of L
st A is_coarser_than B holds uparrow A c= uparrow B
proof
let L be non empty transitive RelStr, A, B be Subset of L such that
A1: for a being Element of L st a in A ex b being Element of L st b in B
& b <= a;
let q be object;
assume
A2: q in uparrow A;
then reconsider q1 = q as Element of L;
consider a being Element of L such that
A3: a <= q1 and
A4: a in A by A2,WAYBEL_0:def 16;
consider b being Element of L such that
A5: b in B and
A6: b <= a by A1,A4;
b <= q1 by A3,A6,ORDERS_2:3;
hence thesis by A5,WAYBEL_0:def 16;
end;
theorem
for L being non empty Poset, D being non empty finite filtered Subset
of L st ex_inf_of D,L holds inf D in D
proof
let L be non empty Poset, D be non empty finite filtered Subset of L such
that
A1: ex_inf_of D,L;
D c= D;
then consider d being Element of L such that
A2: d in D and
A3: d is_<=_than D by WAYBEL_0:2;
A4: inf D >= d by A1,A3,YELLOW_0:31;
inf D is_<=_than D by A1,YELLOW_0:31;
then inf D <= d by A2;
hence thesis by A2,A4,ORDERS_2:2;
end;
theorem
for L being lower-bounded antisymmetric non empty RelStr for X being
non empty lower Subset of L holds Bottom L in X
proof
let L be lower-bounded antisymmetric non empty RelStr, X be non empty lower
Subset of L;
consider y being object such that
A1: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A1;
Bottom L <= y by YELLOW_0:44;
hence thesis by WAYBEL_0:def 19;
end;
theorem
for L being lower-bounded antisymmetric non empty RelStr for X being
non empty Subset of L holds Bottom L in downarrow X
proof
let L be lower-bounded antisymmetric non empty RelStr, X be non empty Subset
of L;
consider y being object such that
A1: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A1;
downarrow X = {x where x is Element of L: ex y being Element of L st x
<= y & y in X} & Bottom L <= y by WAYBEL_0:14,YELLOW_0:44;
hence thesis;
end;
theorem Th8:
for L being upper-bounded antisymmetric non empty RelStr for X
being non empty upper Subset of L holds Top L in X
proof
let L be upper-bounded antisymmetric non empty RelStr, X be non empty upper
Subset of L;
consider y being object such that
A1: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A1;
Top L >= y by YELLOW_0:45;
hence thesis by WAYBEL_0:def 20;
end;
theorem Th9:
for L being upper-bounded antisymmetric non empty RelStr for X
being non empty Subset of L holds Top L in uparrow X
proof
let L be upper-bounded antisymmetric non empty RelStr, X be non empty Subset
of L;
consider y being object such that
A1: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A1;
uparrow X = {x where x is Element of L: ex y being Element of L st x >=
y & y in X} & Top L >= y by WAYBEL_0:15,YELLOW_0:45;
hence thesis;
end;
theorem Th10:
for L being lower-bounded with_infima antisymmetric RelStr for X
being Subset of L holds X "/\" {Bottom L} c= {Bottom L}
proof
let L be lower-bounded with_infima antisymmetric RelStr, X be Subset of L;
A1: {Bottom L} "/\" X = {Bottom L "/\" y where y is Element of L: y in X} by
YELLOW_4:42;
let q be object;
assume q in X "/\" {Bottom L};
then consider y being Element of L such that
A2: q = Bottom L "/\" y and
y in X by A1;
y "/\" Bottom L = Bottom L by WAYBEL_1:3;
hence thesis by A2,TARSKI:def 1;
end;
theorem
for L being lower-bounded with_infima antisymmetric RelStr for X being
non empty Subset of L holds X "/\" {Bottom L} = {Bottom L}
proof
let L be lower-bounded with_infima antisymmetric RelStr, X be non empty
Subset of L;
thus X "/\" {Bottom L} c= {Bottom L} by Th10;
let q be object;
assume q in {Bottom L};
then
A1: X "/\" {Bottom L} = {Bottom L "/\" y where y is Element of L: y in X} &
q = Bottom L by TARSKI:def 1,YELLOW_4:42;
consider y being object such that
A2: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A2;
Bottom L "/\" y = Bottom L by WAYBEL_1:3;
hence thesis by A1;
end;
theorem Th12:
for L being upper-bounded with_suprema antisymmetric RelStr for
X being Subset of L holds X "\/" {Top L} c= {Top L}
proof
let L be upper-bounded with_suprema antisymmetric RelStr, X be Subset of L;
A1: {Top L} "\/" X = {Top L "\/" y where y is Element of L: y in X} by
YELLOW_4:15;
let q be object;
assume q in X "\/" {Top L};
then consider y being Element of L such that
A2: q = Top L "\/" y and
y in X by A1;
y "\/" Top L = Top L by WAYBEL_1:4;
hence thesis by A2,TARSKI:def 1;
end;
theorem
for L being upper-bounded with_suprema antisymmetric RelStr for X
being non empty Subset of L holds X "\/" {Top L} = {Top L}
proof
let L be upper-bounded with_suprema antisymmetric RelStr, X be non empty
Subset of L;
thus X "\/" {Top L} c= {Top L} by Th12;
let q be object;
assume q in {Top L};
then
A1: X "\/" {Top L} = {Top L "\/" y where y is Element of L: y in X} & q =
Top L by TARSKI:def 1,YELLOW_4:15;
consider y being object such that
A2: y in X by XBOOLE_0:def 1;
reconsider y as Element of X by A2;
Top L "\/" y = Top L by WAYBEL_1:4;
hence thesis by A1;
end;
theorem Th14:
for L being upper-bounded Semilattice, X being Subset of L holds
{Top L} "/\" X = X
proof
let L be upper-bounded Semilattice, X be Subset of L;
A1: {Top L} "/\" X = {Top L "/\" y where y is Element of L: y in X} by
YELLOW_4:42;
thus {Top L} "/\" X c= X
proof
let q be object;
assume q in {Top L} "/\" X;
then ex y being Element of L st q = Top L "/\" y & y in X by A1;
hence thesis by WAYBEL_1:4;
end;
let q be object;
assume
A2: q in X;
then reconsider X1 = X as non empty Subset of L;
reconsider y = q as Element of X1 by A2;
q = Top L "/\" y by WAYBEL_1:4;
hence thesis by A1;
end;
theorem
for L being lower-bounded with_suprema Poset, X being Subset of L
holds {Bottom L} "\/" X = X
proof
let L be lower-bounded with_suprema Poset, X be Subset of L;
A1: {Bottom L} "\/" X = {Bottom L "\/" y where y is Element of L: y in X} by
YELLOW_4:15;
thus {Bottom L} "\/" X c= X
proof
let q be object;
assume q in {Bottom L} "\/" X;
then ex y being Element of L st q = Bottom L "\/" y & y in X by A1;
hence thesis by WAYBEL_1:3;
end;
let q be object;
assume
A2: q in X;
then reconsider X1 = X as non empty Subset of L;
reconsider y = q as Element of X1 by A2;
q = Bottom L "\/" y by WAYBEL_1:3;
hence thesis by A1;
end;
theorem Th16:
for L being non empty reflexive RelStr, A, B being Subset of L
st A c= B holds A is_finer_than B & A is_coarser_than B
proof
let L be non empty reflexive RelStr, A, B be Subset of L such that
A1: A c= B;
thus A is_finer_than B
proof
let a be Element of L such that
A2: a in A;
take b = a;
thus b in B & a <= b by A1,A2;
end;
let a be Element of L such that
A3: a in A;
take b = a;
thus b in B & b <= a by A1,A3;
end;
theorem Th17:
for L being antisymmetric transitive with_infima RelStr for V
being Subset of L, x, y being Element of L st x <= y holds {y} "/\" V
is_coarser_than {x} "/\" V
proof
let L be antisymmetric transitive with_infima RelStr, V be Subset of L, x, y
be Element of L such that
A1: x <= y;
A2: {y} "/\" V = {y "/\" s where s is Element of L: s in V} by YELLOW_4:42;
let b be Element of L;
assume b in {y} "/\" V;
then consider s being Element of L such that
A3: b = y "/\" s and
A4: s in V by A2;
take a = x "/\" s;
{x} "/\" V = {x "/\" t where t is Element of L: t in V} by YELLOW_4:42;
hence a in {x} "/\" V by A4;
thus thesis by A1,A3,WAYBEL_1:1;
end;
theorem
for L being antisymmetric transitive with_suprema RelStr for V being
Subset of L, x, y being Element of L st x <= y holds {x} "\/" V is_finer_than {
y} "\/" V
proof
let L be antisymmetric transitive with_suprema RelStr, V be Subset of L, x,
y be Element of L such that
A1: x <= y;
A2: {x} "\/" V = {x "\/" s where s is Element of L: s in V} by YELLOW_4:15;
let b be Element of L;
assume b in {x} "\/" V;
then consider s being Element of L such that
A3: b = x "\/" s and
A4: s in V by A2;
take a = y "\/" s;
{y} "\/" V = {y "\/" t where t is Element of L: t in V} by YELLOW_4:15;
hence a in {y} "\/" V by A4;
thus thesis by A1,A3,WAYBEL_1:2;
end;
theorem Th19:
for L being non empty RelStr, V, S, T being Subset of L st S
is_coarser_than T & V is upper & T c= V holds S c= V
proof
let L be non empty RelStr, V, S, T be Subset of L such that
A1: S is_coarser_than T and
A2: V is upper & T c= V;
let q be object;
assume
A3: q in S;
then reconsider S1 = S as non empty Subset of L;
reconsider b = q as Element of S1 by A3;
ex a being Element of L st a in T & a <= b by A1;
hence thesis by A2;
end;
theorem
for L being non empty RelStr, V, S, T being Subset of L st S
is_finer_than T & V is lower & T c= V holds S c= V
proof
let L be non empty RelStr, V, S, T be Subset of L such that
A1: S is_finer_than T and
A2: V is lower & T c= V;
let q be object;
assume
A3: q in S;
then reconsider S1 = S as non empty Subset of L;
reconsider a = q as Element of S1 by A3;
ex b being Element of L st b in T & a <= b by A1;
hence thesis by A2;
end;
theorem Th21:
for L being Semilattice, F being upper filtered Subset of L
holds F "/\" F = F
proof
let L be Semilattice, F be upper filtered Subset of L;
thus F "/\" F c= F
proof
let x be object;
assume x in F "/\" F;
then consider y, z being Element of L such that
A1: x = y "/\" z and
A2: y in F & z in F;
consider t being Element of L such that
A3: t in F and
A4: t <= y & t <= z by A2,WAYBEL_0:def 2;
y "/\" z >= t by A4,YELLOW_0:23;
hence thesis by A1,A3,WAYBEL_0:def 20;
end;
thus thesis by YELLOW_4:40;
end;
theorem
for L being sup-Semilattice, I being lower directed Subset of L holds
I "\/" I = I
proof
let L be sup-Semilattice, I be lower directed Subset of L;
thus I "\/" I c= I
proof
let x be object;
assume x in I "\/" I;
then consider y, z being Element of L such that
A1: x = y "\/" z and
A2: y in I & z in I;
consider t being Element of L such that
A3: t in I and
A4: t >= y & t >= z by A2,WAYBEL_0:def 1;
y "\/" z <= t by A4,YELLOW_0:22;
hence thesis by A1,A3,WAYBEL_0:def 19;
end;
thus thesis by YELLOW_4:13;
end;
Lm2: for L being non empty RelStr, V being Subset of L holds {x where x is
Element of L : V "/\" {x} c= V} is Subset of L
proof
let L be non empty RelStr, V be Subset of L;
set G = {x where x is Element of L : V "/\" {x} c= V};
G c= the carrier of L
proof
let q be object;
assume q in G;
then ex x being Element of L st q = x & V "/\" {x} c= V;
hence thesis;
end;
hence thesis;
end;
theorem Th23:
for L being upper-bounded Semilattice, V being Subset of L holds
{x where x is Element of L : V "/\" {x} c= V} is non empty
proof
let L be upper-bounded Semilattice, V be Subset of L;
set G = {x where x is Element of L : V "/\" {x} c= V};
V "/\" {Top L} = V by Th14;
then Top L in G;
hence thesis;
end;
theorem Th24:
for L being antisymmetric transitive with_infima RelStr, V being
Subset of L holds {x where x is Element of L : V "/\" {x} c= V} is filtered
Subset of L
proof
let L be antisymmetric transitive with_infima RelStr, V be Subset of L;
reconsider G1 = {x where x is Element of L : V "/\" {x} c= V} as Subset of L
by Lm2;
G1 is filtered
proof
let x, y be Element of L;
assume x in G1;
then consider x1 being Element of L such that
A1: x = x1 and
A2: V "/\" {x1} c= V;
assume y in G1;
then consider y1 being Element of L such that
A3: y = y1 and
A4: V "/\" {y1} c= V;
take z = x1 "/\" y1;
V "/\" {z} c= V
proof
A5: {z} "/\" V = {z "/\" v where v is Element of L: v in V} by YELLOW_4:42;
let q be object;
assume q in V "/\" {z};
then consider v being Element of L such that
A6: q = z "/\" v and
A7: v in V by A5;
A8: {x1} "/\" V = {x1 "/\" s where s is Element of L: s in V} & q = x1
"/\" (y1 "/\" v) by A6,LATTICE3:16,YELLOW_4:42;
{y1} "/\" V = {y1 "/\" t where t is Element of L: t in V} by YELLOW_4:42;
then y1 "/\" v in V "/\" {y1} by A7;
then q in V "/\" {x1} by A4,A8;
hence thesis by A2;
end;
hence z in G1;
thus thesis by A1,A3,YELLOW_0:23;
end;
hence thesis;
end;
theorem Th25:
for L being antisymmetric transitive with_infima RelStr for V
being upper Subset of L holds {x where x is Element of L : V "/\" {x} c= V} is
upper Subset of L
proof
let L be antisymmetric transitive with_infima RelStr, V be upper Subset of L;
reconsider G1 = {x where x is Element of L : V "/\" {x} c= V} as Subset of L
by Lm2;
G1 is upper
proof
let x, y be Element of L;
assume x in G1;
then
A1: ex x1 being Element of L st x1 = x & V "/\" {x1} c= V;
assume x <= y;
then V "/\" {y} c= V by A1,Th17,Th19;
hence thesis;
end;
hence thesis;
end;
theorem Th26:
for L being with_infima Poset, X being Subset of L st X is Open
lower holds X is filtered
proof
let L be with_infima Poset, X be Subset of L such that
A1: X is Open lower;
let x, y be Element of L such that
A2: x in X and
y in X;
A3: x "/\" y <= x by YELLOW_0:23;
then x "/\" y in X by A1,A2;
then consider z being Element of L such that
A4: z in X and
A5: z << x "/\" y by A1;
take z;
x "/\" y <= y & z <= x "/\" y by A5,WAYBEL_3:1,YELLOW_0:23;
hence z in X & z <= x & z <= y by A3,A4,ORDERS_2:3;
end;
registration
let L be with_infima Poset;
cluster Open lower -> filtered for Subset of L;
coherence by Th26;
end;
registration
let L be continuous antisymmetric non empty reflexive RelStr;
cluster lower -> Open for Subset of L;
coherence
proof
let A be Subset of L such that
A1: A is lower;
let x be Element of L such that
A2: x in A;
consider y being object such that
A3: y in waybelow x by XBOOLE_0:def 1;
reconsider y as Element of L by A3;
take y;
y << x by A3,WAYBEL_3:7;
then y <= x by WAYBEL_3:1;
hence thesis by A1,A2,A3,WAYBEL_3:7;
end;
end;
registration
let L be continuous Semilattice, x be Element of L;
cluster (downarrow x)` -> Open;
coherence
proof
let a be Element of L;
set A = (downarrow x)`;
assume a in A;
then not a in downarrow x by XBOOLE_0:def 5;
then
A1: not a <= x by WAYBEL_0:17;
for x being Element of L holds waybelow x is non empty directed;
then consider y being Element of L such that
A2: y << a and
A3: not y <= x by A1,WAYBEL_3:24;
take y;
not y in downarrow x by A3,WAYBEL_0:17;
hence y in A by XBOOLE_0:def 5;
thus thesis by A2;
end;
end;
theorem Th27:
for L being Semilattice, C being non empty Subset of L st for x,
y being Element of L st x in C & y in C holds x <= y or y <= x for Y being non
empty finite Subset of C holds "/\"(Y,L) in Y
proof
let L be Semilattice, C be non empty Subset of L such that
A1: for x, y being Element of L st x in C & y in C holds x <= y or y <= x;
defpred P[set] means "/\"($1,L) in $1 & ex_inf_of $1,L;
A2: for B1, B2 being non empty Element of Fin C holds P[B1] & P[B2] implies
P[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin C such that
A3: ( P[B1])& P[B2];
B1 c= C & B2 c= C by FINSUB_1:def 5;
then "/\"(B1,L) <= "/\"(B2,L) or "/\"(B2,L) <= "/\"(B1,L) by A1,A3;
then
A4: "/\"(B1,L) "/\" "/\"(B2,L) = "/\"(B1,L) or "/\"(B1,L) "/\" "/\"(B2,L )
= "/\"(B2,L) by YELLOW_0:25;
"/\"(B1 \/ B2,L) = "/\"(B1, L) "/\" "/\"(B2, L) by A3,YELLOW_2:4;
hence thesis by A3,A4,XBOOLE_0:def 3,YELLOW_2:4;
end;
let Y be non empty finite Subset of C;
A5: Y in Fin C by FINSUB_1:def 5;
A6: for x being Element of C holds P[{x}]
proof
let x be Element of C;
"/\"({x},L) = x by YELLOW_0:39;
hence thesis by TARSKI:def 1,YELLOW_0:38;
end;
for B being non empty Element of Fin C holds P[B] from SETWISEO:sch 3(
A6,A2);
hence thesis by A5;
end;
theorem
for L being sup-Semilattice, C being non empty Subset of L st for x, y
being Element of L st x in C & y in C holds x <= y or y <= x for Y being non
empty finite Subset of C holds "\/"(Y,L) in Y
proof
let L be sup-Semilattice, C be non empty Subset of L such that
A1: for x, y being Element of L st x in C & y in C holds x <= y or y <= x;
defpred P[set] means "\/"($1,L) in $1 & ex_sup_of $1,L;
A2: for B1, B2 being non empty Element of Fin C holds P[B1] & P[B2] implies
P[B1 \/ B2]
proof
let B1, B2 be non empty Element of Fin C such that
A3: ( P[B1])& P[B2];
B1 c= C & B2 c= C by FINSUB_1:def 5;
then "\/"(B1,L) <= "\/"(B2,L) or "\/"(B2,L) <= "\/"(B1,L) by A1,A3;
then
A4: "\/"(B1,L) "\/" "\/"(B2,L) = "\/"(B1,L) or "\/"(B1,L) "\/" "\/"(B2,L )
= "\/"(B2,L) by YELLOW_0:24;
"\/"(B1 \/ B2,L) = "\/"(B1, L) "\/" "\/"(B2, L) by A3,YELLOW_2:3;
hence thesis by A3,A4,XBOOLE_0:def 3,YELLOW_2:3;
end;
let Y be non empty finite Subset of C;
A5: Y in Fin C by FINSUB_1:def 5;
A6: for x being Element of C holds P[{x}]
proof
let x be Element of C;
"\/"({x},L) = x by YELLOW_0:39;
hence thesis by TARSKI:def 1,YELLOW_0:38;
end;
for B being non empty Element of Fin C holds P[B] from SETWISEO:sch 3(
A6,A2);
hence thesis by A5;
end;
Lm3: for L being Semilattice, F being Filter of L holds F = uparrow fininfs F
by WAYBEL_0:62;
definition
let L be Semilattice, F be Filter of L;
mode GeneratorSet of F -> Subset of L means
:Def3:
F = uparrow fininfs it;
existence
proof
take F;
thus thesis by Lm3;
end;
end;
registration
let L be Semilattice, F be Filter of L;
cluster non empty for GeneratorSet of F;
existence
proof
F = uparrow fininfs F by Lm3;
then reconsider F1 = F as GeneratorSet of F by Def3;
take F1;
thus thesis;
end;
end;
Lm4: for L being Semilattice, F being Filter of L for G being GeneratorSet of
F holds G c= F
proof
let L be Semilattice, F be Filter of L, G be GeneratorSet of F;
F = uparrow fininfs G by Def3;
hence thesis by WAYBEL_0:62;
end;
theorem Th29:
for L being Semilattice, A being Subset of L for B being non
empty Subset of L st A is_coarser_than B holds fininfs A is_coarser_than
fininfs B
proof
let L be Semilattice, A be Subset of L, B be non empty Subset of L such that
A1: for a being Element of L st a in A ex b being Element of L st b in B
& b <= a;
defpred P[object,object] means
ex x, y being Element of L st x = $1 & y = $2 & y <= x;
let a be Element of L;
assume a in fininfs A;
then consider Y being finite Subset of A such that
A2: a = "/\"(Y,L) and
A3: ex_inf_of Y,L;
A4: for e being object st e in Y ex u being object st u in B & P[e,u]
proof
let e be object such that
A5: e in Y;
Y c= the carrier of L by XBOOLE_1:1;
then reconsider e as Element of L by A5;
ex b being Element of L st b in B & b <= e by A1,A5;
hence thesis;
end;
consider f being Function of Y, B such that
A6: for e being object st e in Y holds P[e,f.e] from FUNCT_2:sch 1(A4);
A7: f.:Y c= the carrier of L
proof
let y be object;
assume y in f.:Y;
then consider x being object such that
A8: x in dom f and
x in Y and
A9: y = f.x by FUNCT_1:def 6;
f.x in B by A8,FUNCT_2:5;
hence thesis by A9;
end;
A10: now
per cases;
case
Y = {};
hence ex_inf_of f.:Y,L by A3;
end;
case
Y <> {};
then consider e being object such that
A11: e in Y by XBOOLE_0:def 1;
dom f = Y by FUNCT_2:def 1;
then f.e in f.:Y by A11,FUNCT_1:def 6;
hence ex_inf_of f.:Y,L by A7,YELLOW_0:55;
end;
end;
"/\"(f.:Y,L) is_<=_than Y
proof
let e be Element of L;
assume
A12: e in Y;
then consider x, y being Element of L such that
A13: x = e and
A14: y = f.e and
A15: y <= x by A6;
dom f = Y by FUNCT_2:def 1;
then f.e in f.:Y by A12,FUNCT_1:def 6;
then "/\"(f.:Y,L) <= y by A10,A14,YELLOW_4:2;
hence "/\"(f.:Y,L) <= e by A13,A15,ORDERS_2:3;
end;
then
A16: "/\"(f.:Y,L) <= "/\"(Y,L) by A3,YELLOW_0:31;
"/\"(f.:Y,L) in fininfs B by A10;
hence ex b being Element of L st b in fininfs B & b <= a by A2,A16;
end;
theorem Th30:
for L being Semilattice, F being Filter of L, G being
GeneratorSet of F for A being non empty Subset of L st G is_coarser_than A & A
is_coarser_than F holds A is GeneratorSet of F
proof
let L be Semilattice, F be Filter of L, G be GeneratorSet of F, A be non
empty Subset of L such that
A1: G is_coarser_than A;
assume
A2: A is_coarser_than F;
F = uparrow fininfs G by Def3;
hence F c= uparrow fininfs A by A1,Th4,Th29;
A c= F by A2,YELLOW_4:8;
hence thesis by WAYBEL_0:62;
end;
theorem Th31:
for L being Semilattice, A being Subset of L for f, g being
sequence of the carrier of L st rng f = A & for n being Element of NAT
holds g.n = "/\"({f.m where m is Element of NAT: m <= n},L) holds A
is_coarser_than rng g
proof
let L be Semilattice, A be Subset of L, f, g be sequence of the carrier
of L such that
A1: rng f = A and
A2: for n being Element of NAT holds g.n = "/\"({f.m where m is Element
of NAT: m <= n},L);
let a be Element of L;
assume a in A;
then consider n being object such that
A3: n in dom f and
A4: f.n = a by A1,FUNCT_1:def 3;
reconsider n as Element of NAT by A3;
reconsider T = {f.m where m is Element of NAT: m <= n} as non empty finite
Subset of L by Lm1;
take b = "/\"(T,L);
dom g = NAT & g.n = b by A2,FUNCT_2:def 1;
hence b in rng g by FUNCT_1:def 3;
f.n in T;
then
A5: {f.n} c= T by ZFMISC_1:31;
ex_inf_of {f.n},L & ex_inf_of T,L by YELLOW_0:55;
then b <= "/\"({f.n},L) by A5,YELLOW_0:35;
hence b <= a by A4,YELLOW_0:39;
end;
theorem Th32:
for L being Semilattice, F being Filter of L, G being
GeneratorSet of F for f, g being sequence of the carrier of L st rng f = G
& for n being Element of NAT holds g.n = "/\"({f.m where m is Element of NAT: m
<= n},L) holds rng g is GeneratorSet of F
proof
let L be Semilattice, F be Filter of L, G be GeneratorSet of F, f, g be
sequence of the carrier of L such that
A1: rng f = G and
A2: for n being Element of NAT holds g.n = "/\"({f.m where m is Element
of NAT: m <= n},L);
A3: rng g is_coarser_than F
proof
let a be Element of L;
assume a in rng g;
then consider n being object such that
A4: n in dom g and
A5: g.n = a by FUNCT_1:def 3;
reconsider n as Element of NAT by A4;
reconsider Y = {f.m where m is Element of NAT: m <= n} as non empty finite
Subset of L by Lm1;
A6: Y c= G
proof
let q be object;
assume q in Y;
then
A7: ex m being Element of NAT st q = f.m & m <= n;
dom f = NAT by FUNCT_2:def 1;
hence thesis by A1,A7,FUNCT_1:def 3;
end;
G c= F by Lm4;
then Y c= F by A6;
then
A8: "/\"(Y,L) in F by WAYBEL_0:43;
g.n = "/\"(Y,L) by A2;
hence ex b being Element of L st b in F & b <= a by A5,A8;
end;
g.0 in rng g by FUNCT_2:4;
hence thesis by A1,A2,A3,Th30,Th31;
end;
begin :: On the Baire Category Theorem
:: Proposition 3.43.1
theorem Th33:
for L being lower-bounded continuous LATTICE, V being Open upper
Subset of L for F being Filter of L, v being Element of L st V "/\" F c= V & v
in V & ex A being non empty GeneratorSet of F st A is countable ex O being Open
Filter of L st O c= V & v in O & F c= O
proof
let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, F be
Filter of L, v be Element of L such that
A1: V "/\" F c= V and
A2: v in V;
reconsider V1 = V as non empty Open upper Subset of L by A2;
reconsider v1 = v as Element of V1 by A2;
reconsider G = {x where x is Element of L : V "/\" {x} c= V} as Filter of L
by Th23,Th24,Th25;
given A being non empty GeneratorSet of F such that
A3: A is countable;
consider f being sequence of A such that
A4: rng f = A by A3,CARD_3:96;
reconsider f as sequence of the carrier of L by FUNCT_2:7;
deffunc F(Element of NAT) = "/\"({f.m where m is Element of NAT: m <= $1},L);
consider g being sequence of the carrier of L such that
A5: for n being Element of NAT holds g.n = F(n) from FUNCT_2:sch 4;
defpred P[Nat,set,set] means ex x1, y1 being Element of V1, z1
being Element of L st x1 = $2 & y1 = $3 & z1 = g.($1+1) & y1 << x1 "/\" z1;
A6: dom g = NAT by FUNCT_2:def 1;
then reconsider AA = rng g as non empty Subset of L by RELAT_1:42;
A7: AA is GeneratorSet of F by A4,A5,Th32;
A8: F c= G
proof
let q be object;
assume
A9: q in F;
then reconsider s = q as Element of L;
A10: V "/\" {s} = {s "/\" t where t is Element of L : t in V} by YELLOW_4:42;
V "/\" {s} c= V
proof
let w be object;
assume w in V "/\" {s};
then consider t being Element of L such that
A11: w = s "/\" t and
A12: t in V by A10;
t "/\" s in V "/\" F by A9,A12;
hence thesis by A1,A11;
end;
hence thesis;
end;
A13: for n being Nat, x being Element of V1 ex y being Element of
V1 st P[n,x,y]
proof
let n be Nat, x be Element of V1;
AA c= F by A7,Lm4;
then
A14: AA c= G by A8;
g.(n+1) in AA by A6,FUNCT_1:def 3;
then g.(n+1) in G by A14;
then consider g1 being Element of L such that
A15: g.(n+1) = g1 and
A16: V "/\" {g1} c= V;
g1 in {g1} by TARSKI:def 1;
then x "/\" g1 in V "/\" {g1};
then ex y1 being Element of L st y1 in V & y1 << x "/\" g1 by A16,
WAYBEL_6:def 1;
hence thesis by A15;
end;
consider h being sequence of V1 such that
A17: h.0 = v1 and
A18: for n being Nat holds P[n,h.n,h.(n+1)] from RECDEF_1:sch
2 (A13);
A19: dom h = NAT by FUNCT_2:def 1;
then
A20: h.0 in rng h by FUNCT_1:def 3;
then reconsider R = rng h as non empty Subset of L by XBOOLE_1:1;
set O = uparrow fininfs R;
A21: R c= O by WAYBEL_0:62;
A22: for x, y being Element of L, n being Nat st h.n = x & h.(n+1
) = y holds y <= x
proof
let x, y be Element of L, n be Nat such that
A23: h.n = x & h.(n+1) = y;
consider x1, y1 being Element of V1, z1 being Element of L such that
A24: x1 = h.n & y1 = h.(n+1) and
z1 = g.(n+1) and
A25: y1 << x1 "/\" z1 by A18;
A26: x1 "/\" z1 <= x1 by YELLOW_0:23;
y1 <= x1 "/\" z1 by A25,WAYBEL_3:1;
hence thesis by A23,A24,A26,ORDERS_2:3;
end;
A27: for x, y being Element of L, n, m being Element of NAT st h.n = x & h.m
= y & n <= m holds y <= x
proof
defpred P[Nat] means for a being Element of NAT, s, t being
Element of L st t = h.a & s = h.$1 & a <= $1 holds s <= t;
A28: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A29: for j being Element of NAT, s, t being Element of L st t = h.j
& s = h.k & j <= k holds s <= t;
k in NAT by ORDINAL1:def 12;
then h.k in R by A19,FUNCT_1:def 3;
then reconsider s = h.k as Element of L;
let a be Element of NAT, c, d be Element of L such that
A30: d = h.a and
A31: c = h.(k+1) and
A32: a <= k+1;
A33: c <= s by A22,A31;
per cases by A32,NAT_1:8;
suppose
a <= k;
then s <= d by A29,A30;
hence thesis by A33,ORDERS_2:3;
end;
suppose
a = k + 1;
hence thesis by A30,A31;
end;
end;
A34: P[0] by NAT_1:3;
A35: for k being Nat holds P[k] from NAT_1:sch 2(A34,A28);
let x, y be Element of L, n, m be Element of NAT;
assume h.n = x & h.m = y & n <= m;
hence thesis by A35;
end;
A36: for x, y being Element of L st x in R & y in R holds x <= y or y <= x
proof
let x, y be Element of L;
assume that
A37: x in R and
A38: y in R;
consider m being object such that
A39: m in dom h and
A40: y = h.m by A38,FUNCT_1:def 3;
reconsider m as Element of NAT by A39;
consider n being object such that
A41: n in dom h and
A42: x = h.n by A37,FUNCT_1:def 3;
reconsider n as Element of NAT by A41;
per cases;
suppose
m <= n;
hence thesis by A27,A42,A40;
end;
suppose
n <= m;
hence thesis by A27,A42,A40;
end;
end;
A43: O is Open
proof
let x be Element of L;
assume x in O;
then consider y being Element of L such that
A44: y <= x and
A45: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A46: y = "/\"(Y,L) and
ex_inf_of Y,L by A45;
per cases;
suppose
Y <> {};
then y in Y by A36,A46,Th27;
then consider n being object such that
A47: n in dom h and
A48: h.n = y by FUNCT_1:def 3;
reconsider n as Element of NAT by A47;
consider x1, y1 being Element of V1, z1 being Element of L such that
A49: x1 = h.n and
A50: y1 = h.(n+1) and
z1 = g.(n+1) and
A51: y1 << x1 "/\" z1 by A18;
take y1;
y1 in R by A19,A50,FUNCT_1:def 3;
hence y1 in O by A21;
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by A51,WAYBEL_3:2;
hence thesis by A44,A48,A49,WAYBEL_3:2;
end;
suppose
A52: Y = {};
consider b being object such that
A53: b in R by XBOOLE_0:def 1;
reconsider b as Element of L by A53;
consider n being object such that
A54: n in dom h and
h.n = b by A53,FUNCT_1:def 3;
reconsider n as Element of NAT by A54;
A55: x <= Top L by YELLOW_0:45;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h.n and
A56: y1 = h.(n+1) and
z1 = g.(n+1) and
A57: y1 << x1 "/\" z1 by A18;
y = Top L by A46,A52,YELLOW_0:def 12;
then x = Top L by A44,A55,ORDERS_2:2;
then
A58: x1 <= x by YELLOW_0:45;
take y1;
y1 in R by A19,A56,FUNCT_1:def 3;
hence y1 in O by A21;
x1 "/\" z1 <= x1 by YELLOW_0:23;
then y1 << x1 by A57,WAYBEL_3:2;
hence thesis by A58,WAYBEL_3:2;
end;
end;
A59: for n being Element of NAT, a, b being Element of L st a = g.n & b = g.
(n+1) holds b <= a
proof
let n be Element of NAT, a, b be Element of L such that
A60: a = g.n & b = g.(n+1);
reconsider gn = {f.m where m is Element of NAT: m <= n}, gn1 = {f.k where
k is Element of NAT: k <= n+1} as non empty finite Subset of L by Lm1;
A61: ex_inf_of gn,L & ex_inf_of gn1,L by YELLOW_0:55;
A62: gn c= gn1
proof
let i be object;
assume i in gn;
then consider k being Element of NAT such that
A63: i = f.k and
A64: k <= n;
k <= n+1 by A64,NAT_1:12;
hence thesis by A63;
end;
a = "/\"(gn,L) & b = "/\"(gn1,L) by A5,A60;
hence thesis by A61,A62,YELLOW_0:35;
end;
A65: AA is_coarser_than R
proof
let a be Element of L;
assume a in AA;
then consider x being object such that
A66: x in dom g and
A67: g.x = a by FUNCT_1:def 3;
reconsider x as Element of NAT by A66;
consider x1, y1 being Element of V1, z1 being Element of L such that
x1 = h.x and
A68: y1 = h.(x+1) and
A69: z1 = g.(x+1) and
A70: y1 << x1 "/\" z1 by A18;
x1 "/\" z1 <= z1 & y1 <= x1 "/\" z1 by A70,WAYBEL_3:1,YELLOW_0:23;
then
A71: y1 <= z1 by ORDERS_2:3;
A72: h.(x+1) in R by A19,FUNCT_1:def 3;
z1 <= a by A59,A67,A69;
hence ex b be Element of L st b in R & b <= a by A68,A72,A71,ORDERS_2:3;
end;
reconsider O as Open Filter of L by A43;
R is_coarser_than O by A21,Th16;
then
A73: AA c= O by A65,YELLOW_4:7,8;
take O;
thus O c= V
proof
let q be object;
assume q in O;
then reconsider q as Element of O;
consider y being Element of L such that
A74: y <= q and
A75: y in fininfs R by WAYBEL_0:def 16;
consider Y being finite Subset of R such that
A76: y = "/\"(Y,L) and
ex_inf_of Y,L by A75;
per cases;
suppose
Y <> {};
then y in Y by A36,A76,Th27;
then consider n being object such that
A77: n in dom h and
A78: h.n = y by FUNCT_1:def 3;
reconsider n as Element of NAT by A77;
ex x1, y1 being Element of V1, z1 being Element of L st x1 = h.n &
y1 = h.(n+1) & z1 = g.(n+1) & y1 << x1 "/\" z1 by A18;
hence thesis by A74,A78,WAYBEL_0:def 20;
end;
suppose
A79: Y = {};
A80: q <= Top L by YELLOW_0:45;
y = Top L by A76,A79,YELLOW_0:def 12;
then q = Top L by A74,A80,ORDERS_2:2;
hence thesis by Th8;
end;
end;
thus v in O by A17,A20,A21;
uparrow fininfs AA = F by A7,Def3;
hence thesis by A73,WAYBEL_0:62;
end;
:: Corolarry 3.43.2
theorem Th34:
for L being lower-bounded continuous LATTICE, V being Open upper
Subset of L for N being non empty countable Subset of L for v being Element of
L st V "/\" N c= V & v in V ex O being Open Filter of L st {v} "/\" N c= O & O
c= V & v in O
proof
let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, N be
non empty countable Subset of L, v be Element of L such that
A1: V "/\" N c= V and
A2: v in V;
reconsider G = {x where x is Element of L : V "/\" {x} c= V} as Filter of L
by Th23,Th24,Th25;
A3: N c= G
proof
let q be object;
assume
A4: q in N;
then reconsider q1 = q as Element of L;
A5: {q1} "/\" V = {q1 "/\" y where y is Element of L: y in V} by YELLOW_4:42;
V "/\" {q1} c= V
proof
let t be object;
assume t in V "/\" {q1};
then consider y being Element of L such that
A6: t = q1 "/\" y and
A7: y in V by A5;
q1 "/\" y in N "/\" V by A4,A7;
hence thesis by A1,A6;
end;
hence thesis;
end;
N is GeneratorSet of uparrow fininfs N by Def3;
then consider F being Filter of L such that
A8: N is GeneratorSet of F;
F = uparrow fininfs N by A8,Def3;
then
A9: F c= G by A3,WAYBEL_0:62;
V "/\" F c= V
proof
let q be object;
assume q in V "/\" F;
then consider d, f being Element of L such that
A10: q = d "/\" f and
A11: d in V and
A12: f in F;
f in G by A9,A12;
then consider x being Element of L such that
A13: f = x and
A14: V "/\" {x} c= V;
x in {x} by TARSKI:def 1;
then d "/\" f in V "/\" {x} by A11,A13;
hence thesis by A10,A14;
end;
then consider O being Open Filter of L such that
A15: O c= V and
A16: v in O and
A17: F c= O by A2,A8,Th33;
take O;
A18: {v} "/\" N = {v "/\" n where n is Element of L: n in N} by YELLOW_4:42;
thus {v} "/\" N c= O
proof
let q be object;
assume q in {v} "/\" N;
then consider n being Element of L such that
A19: q = v "/\" n and
A20: n in N by A18;
N c= F by A8,Lm4;
then N c= O by A17;
then v "/\" n in O "/\" O by A16,A20;
hence thesis by A19,Th21;
end;
thus thesis by A15,A16;
end;
:: Proposition 3.43.3
theorem Th35:
for L being lower-bounded continuous LATTICE, V being Open upper
Subset of L for N being non empty countable Subset of L, x, y being Element of
L st V "/\" N c= V & y in V & not x in V ex p being irreducible Element of L st
x <= p & not p in uparrow ({y} "/\" N)
proof
let L be lower-bounded continuous LATTICE, V be Open upper Subset of L, N be
non empty countable Subset of L, x, y be Element of L such that
A1: V "/\" N c= V & y in V and
A2: not x in V;
consider O being Open Filter of L such that
A3: {y} "/\" N c= O and
A4: O c= V and
y in O by A1,Th34;
uparrow O c= O & O c= uparrow O by WAYBEL_0:16,24;
then uparrow O = O;
then
A5: uparrow({y} "/\" N) c= O by A3,YELLOW_3:7;
not x in O by A2,A4;
then x in O` by XBOOLE_0:def 5;
then consider p being Element of L such that
A6: x <= p and
A7: p is_maximal_in O` by WAYBEL_6:9;
reconsider p as irreducible Element of L by A7,WAYBEL_6:13;
take p;
thus x <= p by A6;
p in O` by A7,WAYBEL_4:55;
hence thesis by A5,XBOOLE_0:def 5;
end;
:: Corollary 3.43.4
theorem Th36:
for L being lower-bounded continuous LATTICE, x being Element of
L for N being non empty countable Subset of L st for n, y being Element of L st
not y <= x & n in N holds not y "/\" n <= x for y being Element of L st not y
<= x ex p being irreducible Element of L st x <= p & not p in uparrow ({y} "/\"
N)
proof
let L be lower-bounded continuous LATTICE, x be Element of L, N be non empty
countable Subset of L such that
A1: for n, y being Element of L st not y <= x & n in N holds not y "/\" n <= x;
set V = (downarrow x)`;
A2: V "/\" N c= V
proof
let q be object;
assume q in V "/\" N;
then consider v, n being Element of L such that
A3: q = v "/\" n and
A4: v in V and
A5: n in N;
not v in downarrow x by A4,XBOOLE_0:def 5;
then not v <= x by WAYBEL_0:17;
then not v "/\" n <= x by A1,A5;
then not v "/\" n in downarrow x by WAYBEL_0:17;
hence thesis by A3,XBOOLE_0:def 5;
end;
x <= x;
then x in downarrow x by WAYBEL_0:17;
then
A6: not x in V by XBOOLE_0:def 5;
let y be Element of L;
assume not y <= x;
then not y in downarrow x by WAYBEL_0:17;
then y in V by XBOOLE_0:def 5;
hence thesis by A2,A6,Th35;
end;
:: Definition 3.43.5
definition
let L be non empty RelStr, u be Element of L;
attr u is dense means
for v being Element of L st v <> Bottom L holds u "/\" v <> Bottom L;
end;
registration
let L be upper-bounded Semilattice;
cluster Top L -> dense;
coherence
by WAYBEL_1:4;
end;
registration
let L be upper-bounded Semilattice;
cluster dense for Element of L;
existence
proof
take Top L;
thus thesis;
end;
end;
theorem
for L being non trivial bounded Semilattice for x being Element of L
st x is dense holds x <> Bottom L
proof
let L be non trivial bounded Semilattice, x be Element of L such that
A1: x is dense;
Top L <> Bottom L by WAYBEL_7:3;
then x "/\" Top L <> Bottom L by A1;
hence thesis by WAYBEL_1:4;
end;
definition
let L be non empty RelStr, D be Subset of L;
attr D is dense means
:Def5:
for d being Element of L st d in D holds d is dense;
end;
theorem Th38:
for L being upper-bounded Semilattice holds {Top L} is dense
by TARSKI:def 1;
registration
let L be upper-bounded Semilattice;
cluster non empty finite countable dense for Subset of L;
existence
proof
take {Top L};
thus {Top L} is non empty finite countable;
thus thesis by Th38;
end;
end;
:: Theorem 3.43.7
::$N Baire Category Theorem for Continuous Lattices
theorem Th39:
for L being lower-bounded continuous LATTICE for D being non
empty countable dense Subset of L, u being Element of L st u <> Bottom L ex p
being irreducible Element of L st p <> Top L & not p in uparrow ({u} "/\" D)
proof
let L be lower-bounded continuous LATTICE, D be non empty countable dense
Subset of L, u be Element of L such that
A1: u <> Bottom L;
A2: for d, y being Element of L st not y <= Bottom L & d in D holds not y
"/\" d <= Bottom L
proof
let d, y be Element of L such that
A3: not y <= Bottom L;
assume d in D;
then d is dense by Def5;
then
A4: y "/\" d <> Bottom L by A3;
Bottom L <= y "/\" d by YELLOW_0:44;
hence thesis by A4,ORDERS_2:2;
end;
Bottom L <= u by YELLOW_0:44;
then not u <= Bottom L by A1,ORDERS_2:2;
then consider p being irreducible Element of L such that
Bottom L <= p and
A5: not p in uparrow ({u} "/\" D) by A2,Th36;
take p;
thus p <> Top L by A5,Th9;
thus thesis by A5;
end;
theorem Th40:
for T being non empty TopSpace for A being Element of InclPoset
the topology of T for B being Subset of T st A = B & B` is irreducible holds A
is irreducible
proof
let T be non empty TopSpace, A be Element of InclPoset the topology of T, B
be Subset of T such that
A1: A = B;
assume that
B` is non empty closed and
A2: for S1, S2 being Subset of T st S1 is closed & S2 is closed & B` =
S1 \/ S2 holds S1 = B` or S2 = B`;
let x, y be Element of InclPoset the topology of T such that
A3: A = x "/\" y;
A4: the carrier of InclPoset the topology of T = the topology of T by
YELLOW_1:1;
then x in the topology of T & y in the topology of T;
then reconsider x1 = x, y1 = y as Subset of T;
A5: y1 is open by A4;
then
A6: y1` is closed;
A7: x1 is open by A4;
then x1 /\ y1 is open by A5;
then x /\ y in the topology of T;
then A = x /\ y by A3,YELLOW_1:9;
then
A8: B` = (x1`) \/ y1` by A1,XBOOLE_1:54;
x1` is closed by A7;
then x1` = B` or y1` = B` by A2,A6,A8;
hence thesis by A1,TOPS_1:1;
end;
theorem Th41:
for T being non empty TopSpace for A being Element of InclPoset
the topology of T for B being Subset of T st A = B & A <> Top InclPoset the
topology of T holds A is irreducible iff B` is irreducible
proof
let T be non empty TopSpace, A be Element of InclPoset the topology of T, B
be Subset of T such that
A1: A = B and
A2: A <> Top InclPoset the topology of T;
A3: the carrier of InclPoset the topology of T = the topology of T
by YELLOW_1:1;
hereby
assume
A4: A is irreducible;
thus B` is irreducible
proof
B <> the carrier of T by A1,A2,YELLOW_1:24;
then (the carrier of T) \ B <> {} by XBOOLE_1:37;
hence B` is non empty;
B`` is open by A1,A3;
hence B` is closed;
let S1, S2 be Subset of T such that
A5: S1 is closed & S2 is closed and
A6: B` = S1 \/ S2;
A7: S1` is open & S2` is open by A5;
then reconsider
s1 = S1`, s2 = S2` as Element of InclPoset the topology of T
by A3;
(S1`) /\ S2` is open by A7;
then
A8: s1 /\ s2 in the topology of T;
B = (S1 \/ S2)` by A6
.= (S1`) /\ S2` by XBOOLE_1:53;
then A = s1 "/\" s2 by A1,A8,YELLOW_1:9;
then A = s1 or A = s2 by A4;
hence thesis by A1;
end;
end;
thus thesis by A1,Th40;
end;
theorem Th42:
for T being non empty TopSpace for A being Element of InclPoset
the topology of T for B being Subset of T st A = B holds A is dense iff B is
everywhere_dense
proof
let T be non empty TopSpace, A be Element of InclPoset the topology of T, B
be Subset of T such that
A1: A = B;
A2: Bottom InclPoset the topology of T = {} by PRE_TOPC:1,YELLOW_1:13;
A3: the carrier of InclPoset the topology of T = the topology of T by
YELLOW_1:1;
then
A4: B is open by A1;
hereby
assume
A5: A is dense;
for Q being Subset of T st Q <> {} & Q is open holds B meets Q
proof
let Q be Subset of T such that
A6: Q <> {} and
A7: Q is open;
reconsider q = Q as Element of InclPoset the topology of T by A3,A7;
B /\ Q is open by A4,A7;
then
A8: A /\ q in the topology of T by A1;
A "/\" q <> Bottom InclPoset the topology of T by A2,A5,A6;
then B /\ Q <> {} by A1,A2,A8,YELLOW_1:9;
hence thesis;
end;
then B is dense by TOPS_1:45;
hence B is everywhere_dense by A4,TOPS_3:36;
end;
assume B is everywhere_dense;
then
A9: B is dense by TOPS_3:33;
let v be Element of InclPoset the topology of T such that
A10: v <> Bottom InclPoset the topology of T;
v in the topology of T by A3;
then reconsider V = v as Subset of T;
A11: V is open by A3;
B is open by A1,A3;
then B /\ V is open by A11;
then
A12: B /\ V in the topology of T;
B meets V by A2,A9,A10,A11,TOPS_1:45;
then B /\ V <> {};
hence A "/\" v <> Bottom InclPoset the topology of T by A1,A2,A12,YELLOW_1:9;
end;
:: Theorem 3.43.8
theorem Th43:
for T being non empty TopSpace st T is locally-compact for D
being countable Subset-Family of T st D is non empty dense open for O being non
empty Subset of T st O is open ex A being irreducible Subset of T st for V
being Subset of T st V in D holds A /\ O meets V
proof
let T be non empty TopSpace;
assume T is locally-compact;
then reconsider
L = InclPoset the topology of T as bounded continuous LATTICE by WAYBEL_3:42;
A1: the carrier of L = the topology of T by YELLOW_1:1;
let D be countable Subset-Family of T such that
A2: D is non empty dense open;
consider I being object such that
A3: I in D by A2;
reconsider I as Subset of T by A3;
I is open by A2,A3;
then reconsider i = I as Element of L by A1;
set D1 = {d where d is Element of L : ex d1 being Subset of T st d1 in D &
d1 = d & d is dense};
D1 c= the carrier of L
proof
let q be object;
assume q in D1;
then
ex d being Element of L st q = d & ex d1 being Subset of T st d1 in D &
d1 = d & d is dense;
hence thesis;
end;
then reconsider D1 as Subset of L;
A4: D1 c= D
proof
let q be object;
assume q in D1;
then ex d being Element of L st q = d & ex d1 being Subset of T st d1 in D
& d1 = d & d is dense;
hence thesis;
end;
A5: D1 is dense
proof
let q be Element of L;
assume q in D1;
then ex d being Element of L st q = d & ex d1 being Subset of T st d1 in D
& d1 = d & d is dense;
hence thesis;
end;
let O be non empty Subset of T such that
A6: O is open;
reconsider u = O as Element of L by A6,A1;
I is open dense by A2,A3;
then I is everywhere_dense by TOPS_3:36;
then i is dense by Th42;
then u <> Bottom L & i in D1 by A3,PRE_TOPC:1,YELLOW_1:13;
then consider p being irreducible Element of L such that
A7: p <> Top L and
A8: not p in uparrow ({u} "/\" D1) by A4,A5,Th39;
p in the topology of T by A1;
then reconsider P = p as Subset of T;
reconsider A = P` as irreducible Subset of T by A7,Th41;
take A;
let V be Subset of T;
assume
A9: V in D;
then
A10: V is open by A2;
then reconsider v = V as Element of L by A1;
A11: for d1 being Element of L st d1 in D1 holds not u "/\" d1 <= p
proof
A12: u in {u} by TARSKI:def 1;
let d1 be Element of L;
assume d1 in D1;
then u "/\" d1 in {u} "/\" D1 by A12;
hence thesis by A8,WAYBEL_0:def 16;
end;
V is dense by A2,A9;
then V is everywhere_dense by A10,TOPS_3:36;
then v is dense by Th42;
then v in D1 by A9;
then not u "/\" v <= p by A11;
then
A13: not u "/\" v c= p by YELLOW_1:3;
O /\ V is open by A6,A10;
then u /\ v in the topology of T;
then not O /\ V c= p by A13,YELLOW_1:9;
then consider x being object such that
A14: x in O /\ V and
A15: not x in A`;
reconsider x as Element of T by A14;
x in A by A15,XBOOLE_0:def 5;
then O /\ V /\ A <> {} by A14,XBOOLE_0:def 4;
hence A /\ O /\ V <> {} by XBOOLE_1:16;
end;
definition
let T be non empty TopSpace;
redefine attr T is Baire means :: redefines Baire (YELLOW_8, definition)
for F being Subset-Family of T st F is
countable & for S being Subset of T st S in F holds S is open dense ex I being
Subset of T st I = Intersect F & I is dense;
compatibility
proof
set D = bool the carrier of T;
hereby
assume
A1: T is Baire;
thus for F being Subset-Family of T st F is countable & for S being
Subset of T st S in F holds S is open dense ex I being Subset of T st I =
Intersect F & I is dense
proof
let F be Subset-Family of T such that
A2: F is countable and
A3: for S being Subset of T st S in F holds S is open dense;
for S being Subset of T st S in F holds S is everywhere_dense
proof
let S be Subset of T;
assume S in F;
then S is open dense by A3;
hence thesis by TOPS_3:36;
end;
hence thesis by A1,A2;
end;
end;
assume
A4: for F being Subset-Family of T st F is countable & for S being
Subset of T st S in F holds S is open dense ex I being Subset of T st I =
Intersect F & I is dense;
deffunc F(Element of D) = Int $1;
let F be Subset-Family of T such that
A5: F is countable and
A6: for S being Subset of T st S in F holds S is everywhere_dense;
set F1 = {Int A where A is Subset of T : A in F};
consider f being Function of D, D such that
A7: for x being Element of D holds f.x = F(x) from FUNCT_2:sch 4;
F1 c= f.:F
proof
let q be object;
assume q in F1;
then consider A being Subset of T such that
A8: q = Int A & A in F;
dom f = D & f.A = Int A by A7,FUNCT_2:def 1;
hence thesis by A8,FUNCT_1:def 6;
end;
then card F1 c= card F by CARD_1:66;
then
A9: F1 is countable by A5,Th1;
reconsider J = Intersect F as Subset of T;
A10: F1 c= bool the carrier of T
proof
let q be object;
assume q in F1;
then ex A being Subset of T st q = Int A & A in F;
hence thesis;
end;
take J;
thus J = Intersect F;
reconsider F1 as Subset-Family of T by A10;
for X being set st X in F holds Intersect F1 c= X
proof
let X be set such that
A11: X in F;
reconsider X1 = X as Subset of T by A11;
A12: Int X1 in F1 by A11;
let q be object;
assume q in Intersect F1;
then Int X1 c= X1 & q in Int X1 by A12,SETFAM_1:43,TOPS_1:16;
hence thesis;
end;
then
A13: Intersect F1 c= Intersect F by MSSUBFAM:4;
now
let S be Subset of T;
assume S in F1;
then consider A being Subset of T such that
A14: S = Int A and
A15: A in F;
A is everywhere_dense by A6,A15;
hence S is open dense by A14,TOPS_3:35;
end;
then ex I being Subset of T st I = Intersect F1 & I is dense by A4,A9;
hence thesis by A13,TOPS_1:44;
end;
end;
:: Corolarry 3.43.10
theorem
for T being non empty TopSpace st T is sober locally-compact holds T is Baire
proof
let T be non empty TopSpace such that
A1: T is sober locally-compact;
let F be Subset-Family of T such that
A2: F is countable and
A3: for S being Subset of T st S in F holds S is open dense;
A4: F is open
by A3;
for X being Subset of T st X in F holds X is dense by A3;
then
A5: F is open dense by A4;
reconsider I = Intersect F as Subset of T;
take I;
thus I = Intersect F;
per cases;
suppose
A6: F <> {};
for Q being Subset of T st Q <> {} & Q is open holds (Intersect F) meets Q
proof
let Q be Subset of T;
assume that
A7: Q <> {} and
A8: Q is open;
consider S being irreducible Subset of T such that
A9: for V being Subset of T st V in F holds S /\ Q meets V by A1,A2,A5,A6,A7
,A8,Th43;
consider p being Point of T such that
A10: p is_dense_point_of S and
for q being Point of T st q is_dense_point_of S holds p = q by A1;
S is closed by YELLOW_8:def 3;
then
A11: S = Cl{p} by A10,YELLOW_8:16;
A12: for Y being set holds Y in F implies p in Y & p in Q
proof
let Y be set;
assume
A13: Y in F;
then reconsider Y1 = Y as Subset of T;
S /\ Q meets Y1 by A9,A13;
then
A14: S /\ Q /\ Y1 <> {};
now
assume not p in Q /\ Y1;
then p in (Q /\ Y1)` by XBOOLE_0:def 5;
then {p} c= (Q /\ Y1)` by ZFMISC_1:31;
then
A15: Cl{p} c= Cl(Q /\ Y1)` by PRE_TOPC:19;
Y1 is open by A3,A13;
then Q /\ Y1 is open by A8;
then (Q /\ Y1)` is closed;
then S c= (Q /\ Y1)` by A11,A15,PRE_TOPC:22;
then S misses (Q /\ Y1) by SUBSET_1:23;
then S /\ (Q /\ Y1) = {};
hence contradiction by A14,XBOOLE_1:16;
end;
hence thesis by XBOOLE_0:def 4;
end;
then for Y being set holds Y in F implies p in Y;
then
A16: p in Intersect F by SETFAM_1:43;
ex Y being object st Y in F by A6,XBOOLE_0:def 1;
then p in Q by A12;
then (Intersect F) /\ Q <> {} by A16,XBOOLE_0:def 4;
hence thesis;
end;
hence thesis by TOPS_1:45;
end;
suppose
F = {};
then Intersect F = [#]T by SETFAM_1:def 9;
hence thesis;
end;
end;