:: Convergent Filter Bases
:: by Roland Coghetto
::
:: Received June 30, 2015
:: Copyright (c) 2015-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 FINSET_1, CARD_1, XBOOLE_0, SUBSET_1, SETFAM_1, TARSKI, ZFMISC_1,
ORDINAL1, FUNCT_1, RELAT_1, CARD_FIL, LATTICES, PBOOLE, STRUCT_0,
ORDERS_2, XXREAL_0, LATTICE3, WAYBEL_0, YELLOW_1, NUMBERS, FINSEQ_1,
NAT_1, YELLOW13, ARYTM_3, PRE_TOPC, RCOMP_1, CANTOR_1, FILTER_0, DICKSON,
RELAT_2, MEMBERED, XXREAL_1, FUNCT_3, FINSUB_1, WAYBEL_7, YELLOW19,
COMPTS_1, CARD_3, CARDFIL2;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, FINSET_1,
ORDINAL1, CARD_1, RELSET_1, CARD_FIL, DOMAIN_1, NAT_1, STRUCT_0,
LATTICES, FILTER_0, NUMBERS, LATTICE3, YELLOW_0, ORDERS_2, YELLOW_1,
XXREAL_0, FINSEQ_1, CANTOR_1, NAT_LAT, DICKSON, WAYBEL_0, MEMBERED,
FUNCT_3, FUNCT_2, FINSUB_1, PBOOLE, ZFMISC_1, PRE_TOPC, WAYBEL_7,
COMPTS_1, YELLOW19, YELLOW_6, MCART_1, CARD_3;
constructors CARD_FIL, WAYBEL_7, CANTOR_1, NAT_LAT, DICKSON, FINSUB_1, PROB_1,
NAT_1, COMPTS_1, YELLOW19, BORSUK_1, ORDERS_3, WAYBEL11, XXREAL_2,
SIMPLEX0;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, RELSET_1, FINSET_1, CARD_1,
STRUCT_0, LATTICE3, WAYBEL_0, YELLOW_1, WAYBEL_7, RELAT_1, XREAL_0,
NAT_1, DICKSON, MEMBERED, FUNCT_2, CANTOR_1, PBOOLE, PROB_1, SETFAM_1,
YELLOW19, WAYBEL_3, CARD_3;
requirements NUMERALS, SUBSET, BOOLE, REAL;
definitions TARSKI, XBOOLE_0;
equalities STRUCT_0, LATTICE3, YELLOW_1, CARD_FIL, DICKSON, WAYBEL_0;
expansions TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, ORDERS_2, WAYBEL_0, FINSUB_1;
theorems TARSKI, FUNCT_1, FUNCT_2, ORDINAL1, SETFAM_1, ZFMISC_1, RELAT_1,
XBOOLE_0, XBOOLE_1, CARD_FIL, FILTER_0, LATTICE3, WAYBEL_0, YELLOW_1,
WAYBEL_7, WAYBEL_8, WAYBEL15, WAYBEL16, AFINSQ_1, NAT_1, FINSEQ_1,
PRE_TOPC, CONNSP_2, CANTOR_1, DICKSON, XTUPLE_0, AFINSQ_2, SUBSET_1,
PRE_CIRC, PARTFUN1, YELLOW19, CARD_3;
schemes FUNCT_2, NAT_1, SUBSET_1;
begin :: Filters -- Set-theoretical Approach
reserve
X for non empty set,
FX for Filter of X,
SFX for Subset-Family of X;
definition
let X be set, SFX be Subset-Family of X;
attr SFX is upper means :def1:
for Y1,Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds Y2 in SFX;
end;
registration
let X be set;
cluster non empty for cap-closed Subset-Family of X;
existence
proof
reconsider SFX={{}} as non empty Subset-Family of X by SETFAM_1:46;
now
let x,y be set;
assume x in {{}} & y in {{}};
then x={} & y={} by TARSKI:def 1;
hence x/\y in {{}} by TARSKI:def 1;
end;
then SFX is cap-closed;
hence thesis;
end;
end;
registration
let X be set;
cluster upper for non empty cap-closed Subset-Family of X;
existence
proof
per cases;
suppose X is non empty;
then reconsider B={X} as non empty Subset-Family of X by CARD_FIL:2;
A1: now
let x,y be set;
assume x in {X} & y in {X};
then x=X & y=X by TARSKI:def 1;
hence x/\y in {X} by TARSKI:def 1;
end;
now
let Y1,Y2 be Subset of X;
assume
A2: Y1 in B & Y1 c= Y2;
then Y1=X & Y2=X by TARSKI:def 1;
hence Y2 in B by A2;
end;
then B is cap-closed & B is upper by A1;
hence thesis;
end;
suppose
A3: X is empty;
now
let x,y be set;
assume x in {{}} & y in {{}};
then x={} & y={} by TARSKI:def 1;
hence x/\y in {{}} by TARSKI:def 1;
end;
then {{}} is cap-closed;
then reconsider B={{}} as non empty cap-closed Subset-Family of {}
by SETFAM_1:46;
B is upper;
hence thesis by A3;
end;
end;
end;
registration
let X be non empty set;
cluster with_non-empty_elements for non empty upper cap-closed
Subset-Family of X;
existence
proof
now
let x,y be set;
assume that
A1: x in {X} and
A2: y in {X};
x=X & y=X by A1,A2,TARSKI:def 1;
hence x/\y in {X} by TARSKI:def 1;
end;
then {X} is cap-closed;
then reconsider B={X} as non empty cap-closed Subset-Family of X
by CARD_FIL:2;
now
let Y1,Y2 be Subset of X;
assume
A3: Y1 in B & Y1 c= Y2;
Y1=X & Y2=X by A3,TARSKI:def 1;
hence Y2 in B by A3;
end;
then B is upper;
hence thesis;
end;
end;
Lm01:
for SFX being non empty with_non-empty_elements upper cap-closed
Subset-Family of X holds SFX is Filter of X
proof
let SFX be non empty with_non-empty_elements upper cap-closed
Subset-Family of X;
now
thus not {} in SFX;
SFX is cap-closed;
hence for Y1,Y2 be Subset of X st Y1 in SFX & Y2 in SFX holds
Y1/\Y2 in SFX;
thus for Y1,Y2 be Subset of X st Y1 in SFX & Y1 c= Y2 holds Y2 in SFX
by def1;
end;
hence thesis by CARD_FIL:def 1;
end;
Lm02:
FX is non empty with_non-empty_elements upper cap-closed Subset-Family of X
proof
FX is non empty with_non-empty_elements cap-closed upper
by CARD_FIL:def 1;
hence thesis;
end;
theorem
SFX is non empty with_non-empty_elements upper cap-closed
Subset-Family of X iff SFX is Filter of X by Lm01,Lm02;
theorem
for X1,X2 being non empty set,F1 being Filter of X1,F2 being Filter of X2
holds
the set of all [:f1,f2:] where f1 is Element of F1,f2 is Element of F2 is
non empty Subset-Family of [:X1,X2:]
proof
let X1,X2 be non empty set,F1 be Filter of X1,F2 be Filter of X2;
set F1xF2=the set of all [:f1,f2:] where f1 is Element of F1,
f2 is Element of F2;
A0: [:the Element of F1,the Element of F2:] in F1xF2;
F1xF2 c= bool [:X1,X2:]
proof
let x be object;assume x in F1xF2;
then consider f1 be Element of F1,f2 be Element of F2 such that
A1: x=[:f1,f2:];
thus thesis by A1;
end;
hence thesis by A0;
end;
definition
let X be non empty set;
attr X is cap-finite-closed means
for SX be finite non empty Subset of X holds meet SX in X;
end;
registration
cluster cap-finite-closed for non empty set;
existence
proof
take X={{}};
now
let SX be finite non empty Subset of X;
meet SX = meet {{}} or meet SX = meet {} by ZFMISC_1:33;
then meet SX = {} by SETFAM_1:10,SETFAM_1:1;
hence meet SX in X by TARSKI:def 1;
end;
hence thesis;
end;
end;
theorem Th01:
for X being non empty set st X is cap-finite-closed holds
X is cap-closed
proof
let X be non empty set;
assume
A1: X is cap-finite-closed;
now
let a,b be set;
assume a in X & b in X;
then {a,b} c= X by TARSKI:def 2;
then meet {a,b} in X by A1;
hence a/\b in X by SETFAM_1:11;
end;
hence thesis;
end;
registration
cluster cap-finite-closed -> cap-closed for non empty set;
coherence by Th01;
end;
theorem Th02:
for X be set,SFX be Subset-Family of X holds SFX is cap-closed & X in SFX iff
FinMeetCl SFX c= SFX
proof
let X be set,F be Subset-Family of X;
hereby
assume that
A1: F is cap-closed and
A2: X in F;
now
let x be object;
assume
A3: x in FinMeetCl F;
then reconsider x1=x as Subset of X;
consider Y be Subset-Family of X such that
A4: Y c= F and
A5: Y is finite and
A6: x1=Intersect Y by A3,CANTOR_1:def 3;
defpred P[Nat] means
for Y be Subset-Family of X,x be Subset of X st
Y c= F & card Y=$1 & x = Intersect Y holds
x in F;
A7: P[0]
proof
let Y be Subset-Family of X,x be Subset of X;
assume that
Y c= F and
A8: card Y=0 and
A9: x = Intersect Y;
A10: Y={} by A8;
reconsider x0=x as set;
thus x in F by A9,A10,SETFAM_1:def 9,A2;
end;
A11: for k being Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume
A12: P[k];
now
let Y be Subset-Family of X,x be Subset of X;
assume that
A13: Y c= F and
A14: card Y=k+1 and
A15: x = Intersect Y;
Y is finite set by A14;
then consider x1 be Element of Y,C being Subset of Y such that
A16: Y=C\/{x1} and
A17: card C = k by A14,PRE_CIRC:24;
A18: C c= F & card C=k by A13,A17;
F c= bool X;
then C c= bool X by A13;
then reconsider C0=C as Subset-Family of X;
per cases;
suppose
A19: C={};
meet {x1}=x1 by SETFAM_1:10;
then x=x1 by A15,A16,A19,SETFAM_1:def 9;
hence x in F by A13,A16;
end;
suppose
A20: C<>{};
then meet(C\/{x1})=meet(C) /\ meet({x1}) by SETFAM_1:9;
then
A21: meet(Y)=meet C /\ x1 by A16,SETFAM_1:10;
meet Y =Intersect(Y) by A16,SETFAM_1:def 9;
then
A22: Intersect(Y)=Intersect(C0)/\x1 by A20,A21,SETFAM_1:def 9;
A23: Intersect(C0) in F by A12,A18;
x1 in F by A13,A16;
hence x in F by A22,A15,A23,A1;
end;
end;
hence P[k+1];
end;
A24: for k being Nat holds P[k] from NAT_1:sch 2(A7,A11);
reconsider CY=card Y as Nat by A5;
P[CY] by A24;
hence x in F by A4,A6;
end;
hence FinMeetCl F c= F;
end;
assume
A25:
FinMeetCl F c= F;
now
let A,B be set;
assume
A26:A in F & B in F;
then A in bool X & B in bool X;
then {A,B} c= bool X by TARSKI:def 2;
then reconsider AB={A,B} as finite Subset-Family of X;
AB c= F & AB is finite & meet AB=Intersect AB
by A26,TARSKI:def 2,SETFAM_1:def 9;
then meet AB in FinMeetCl F by CANTOR_1:def 3;
then A/\B in FinMeetCl F by SETFAM_1:11;
hence A/\B in F by A25;
end;
hence F is cap-closed & X in F by A25,CANTOR_1:8;
end;
theorem
for X be non empty set, A be non empty Subset of X holds
{B where B is Subset of X: A c= B} is Filter of X
proof
let X be non empty set, A be non empty Subset of X;
set C={B where B is Subset of X:A c= B};
A1: C is non empty Subset-Family of X
proof
A2: A in C;
now
let x be object such that
A3: x in C;
consider b0 be Subset of X such that
A4: x=b0 and
A c= b0 by A3;
thus x in bool X by A4;
end;
then C c= bool X;
hence thesis by A2;
end;
A5: not {} in C
proof
assume {} in C;
then consider b0 be Subset of X such that
A6: {}=b0 & A c= b0;
thus thesis by A6;
end;
A7: for Y1,Y2 be Subset of X holds Y1 in C & Y2 in C implies Y1/\Y2 in C
proof
let Y1,Y2 be Subset of X such that
A8: Y1 in C and
A9: Y2 in C;
consider b1 be Subset of X such that
A10: Y1=b1 & A c= b1 by A8;
consider b2 be Subset of X such that
A11: Y2=b2 & A c= b2 by A9;
A c= Y1/\Y2 by A10,A11,XBOOLE_1:19;
hence thesis;
end;
for Y1,Y2 be Subset of X holds Y1 in C & Y1 c= Y2 implies Y2 in C
proof
let Y1,Y2 be Subset of X such that
A12: Y1 in C and
A13: Y1 c= Y2;
consider b1 be Subset of X such that
A14: b1=Y1 & A c= b1 by A12;
A c= Y2 by A13,A14;
hence thesis;
end;
hence thesis by A1,A5,A7,CARD_FIL:def 1;
end;
registration
let X be non empty set;
cluster -> cap-closed for Filter of X;
coherence by CARD_FIL:def 1;
end;
theorem
for X be set, B be Subset-Family of X st B={X} holds
B is upper
proof
let X be set,B be Subset-Family of X;
assume
A1: B={X};
now
let Y1,Y2 be Subset of X;
assume
A3: Y1 in B & Y1 c= Y2;
Y1=X & Y2=X by A1,A3,TARSKI:def 1;
hence Y2 in B by A3;
end;
hence thesis;
end;
theorem
for X be non empty set, F be Filter of X holds F <> bool X
proof
let X be non empty set,F be Filter of X;
assume
A1: F = bool X;
{} c= X;
hence contradiction by A1,CARD_FIL:def 1;
end;
definition
let X be non empty set;
func Filt X -> non empty set equals
the set of all F where F is Filter of X;
correctness
proof
reconsider FX={X} as Filter of X by CARD_FIL:4;
FX in the set of all F where F is Filter of X;
hence thesis;
end;
end;
definition
let X be non empty set,I be non empty set,
M be (Filt X)-valued ManySortedSet of I;
func Filter_Intersection M -> Filter of X equals
meet rng M;
coherence
proof
set F=meet rng M;
A1: now
let Y be set;
assume Y in rng M;
then consider a being object such that
A2: a in dom M and
A3: M.a=Y by FUNCT_1:def 3;
M.a in Filt X by A2,FUNCT_1:102;
then consider FF be Filter of X such that
A4: M.a = FF;
thus X in Y by A3,A4,CARD_FIL:5;
end;
now
let x be object;
assume
A5: x in F;
set i0 = the Element of I;
i0 in I & I is non empty;
then
A6: i0 in dom M by PARTFUN1:def 2;
then M.i0 in rng M by FUNCT_1:def 3; then
A7: x in M.i0 by A5,SETFAM_1:def 1;
M.i0 in Filt X by A6,FUNCT_1:102;
then consider F0 be Filter of X such that
A8: M.i0 = F0;
thus x in bool X by A7,A8;
end;
then F c= bool X;
then reconsider F as non empty Subset-Family of X by A1,SETFAM_1:def 1;
A9: not {} in F
proof
assume
A10: {} in F;
set i0 = the Element of I;
i0 in I & I is non empty;
then
A11: i0 in dom M by PARTFUN1:def 2;
then
A12: M.i0 in rng M by FUNCT_1:def 3;
M.i0 in Filt X by A11,FUNCT_1:102;
then consider F0 be Filter of X such that
A13: M.i0 = F0;
{} in F0 by A12,A10,SETFAM_1:def 1,A13;
hence contradiction by CARD_FIL:def 1;
end;
now
hereby
let Y1,Y2 be Subset of X;
assume that
A14: Y1 in F and
A15: Y2 in F;
now
let Y be set;
assume
A16: Y in rng M;
then Y in Filt X;
then consider F0 be Filter of X such that
A17: Y=F0;
Y1 in F0 & Y2 in F0 by A14,A15,A16,A17,SETFAM_1:def 1;
hence Y1/\Y2 in Y by A17,CARD_FIL:def 1;
end;
hence Y1/\Y2 in F by SETFAM_1:def 1;
end;
let Y1,Y2 be Subset of X;
assume that
A18: Y1 in F and
A19: Y1 c= Y2;
now
let Y be set;
assume
A20: Y in rng M;
then Y in Filt X;
then consider F0 be Filter of X such that
A21: Y=F0;
Y1 in Y by A18,A20,SETFAM_1:def 1;
hence Y2 in Y by A19,A21,CARD_FIL:def 1;
end;
hence Y2 in F by SETFAM_1:def 1;
end;
hence thesis by A9,CARD_FIL:def 1;
end;
end;
definition
let X be non empty set, F1,F2 be Filter of X;
pred F1 is_filter-coarser_than F2 means
F1 c= F2;
reflexivity;
pred F1 is_filter-finer_than F2 means
F2 c= F1;
reflexivity;
end;
theorem
for X be non empty set,F be Filter of X,FX be Filter of X st FX={X} holds
FX is_coarser_than F
proof
let X be non empty set,F be Filter of X,FX be Filter of X;
assume
A1: FX={X};
X in F by CARD_FIL:5;
then {X} c= F by TARSKI:def 1;
hence thesis by A1;
end;
theorem
for X be non empty set,I be non empty set,
M be (Filt X)-valued ManySortedSet of I holds
for i be Element of I,F be Filter of X st F=M.i holds
Filter_Intersection M is_filter-coarser_than F
proof
let X be non empty set,I be non empty set,
M be (Filt X)-valued ManySortedSet of I;
let i be Element of I,F be Filter of X;
set FIM=Filter_Intersection M;
assume
A1: F=M.i;
now
let a be object;
assume
A2: a in Filter_Intersection M;
i in I;
then i in dom M by PARTFUN1:def 2;
then M.i in rng M by FUNCT_1:def 3;
hence a in F by A1,A2,SETFAM_1:def 1;
end;
then FIM c= F;
hence FIM is_filter-coarser_than F;
end;
theorem
for X be set,S be Subset-Family of X st
FinMeetCl S is with_non-empty_elements holds
S is with_non-empty_elements
proof
let X be set,S be Subset-Family of X;
assume
A1: FinMeetCl S is with_non-empty_elements;
assume not S is with_non-empty_elements;
then {} in S & S c= FinMeetCl S by CANTOR_1:4;
hence contradiction by A1;
end;
theorem
for X be non empty set, G be Subset-Family of X ,F be Filter of X st
G c= F holds FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements
proof
let X be non empty set,G be Subset-Family of X, F be Filter of X;
assume
A1: G c= F;
A2: FinMeetCl G c= FinMeetCl F by A1,CANTOR_1:14;
FinMeetCl F c= F by Th02,CARD_FIL:5;
hence FinMeetCl G c= F by A2;
hence FinMeetCl G is with_non-empty_elements by CARD_FIL:def 1;
end;
definition
let X be non empty set;
let F be Filter of X;
let B be non empty Subset of F;
attr B is filter_basis means
:def2:
for f be Element of F holds ex b be Element of B st b c=f;
end;
theorem
for X be non empty set,F be Filter of X,B be non empty Subset of F holds
F is_coarser_than B iff B is filter_basis
proof
let X be non empty set,F be Filter of X,B be non empty Subset of F;
hereby
assume
A1: F is_coarser_than B;
now
let f be Element of F;
consider b be set such that
A2: b in B and
A3: b c= f by A1;
reconsider b1=b as Element of B by A2;
b1 is Element of B & b1 c= f by A3;
hence ex b be Element of B st b c= f;
end;
hence B is filter_basis;
end;
assume
A4: B is filter_basis;
for f be set st f in F holds ex b be set st b in B & b c= f
proof
let f be set;
assume f in F;
then consider b be Element of B such that
A5: b c= f by A4;
thus thesis by A5;
end;
hence thesis;
end;
registration
let X be non empty set;
let F be Filter of X;
cluster filter_basis for non empty Subset of F;
existence
proof
reconsider F2=F as non empty Subset of F by XBOOLE_0:def 10;
take F2;
thus thesis;
end;
end;
definition
let X be non empty set;
let F be Filter of X;
mode basis of F is filter_basis non empty Subset of F;
end;
theorem Th03:
for X be non empty set,F be Filter of X holds F is basis of F
proof
let X be non empty set,
F be Filter of X;
thus F is filter_basis non empty Subset of F
proof
F is non empty & F c= F;
then reconsider F0=F as non empty Subset of F;
F0 is filter_basis;
hence thesis;
end;
end;
definition
let X be set, B be Subset-Family of X;
func <.B.] -> Subset-Family of X means
:def3:
for x being Subset of X holds x in it iff ex b be Element of B st b c=x;
existence
proof
defpred P[set] means ex b be Element of B st b c= $1;
ex Z being Subset-Family of X st for x being Subset of X holds x in Z iff
P[x] from SUBSET_1:sch 3;
hence thesis;
end;
correctness
proof
let B1,B2 be Subset-Family of X such that
A1: for x being Subset of X holds x in B1 iff
ex b be Element of B st b c= x and
A2: for x being Subset of X holds x in B2 iff
ex b be Element of B st b c= x;
thus B1 c= B2
proof
let x be object;
assume
A3: x in B1;
then reconsider x as Subset of X;
ex b be Element of B st b c= x by A1,A3;
hence thesis by A2;
end;
let x be object;
assume
A4: x in B2;
then reconsider x as Subset of X;
ex b be Element of B st b c= x by A2,A4;
hence thesis by A1;
end;
end;
theorem
for X be set, S be Subset-Family of X holds
<.S.]={x where x is Subset of X: ex b be Element of S st b c= x}
proof
let X be set,S be Subset-Family of X;
set SX={x where x is Subset of X: ex b be Element of S st b c= x};
hereby
let x be object;
assume
A1: x in <.S.];
then reconsider x1=x as Subset of X;
ex b be Element of S st b c= x1 by A1,def3;
hence x in SX;
end;
let x be object;
assume x in SX;
then consider x0 be Subset of X such that
A2: x=x0 and
A3: ex b be Element of S st b c= x0;
reconsider x1=x as Subset of X by A2;
thus x in <.S.] by A2,A3,def3;
end;
theorem
for X be set,B be empty Subset-Family of X holds <.B.]=bool X
proof
let X be set,B be empty Subset-Family of X;
thus <.B.] c= bool X;
let x be object;
assume x in bool X;
then reconsider x0=x as Subset of X;
{} is Element of B & {} c= x0 by SUBSET_1:def 1;
hence x in <.B.] by def3;
end;
theorem
for X be set,B be Subset-Family of X st {} in B holds <.B.]=bool X
proof
let X be set,B be Subset-Family of X;
assume
A1: {} in B;
thus <.B.] c= bool X;
let x be object;
assume x in bool X;
then reconsider x0=x as Subset of X;
{} is Element of B & {} c= x0 by A1;
hence x in <.B.] by def3;
end;
begin :: Filters -- Lattice-theoretical Approach
theorem Th04:
for X be set, B be non empty Subset-Family of X,
L be Subset of BoolePoset X st B=L holds <.B.]=uparrow L
proof
let X be set,B be non empty Subset-Family of X,
L be Subset of BoolePoset X;
assume
A1: B=L;
hereby let x be object;
assume
A2: x in <.B.];
then reconsider x0=x as Subset of X;
consider b be Element of B such that
A3: b c= x0 by A2,def3;
reconsider b1=b as Element of BoolePoset X
by LATTICE3:def 1;
reconsider x1=x0 as Element of BoolePoset X by LATTICE3:def 1;
b1 <= x1 & b1 in L by A3,A1,YELLOW_1:2;
hence x in uparrow L by WAYBEL_0:def 16;
end;
let x be object;
assume
A4B1: x in uparrow L;
then reconsider x0=x as Element of BoolePoset X;
consider y be Element of BoolePoset X such that
A5B2: y <= x0 and
A6B3: y in L by A4B1,WAYBEL_0:def 16;
A7B4: y c= x0 by A5B2,YELLOW_1:2;
x0 is Element of bool X by LATTICE3:def 1;
then reconsider x1=x as Subset of X;
x1 in <.B.] by A1,A6B3,A7B4,def3;
hence x in <.B.];
end;
theorem
for X be set, B be Subset-Family of X holds B c= <.B.] by def3;
definition
let X be set;
let B1,B2 be Subset-Family of X;
pred B1,B2 are_equivalent_generators means
(for b1 be Element of B1 holds ex b2 be Element of B2 st b2 c= b1) &
(for b2 be Element of B2 holds ex b1 be Element of B1 st b1 c= b2);
reflexivity;
symmetry;
end;
theorem Th05:
for X be set,B1,B2 be Subset-Family of X st B1,B2 are_equivalent_generators
holds <.B1.] c= <.B2.]
proof
let X be set,B1,B2 be Subset-Family of X;
assume
A1: B1,B2 are_equivalent_generators;
let x be object;
assume
A2: x in <.B1.];
then reconsider x0=x as Subset of X;
consider b1 be Element of B1 such that
A3: b1 c= x0 by A2,def3;
consider b2 be Element of B2 such that
A4: b2 c= b1 by A1;
b2 c= x0 by A3,A4;
hence thesis by def3;
end;
theorem
for X be set,B1,B2 be Subset-Family of X st
B1,B2 are_equivalent_generators holds <.B1.]=<.B2.] by Th05;
definition
let X be non empty set;
let F be Filter of X;
let B be non empty Subset of F;
func #B -> non empty Subset-Family of X equals
B;
coherence by XBOOLE_1:1;
end;
theorem Th06:
for X be non empty set,F be Filter of X,B be basis of F holds F=<.#B.]
proof
let X be non empty set,F be Filter of X, B be basis of F;
hereby
let x be object;
assume x in F;
then reconsider x0=x as Element of F;
consider b0 be Element of B such that
A1: b0 c= x0 by def2;
reconsider x0 as Subset of X;
thus x in <.#B.] by A1,def3;
end;
let x be object;
assume
A2: x in <.#B.];
then reconsider x0=x as Subset of X;
reconsider B2=#B as Subset-Family of X;
consider b0 be Element of B such that
A3: b0 c= x0 by A2,def3;
thus x in F by A3,CARD_FIL:def 1;
end;
theorem Th07:
for X be non empty set,F be Filter of X,
B be Subset-Family of X st F=<.B.] holds B is basis of F
proof
let X be non empty set,
F be Filter of X,
B be Subset-Family of X;
assume
A1: F=<.B.];
then
A2: B c= F by def3;
B is non empty
proof
assume
A3I1: B is empty;
A4I2A: {} c= X;
{} is Element of B by A3I1,SUBSET_1:def 1;
then {} in <.B.] by A4I2A,def3;
hence contradiction by A1,CARD_FIL:def 1;
end;
then reconsider B1=B as non empty Subset of F by A2;
B1 is filter_basis by A1,def3;
hence thesis;
end;
theorem
for X be non empty set,F be Filter of X,B be basis of F,
S be Subset-Family of X, S1 be Subset of F
st S=S1 & #B,S are_equivalent_generators holds S1 is basis of F
proof
let X be non empty set,F be Filter of X,B be basis of F,
S be Subset-Family of X,
S1 be Subset of F
such that
A1: S=S1 and
A2: #B,S are_equivalent_generators;
<.#B.]=<.S.] by A2,Th05;
hence thesis by A1,Th06,Th07;
end;
theorem
for X be non empty set,F be Filter of X,B1,B2 be basis of F holds
#B1, #B2 are_equivalent_generators
proof
let X be non empty set,F be Filter of X,B1,B2 be basis of F;
hereby
let b1 be Element of #B1;
b1 in #B1;
then b1 in F;
then b1 in <.#B2.] by Th06;
hence ex b2 be Element of #B2 st b2 c= b1 by def3;
end;
let b2 be Element of #B2;
b2 in #B2;
then b2 in F;
then b2 in <.#B1.] by Th06;
hence ex b1 be Element of #B1 st b1 c= b2 by def3;
end;
definition
let X be set;
let B be Subset-Family of X;
attr B is quasi_basis means
:def4:
for b1,b2 be Element of B ex b be Element of B st b c= b1/\b2;
end;
registration
let X be non empty set;
cluster quasi_basis for non empty Subset-Family of X;
existence
proof
take S={X};
thus S is non empty Subset-Family of X by CARD_FIL:2;
reconsider S1=S as Subset-Family of X by CARD_FIL:2;
now
let b1,b2 be Element of S1;
set b=b1/\b2;
b1=X & b2=X by TARSKI:def 1;
hence ex b be Element of S1 st b c= b1/\b2;
end;
then S1 is quasi_basis;
hence thesis;
end;
end;
registration
let X be non empty set;
cluster with_non-empty_elements for non empty quasi_basis Subset-Family of X;
existence
proof
set S={X};
reconsider S1=S as Subset-Family of X by CARD_FIL:2;
now
let b1,b2 be Element of S1;
set b=b1/\b2;
b1=X & b2=X by TARSKI:def 1;
hence ex b be Element of S1 st b c= b1/\b2;
end;
then S1 is quasi_basis;
then reconsider S2=S1 as quasi_basis non empty Subset-Family of X;
S2 is with_non-empty_elements;
hence thesis;
end;
end;
definition
let X be non empty set;
mode filter_base of X is with_non-empty_elements non empty
quasi_basis Subset-Family of X;
end;
theorem Th08:
for X be non empty set,B be filter_base of X holds <.B.] is Filter of X
proof
let X be non empty set, B be filter_base of X;
consider b0 be object such that
A1: b0 in B by XBOOLE_0:def 1;
now
thus <.B.] is non empty by A1,def3;
hereby
assume
A2: {} in <.B.];
then reconsider x0={} as Subset of X;
consider b0 be Element of B such that
A3: b0 c= x0 by A2,def3;
thus not {} in <.B.] by A3;
end;
let Y1,Y2 be Subset of X;
hereby
assume that
A4: Y1 in <.B.] and
A5: Y2 in <.B.];
reconsider y1=Y1,y2=Y2 as Subset of X;
consider b1 be Element of B such that
A6: b1 c= y1 by A4,def3;
consider b2 be Element of B such that
A7: b2 c= y2 by A5,def3;
consider b3 be Element of B such that
A8: b3 c= b1/\b2 by def4;
b1/\b2 c= Y1/\Y2 by A6,A7,XBOOLE_1:27;
then b3 c= Y1/\Y2 by A8;
hence Y1/\Y2 in <.B.] by def3;
end;
assume that
A9: Y1 in <.B.] and
A10: Y1 c= Y2;
reconsider y1=Y1 as Subset of X;
consider b1 be Element of B such that
A11: b1 c= y1 by A9,def3;
b1 c= Y2 by A10,A11;
hence Y2 in <.B.] by def3;
end;
hence thesis by CARD_FIL:def 1;
end;
definition
let X be non empty set,B be filter_base of X;
func <.B.) -> Filter of X equals
<.B.];
coherence by Th08;
end;
theorem
for X be non empty set,B1,B2 be filter_base of X st <.B1.)=<.B2.) holds
B1,B2 are_equivalent_generators
proof
let X be non empty set,B1,B2 be filter_base of X;
assume
A1: <.B1.)=<.B2.);
A2: for b1 be Element of B1 ex b2 be Element of B2 st b2 c= b1
proof
let b1 be Element of B1;
b1 in <.B2.] by A1,def3;
then consider b2 be Element of B2 such that
A3: b2 c= b1 by def3;
thus thesis by A3;
end;
for b2 be Element of B2 ex b1 be Element of B1 st b1 c= b2
proof
let b2 be Element of B2;
b2 in <.B1.] by A1,def3;
then consider b1 be Element of B1 such that
A4: b1 c= b2 by def3;
thus thesis by A4;
end;
hence thesis by A2;
end;
theorem
for X be non empty set, FB be filter_base of X,F be Filter of X st
FB c= F holds <.FB.) is_coarser_than F
proof
let X be non empty set,FB be filter_base of X,F be Filter of X;
assume
A1: FB c= F;
now let x be object;
assume
A2: x in <.FB.);
then reconsider x1=x as Subset of X;
consider b be Element of FB such that
A4: b c= x1 by A2,def3;
A5: b in F by A1;
reconsider x2=x1 as Subset of X;
consider c be Element of F such that
A6: c c= x2 by A4,A5;
thus x in F by A6,CARD_FIL:def 1;
end;
hence thesis;
end;
theorem
for X be non empty set, G be Subset-Family of X st
FinMeetCl G is with_non-empty_elements holds
FinMeetCl G is filter_base of X &
ex F be Filter of X st FinMeetCl G c= F
proof
let X be non empty set,G be Subset-Family of X;
assume
A1: FinMeetCl G is with_non-empty_elements;
reconsider FG=FinMeetCl G as Subset-Family of X;
now
let b1,b2 be Element of FG;
FinMeetCl FG c= FG by CANTOR_1:11;
then FG is cap-closed by Th02;
then reconsider b=b1/\b2 as Element of FG;
b is Element of FG & b c= b1/\b2;
hence ex b be Element of FG st b c= b1/\b2;
end;
then FG is quasi_basis;
then reconsider FG as filter_base of X by A1;
FG c= <.FG.) by def3;
hence thesis;
end;
theorem Th09:
for X be non empty set, F be Filter of X, B be basis of F holds
B is filter_base of X
proof
let X be non empty set, F be Filter of X, B be basis of F;
for b1,b2 be Element of B holds ex b be Element of B st b c= b1/\b2
proof
let b1,b2 be Element of B;
b1/\b2 in F by CARD_FIL:def 1;
then consider b0 be Element of B such that
A1: b0 c= b1/\b2 by def2;
thus thesis by A1;
end;
then
A2: #B is quasi_basis;
B is with_non-empty_elements by CARD_FIL:def 1;
hence thesis by A2;
end;
theorem Th10:
for X be non empty set, B be filter_base of X holds B is basis of <.B.)
proof
let X be non empty set,
B be filter_base of X;
reconsider B2=<.B.) as Filter of X;
B is filter_basis non empty Subset of B2
proof
B is non empty Subset of B2
proof
B c= B2 by def3;
hence thesis;
end;
then reconsider B3=B as non empty Subset of B2;
B3 is filter_basis by def3;
hence thesis;
end;
hence thesis;
end;
theorem
for X be non empty set, F be Filter of X,B be basis of F,
L be Subset of BoolePoset X st L=#B holds F=uparrow L
proof
let X be non empty set,F be Filter of X,B be basis of F,
L be Subset of BoolePoset X;
assume
A1: L=#B;
F=<.#B.] by Th06;
hence F=uparrow L by Th04,A1;
end;
theorem
for X be non empty set, B be filter_base of X,L be Subset of BoolePoset X
st L=B holds <.B.)=uparrow L by Th04;
theorem Th11:
for X be non empty set, F1,F2 be Filter of X,
B1 be basis of F1,B2 be basis of F2 holds
F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2
proof
let X be non empty set,
F1,F2 be Filter of X,
B1 be basis of F1,B2 be basis of F2;
hereby
assume F1 is_filter-coarser_than F2;
then
A1: F1 c= F2;
now
let x be set;
assume x in B1;
then x in F2 by A1;
then ex b be Element of B2 st b c= x by def2;
hence ex y be set st y in B2 & y c= x;
end;
hence B1 is_coarser_than B2;
end;
assume
A2: B1 is_coarser_than B2;
now
let x be object;
assume
A3: x in F1;
then reconsider x1=x as Subset of X;
consider b1 be Element of B1 such that
A4: b1 c= x1 by A3,def2;
consider b2 be set such that
A5: b2 in B2 and
A6: b2 c= b1 by A2;
reconsider b2 as Element of B2 by A5;
A7: b2 c= x1 by A4,A6;
x1 in <.#B2.] by A7,def3;
hence x in F2 by Th06;
end;
then F1 c= F2;
hence F1 is_filter-coarser_than F2;
end;
theorem Th12:
for X,Y be non empty set,f be Function of X,Y,
F be Filter of X, B be basis of F holds
f.:( #B ) is filter_base of Y &
<.(f.:( #B )).] is Filter of Y &
<.(f.:( #B )).] = { M where M is Subset of Y: f"(M) in F}
proof
let X,Y be non empty set,f be Function of X,Y,
F be Filter of X,B be basis of F;
set FB=f.:( #B );
now
set b0 = the Element of B;
f.:b0 in FB by FUNCT_2:def 10;
hence FB is non empty;
end;
then reconsider FB1=FB as non empty Subset-Family of Y;
A1: FB is quasi_basis non empty Subset-Family of Y
proof
now
let b1,b2 be Element of FB;
b1 in FB1;
then consider M be Subset of X such that
A2: M in #B and
A3: b1=f.:M by FUNCT_2:def 10;
b2 in FB1;
then
consider N be Subset of X such that
A4: N in #B and
A5: b2=f.:N by FUNCT_2:def 10;
#B is quasi_basis & M in #B & N in #B by A2,A4,Th09;
then consider P be Element of B such that
A6: P c= M/\N;
A7: f.:P c= f.:(M /\ N) by A6,RELAT_1:123;
f.:(M /\ N) c=f.:M /\ f.:N by RELAT_1:121;
then
A8: f.:P c= b1 /\ b2 by A3,A5,A7;
f.:P is Element of FB by FUNCT_2:def 10;
hence ex b be Element of FB st b c= b1/\b2 by A8;
end;
then FB1 is quasi_basis;
hence thesis;
end;
A9: FB is with_non-empty_elements
proof
assume not FB is with_non-empty_elements;
then consider x be Subset of X such that
A10: x in #B and
A11: {} = f.:x by FUNCT_2:def 10;
dom f = X by FUNCT_2:def 1;
then X misses x by A11,RELAT_1:118;
then {} in B by A10,XBOOLE_1:67;
hence contradiction by CARD_FIL:def 1;
end;
hence FB is filter_base of Y by A1;
thus <.FB.] is Filter of Y by A1,A9,Th08;
thus <.FB.] = { M where M is Subset of Y: f"(M) in F}
proof
hereby
let y be object;
assume
A12: y in <.FB.];
then reconsider y0=y as Subset of Y;
consider b be Element of FB such that
A13: b c= y0 by A12,def3;
b in FB1;
then
consider M be Subset of X such that
A14: M in #B and
A15: b=f.:M by FUNCT_2:def 10;
A16: f"(f.:M) c= f"(y0) by A13,A15,RELAT_1:143;
M c= f"(f.:M) by FUNCT_2:42;
then M c= f"(y0) by A16;
then f"(y0) in <.#B.] by A14,def3;
then f"(y0) in F by Th06;
hence y in { M where M is Subset of Y: f"(M) in F};
end;
let x be object;
assume x in { M where M is Subset of Y: f"(M) in F};
then consider M0 be Subset of Y such that
A17: x=M0 and
A18: f"(M0) in F;
f"(M0) in <.#B.] by A18,Th06;
then consider b0 be Element of #B such that
A19: b0 c= f"(M0) by def3;
A20: f.:b0 c= f.:(f"(M0)) by A19,RELAT_1:123;
reconsider fb=f.:b0 as Element of FB by FUNCT_2:def 10;
f.:(f"(M0)) c= M0 by FUNCT_1:75;
then fb c= M0 by A20;
hence x in <.FB.] by A17,def3;
end;
end;
definition
let X,Y be non empty set,f be Function of X,Y,
F be Filter of X;
func filter_image(f,F) -> Filter of Y equals
{M where M is Subset of Y : f"(M) in F};
correctness
proof
reconsider F0=F as basis of F by Th03;
<.(f.:( #F0 )).] is Filter of Y &
<.(f.:( #F0 )).] = { M where M is Subset of Y: f"(M) in F} by Th12;
hence thesis;
end;
end;
theorem Th13:
for X,Y be non empty set,f be Function of X,Y,
F be Filter of X holds f.:F is filter_base of Y &
<.f.:F.]=filter_image(f,F)
proof
let X,Y be non empty set,f be Function of X,Y,F be Filter of X;
reconsider F1=F as basis of F by Th03;
f.:( #F1 ) is filter_base of Y &
<.f.:( #F1 ).]=filter_image(f,F) by Th12;
hence thesis;
end;
theorem
for X be non empty set, B be filter_base of X st B=<.B.) holds
B is Filter of X;
theorem Th13bThmBA2:
for X,Y be non empty set, f be Function of X,Y,
F be Filter of X, B be basis of F holds
f.:#B is basis of filter_image(f,F) &
<.f.:( #B ).] = filter_image(f,F)
proof
let X,Y be non empty set,f be Function of X,Y,
F be Filter of X,B be basis of F;
reconsider FB=f.:( #B ) as filter_base of Y by Th12;
reconsider FB2=<.FB.) as Filter of Y;
FB2=filter_image(f,F) by Th12;
hence thesis by Th10;
end;
theorem
for X,Y be non empty set, f be Function of X,Y,
B1,B2 be filter_base of X st B1 is_coarser_than B2
holds <.B1.) is_filter-coarser_than <.B2.)
proof
let X,Y be non empty set, f be Function of X,Y,
B1,B2 be filter_base of X;
assume
A1: B1 is_coarser_than B2;
B1 is basis of <.B1.) & B2 is basis of <.B2.) by Th10;
hence thesis by A1,Th11;
end;
theorem
for X,Y be non empty set, f be Function of X,Y,
F be Filter of X holds f.:F is Filter of Y iff Y = rng f
proof
let X,Y be non empty set,f be Function of X,Y,
F be Filter of X;
hereby
assume f.:F is Filter of Y;
then Y in f.:F by CARD_FIL:5;
then consider B being Subset of X such that
B in F and
A1: Y = f.:B by FUNCT_2:def 10;
now
let y be object;
assume y in Y;
then consider x being object such that
A2: x in dom f and
x in B and
A3: y=f.x by A1,FUNCT_1:def 6;
thus y in rng f by A2,A3,FUNCT_1:def 3;
end;
then Y c= rng f;
hence Y=rng f; end;
assume
A4: Y = rng f;
reconsider fF=f.:F as filter_base of Y by Th13;
A5: fF c= <.fF.) by def3;
<.fF.) c= fF
proof
let x be object;
assume
A6: x in <.fF.);
then reconsider x1=x as Subset of Y;
consider b2 be Element of fF such that
A7: b2 c= x1 by A6,def3;
consider bx being Subset of X such that
A8: bx in F and
A9: b2=f.:bx by FUNCT_2:def 10;
reconsider fx1=f"(x1) as Subset of X;
A10: dom f = X by FUNCT_2:def 1;
A11: f"(f.:bx) c= f"(x1) by A7,A9,RELAT_1:143;
bx c= f"(f.:bx) by A10,FUNCT_1:76;
then
bx c= f"(x1) by A11;
then fx1 in F by A8,CARD_FIL:def 1;
then f.:fx1 in fF by FUNCT_2:def 10;
hence thesis by A4,FUNCT_1:77;
end;
then fF=<.fF.) by A5;
hence thesis;
end;
theorem
for X be non empty set, A be non empty Subset of X holds for
F be Filter of A, B be basis of F holds
(incl A).:( #B ) is filter_base of X &
<.((incl A).:( #B )).] is Filter of X &
<.((incl A).:( #B )).]= { M where M is Subset of X: (incl A)"(M) in F}
by Th12;
definition
let L be non empty RelStr;
func Tails L -> non empty Subset-Family of L equals
the set of all uparrow i where i is Element of L;
coherence
proof
A1: the set of all uparrow i where i is Element of L is non empty
proof
set l0=the Element of L;
take uparrow the Element of L;
thus thesis;
end;
the set of all uparrow i where i is Element of L c= bool the carrier of L
proof
let t be object;
assume t in the set of all uparrow i where i is Element of L;
then consider i0 be Element of L such that
A2: t=uparrow i0;
thus thesis by A2;
end;
hence thesis by A1;
end;
end;
theorem Th14:
for L be non empty transitive reflexive RelStr st [#]L is directed
holds <.Tails L.] is Filter of [#]L
proof
let L be non empty transitive reflexive RelStr;
assume
A1: [#]L is directed;
Tails L is non empty Subset-Family of L &
Tails L is with_non-empty_elements &
Tails L is quasi_basis
proof
A2: Tails L is with_non-empty_elements
proof
assume not Tails L is with_non-empty_elements;
then consider i0 be Element of L such that
A3: {}=uparrow i0;
thus contradiction by A3;
end;
(for x,y be Element of Tails L
ex z be Element of Tails L st z c= x/\y)
proof
let x,y be Element of Tails L;
x in Tails L;
then consider lx be Element of L such that
A4: x=uparrow lx;
y in Tails L;
then consider ly be Element of L such that
A5: y=uparrow ly;
consider lz be Element of L such that
lz in the carrier of L and
A6: lx <= lz and
A7: ly <= lz by A1;
set z=uparrow lz;
z in Tails L;
then reconsider z as Element of Tails L;
take z;
uparrow lz c= uparrow lx & uparrow lz c= uparrow ly
by A6,A7,WAYBEL_0:22;
hence thesis by A4,A5,XBOOLE_1:19;
end;
hence thesis by A2;
end;
hence thesis by Th08;
end;
definition
let L be non empty transitive reflexive RelStr;
assume
A1:[#]L is directed;
func Tails_Filter(L) -> Filter of [#]L equals
:DefL9:
<.Tails L.];
coherence by A1,Th14;
end;
theorem Th15:
for L be non empty transitive reflexive RelStr
st [#]L is directed holds
Tails L is basis of Tails_Filter(L)
proof
let L be non empty transitive reflexive RelStr;
assume [#]L is directed;
then Tails_Filter(L)=<.Tails L.] by DefL9;
hence thesis by Th07;
end;
definition
let L be RelStr;
let x be Subset-Family of L;
func #x -> Subset-Family of [#]L equals
x;
coherence;
end;
theorem Th16:
for X be non empty set,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,X st [#]L is directed
holds
f.:#(Tails L) is basis of filter_image(f,Tails_Filter(L))
proof
let X be non empty set,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,X such that A1: [#]L is directed;
reconsider SL = Tails(L) as basis of Tails_Filter(L)
by A1,Th15;
f.:#SL is basis of filter_image(f,Tails_Filter(L)) by Th13bThmBA2;
hence thesis;
end;
theorem Th17:
for X be non empty set, L be non empty transitive reflexive RelStr,
f be Function of [#]L,X, x be Subset of X st [#]L is directed
& x in f.:#(Tails L) holds
ex j be Element of L st for i be Element of L st i >= j holds f.i in x
proof
let X be non empty set,L be non empty transitive reflexive RelStr,
f be Function of [#]L,X, x be Subset of X;
assume that [#]L is directed and
A2: x in f.:#(Tails L);
reconsider x0=x as Subset of X;
consider b0 be Subset of [#]L such that
A3: b0 in #(Tails L) and
A4: x0=f.:b0 by A2,FUNCT_2:def 10;
consider i be Element of L such that
A5: b0=uparrow i by A3;
now
let j be Element of L;
assume j >= i;
then C1: i <= j & i in {i} by TARSKI:def 1;
j in [#]L;
then j in uparrow i & j in dom f by C1,WAYBEL_0:def 16,FUNCT_2:def 1;
hence f.j in x by A4,A5,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th18:
for X be non empty set, L be non empty transitive reflexive RelStr,
f be Function of [#]L,X, x be Subset of X st [#]L is directed
& (ex j be Element of L st for i be Element of L st i >= j holds f.i in x)
holds ex b be Element of Tails L st f.:b c= x
proof
let X be non empty set,L be non empty transitive reflexive RelStr,
f be Function of [#]L,X, x be Subset of X;
assume that [#]L is directed and
A1: ex j be Element of L st for i be Element of L st i >=j holds f.i in x;
consider j0 be Element of L such that
A2: for i be Element of L st i >=j0 holds f.i in x by A1;
set b0=uparrow {j0};
b0=uparrow j0;
then
A3: b0 in #(Tails L);
now
let t be object;
assume t in f.:b0;
then consider x0 be object such that
A4: x0 in dom f and
A5: x0 in uparrow j0 and
A6: t=f.x0 by FUNCT_1:def 6;
reconsider x1=x0 as Element of L by A4;
consider y1 be Element of L such that
A7: y1<= x1 and
A8: y1 in {j0} by A5,WAYBEL_0:def 16;
y1=j0 by A8,TARSKI:def 1;
hence t in x by A2,A6,A7;
end;
then f.:b0 c= x;
hence thesis by A3;
end;
theorem Th19:
for X be non empty set,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,X,
F be Filter of X, B be basis of F st [#]L is directed holds
F is_filter-coarser_than filter_image(f,Tails_Filter(L)) iff
B is_coarser_than f.:#(Tails L)
proof
let X be non empty set,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,X,
F be Filter of X, B be basis of F;
assume [#]L is directed;
then f.:#(Tails L) is basis of filter_image(f,Tails_Filter(L))
by Th16;
hence thesis by Th11;
end;
theorem Th20:
for X be non empty set,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,X,
B be filter_base of X st [#]L is directed holds
B is_coarser_than f.:#(Tails L) iff
for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b
proof
let X be non empty set, L be non empty transitive reflexive RelStr,
f be Function of [#]L,X,
B be filter_base of X;
assume
A1: [#]L is directed;
hereby
assume
A2: B is_coarser_than f.:#(Tails L);
hereby
let b be Element of B;
consider x0 be set such that
A3: x0 in f.:#(Tails L) and
A4: x0 c= b by A2;
reconsider x1=x0 as Subset of X by A4,XBOOLE_1:1;
consider j0 be Element of L such that
A5: for i be Element of L st i>=j0 holds f.i in x1 by A1,A3,Th17;
for i be Element of L st i >=j0 holds f.i in b by A4,A5;
hence ex i be Element of L st
for j be Element of L st i <=j holds f.j in b;
end;
end;
assume
A6: for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b;
now
let Y be set;
assume
A7: Y in B;
then consider i0 be Element of L such that
A8: for j be Element of L st i0 <= j holds f.j in Y by A6;
reconsider b=Y as Subset of X by A7;
consider b0 be Element of Tails L such that
A9: f.:b0 c= b by A1,A8,Th18;
f.:b0 in f.:#(Tails L) by FUNCT_2:def 10;
hence ex X be set st X in f.:#(Tails L) & X c= Y by A9;
end;
hence B is_coarser_than f.:#(Tails L);
end;
definition
let X be non empty set,
s be sequence of X;
func elementary_filter(s) -> Filter of X equals
filter_image(s,Frechet_Filter(NAT));
correctness;
end;
theorem Th21:
ex F be sequence of bool NAT st
for x be Element of NAT holds F.x = {y where y is Element of NAT:x <= y}
proof
deffunc FF(object)={y where y is Element of NAT:ex x0 be Element of NAT
st x0=$1 & x0 <= y};
A1: now
let x be object;
assume x in NAT;
now
let t be object;
assume t in {y where y is Element of NAT:ex x0 be Element of NAT st
x0=x & x0 <= y};
then consider y0 be Element of NAT such that
A2: t=y0 and
ex x0 be Element of NAT st x0=x & x0 <=y0;
thus t in NAT by A2;
end;
then {y where y is Element of NAT:ex x0 be Element of NAT st
x0=x & x0 <= y} c= NAT;
hence FF(x) in bool NAT;
end;
ex f being Function of NAT,bool NAT st
for x being object st x in NAT holds f.x=FF(x) from FUNCT_2:sch 2(A1);
then consider F being Function of NAT,bool NAT such that
A3: for x being object st x in NAT holds F.x=FF(x);
for x be Element of NAT holds F.x = {y where y is Element of NAT:x <=y}
proof
let x be Element of NAT;
{y where y is Element of NAT:ex x0 be Element of NAT st x0=x & x0 <= y}=
{y where y is Element of NAT:x <= y}
proof
hereby let t be object;assume t in
{y where y is Element of NAT:ex x0 be Element of NAT st x0=x &
x0 <= y};
then consider y0 be Element of NAT such that
A4: t=y0 and
A5: ex x0 be Element of NAT st x0=x & x0 <= y0;
consider x1 be Element of NAT such that
A6: x1=x and
A7: x1 <= y0 by A5;
thus t in {y where y is Element of NAT:x <= y} by A4,A6,A7;
end;
let t be object;assume t in {y where y is Element of NAT:x <= y};
then consider y0 be Element of NAT such that
A8: t=y0 and
A9: x <= y0;
thus t in {y where y is Element of NAT:ex x0 be Element of NAT st
x0=x & x0 <= y} by A8,A9;
end;
hence thesis by A3;
end;
hence thesis;
end;
theorem Th22:
for n be natural number holds
NAT\{t where t is Element of NAT:n <= t} is finite
proof
let n be natural number;
NAT\{t where t is Element of NAT:n <= t} c= n+1
proof
NAT\{t where t is Element of NAT:n <= t} c= Seg n \/{0}
proof
set S= NAT\{t where t is Element of NAT:n <= t};
per cases;
suppose
A1: n=0;
S is empty
proof
let x be object such that
A2: x in S;
x in NAT & not x in {t where t is Element of NAT:0<=t}
by A1,A2,XBOOLE_0:def 5;
hence thesis;
end;
hence thesis;
end;
suppose
n>0;
let x be object such that
A3: x in S;
A4: x in NAT & not x in {t where t is Element of NAT:n<=t}
by A3,XBOOLE_0:def 5;
reconsider x as Element of NAT by A3;
A5: x=0 or x in Seg x by FINSEQ_1:3;
x <= n by A4;
then Seg x c= Seg n by FINSEQ_1:5;
then x in {0} or x in Seg n by A5,TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by AFINSQ_1:4;
end;
hence thesis;
end;
Lm3:
for p be Element of OrderedNAT,p0 be Element of NAT st p=p0 holds
{x where x is Element of NAT:p0 <= x}=
{x where x is Element of OrderedNAT: p <= x}
proof
let p be Element of OrderedNAT,p0 be Element of NAT;
assume
A1: p=p0;
hereby
let t be object;
assume t in {x where x is Element of NAT:p0 <= x};
then consider x0 be Element of NAT such that
A2: t=x0 and
A3: p0<=x0;
reconsider x1=x0 as Element of OrderedNAT;
p <= x1 by A3,A1;
hence t in {x where x is Element of OrderedNAT:p <= x} by A2;
end;
let t be object;
assume t in {x where x is Element of OrderedNAT:p <= x};
then consider x0 be Element of OrderedNAT such that
A4: t=x0 and
A5: p<=x0;
consider a,b be Element of NAT such that
A6: [p0,x0]=[a,b] and
A7: a <= b by A1,A5;
p0=a & x0=b by A6,XTUPLE_0:1;
hence t in {x where x is Element of NAT: p0 <= x} by A4,A7;
end;
Lm4:
for p be Element of OrderedNAT holds
{x where x is Element of NAT:ex p0 be Element of NAT st
p=p0 & p0 <= x}=
{x where x is Element of OrderedNAT:p <= x}
proof
let p be Element of OrderedNAT;
hereby
let t be object;
assume t in {x where x is Element of NAT:ex p0 be Element of NAT st
p=p0 & p0 <= x};
then consider x0 be Element of NAT such that
A1: t=x0 and
A2: ex p0 be Element of NAT st p=p0 & p0<=x0;
consider p0 be Element of NAT such that
A3: p=p0 and
A4: p0 <= x0 by A2;
reconsider x1=x0 as Element of OrderedNAT;
p <= x1 by A4,A3;
hence t in {x where x is Element of OrderedNAT:p <= x} by A1;
end;
let t be object;assume t in {x where x is Element of OrderedNAT:p <= x};
then consider x0 be Element of OrderedNAT such that
A5: t=x0 and
A6: p<=x0;
reconsider p0=p as Element of NAT;
consider a,b be Element of NAT such that
A7: [p0,x0]=[a,b] and
A8: a <= b by A6;
p0=a & x0=b by A7,XTUPLE_0:1;
hence t in {x where x is Element of NAT:ex p0 be Element of NAT st
p=p0 & p0 <= x} by A5,A8;
end;
theorem Th23:
for p be Element of OrderedNAT holds
{x where x is Element of NAT:ex p0 be Element of NAT st
p=p0 & p0 <= x}=uparrow p
proof
let p be Element of OrderedNAT;
reconsider p0=p as Element of NAT;
A1: for p be Element of the carrier of OrderedNAT holds
{x where x is Element of the carrier of OrderedNAT:p <= x}=uparrow p
proof
let p be Element of OrderedNAT;
hereby
let t be object;
assume t in {x where x is Element of OrderedNAT:p <=x};
then consider x0 be Element of OrderedNAT such that
A2: t=x0 and
A3: p <= x0;
thus t in uparrow p by A2,A3,WAYBEL_0:18;
end;
let t be object;
assume
A4: t in uparrow p;
then reconsider t0=t as Element of OrderedNAT;
p <= t0 by A4,WAYBEL_0:18;
hence t in {x where x is Element of OrderedNAT:p <=x};
end;
{x where x is Element of NAT:ex p0 be Element of NAT st
p=p0 & p0 <= x} = {x where x is Element of OrderedNAT:p <= x} by Lm4;
hence thesis by A1;
end;
registration
cluster [#]OrderedNAT -> directed;
coherence;
cluster OrderedNAT -> reflexive;
coherence by DICKSON:def 3;
end;
theorem Th24:
for X be denumerable set holds
Frechet_Filter (X) = the set of all X\A where A is finite Subset of X
proof
let X be denumerable set;
A1: card X = omega by CARD_3:def 15;
hereby
let x be object such that
A2: x in Frechet_Filter(X);
reconsider x0=x as Subset of X by A2;
card(X \ x0) in card X by A2,CARD_FIL:18;
then
A3: X \ x0 is finite Subset of X by A1;
X \ ( X \x0 )= X /\ x0 & X /\x0 c= X by XBOOLE_1:48;
then X \ (X \ x0)=x0 by XBOOLE_1:28;
hence x in the set of all X\A where A is finite Subset of X by A3;
end;
let x be object such that
A4: x in the set of all X\A where A is finite Subset of X;
consider a0 be finite Subset of X such that
A5: x=X \ a0 by A4;
reconsider x0=x as Subset of X by A5;
X\(X\a0) = X/\a0 & X/\a0 c= X by XBOOLE_1:48;
then card (X \ x0) = card a0 by A5,XBOOLE_1:28;
hence thesis by A1;
end;
theorem Th25:
for F be sequence of bool NAT st
for x be Element of NAT holds F.x = {y where y is Element of NAT:x <= y}
holds rng F is basis of Frechet_Filter(NAT)
proof
let F be sequence of bool NAT;
assume
A1: for x be Element of NAT holds
F.x = {y where y is Element of NAT:x <= y};
A2: Frechet_Filter(NAT)=the set of all NAT\A where
A is finite Subset of NAT by Th24;
for t be object st t in rng F holds t in Frechet_Filter(NAT)
proof
let t be object;
assume
A3: t in rng F;
then consider x0 be object such that
A4: x0 in dom F & t=F.x0 by FUNCT_1:def 3;
reconsider x2=x0 as natural number by A4;
reconsider t1=t as Subset of NAT by A3;
A5: now
NAT\t1=NAT\{y where y is Element of NAT:x2<=y} by A1,A4;
hence NAT\t1 is finite by Th22;
thus NAT\t1 is Subset of NAT;
end;
NAT\(NAT\t1)=t1/\NAT by XBOOLE_1:48;
then t1=NAT\(NAT\t1) by XBOOLE_1:17,XBOOLE_1:19;
hence thesis by A2,A5;
end;
then rng F c= Frechet_Filter(NAT);
then reconsider F1=rng F as non empty Subset of Frechet_Filter(NAT);
A7: F1 is filter_basis
proof
for f be Element of Frechet_Filter(NAT) holds
ex b be Element of F1 st b c= f
proof
let f be Element of Frechet_Filter(NAT);
f in the set of all NAT\A where A is finite Subset of NAT by A2;
then consider A0 be finite Subset of NAT such that
A8: f=NAT\A0;
reconsider A1=A0 as natural-membered set;
consider n0 be natural number such that
A9: A1 c= Segm n0 by AFINSQ_2:2;
reconsider n1=n0 as Element of NAT by ORDINAL1:def 12;
A10: dom F = NAT by FUNCT_2:def 1;
set b=NAT\Segm n0;
b is Element of rng F
proof
b={y where y is Element of NAT: n0 <= y}
proof
hereby
let x be object;
assume
A11: x in b;
then reconsider x1=x as Element of NAT;
for n0 be natural number,t be Element of NAT\Segm n0
holds n0 <= t
proof
let n0 be natural number,
t be Element of NAT\Segm n0;
Segm n0 c< NAT;
then NAT\Segm n0 is non empty by XBOOLE_1:105;
then not t in Segm n0 by XBOOLE_0:def 5;
hence thesis by NAT_1:44;
end;
then n0 <= x1 by A11;
hence x in {y where y is Element of NAT:n0 <=y};
end;
let x be object;
assume x in {y where y is Element of NAT:n0 <= y};
then consider y0 be Element of NAT such that
A12: x=y0 and
A13: n0 <= y0;
reconsider x1=x as Element of NAT by A12;
x1 in NAT & not x1 in Segm n0 by A12,A13,NAT_1:44;
hence x in b by XBOOLE_0:def 5;
end;
then b=F.n1 by A1;
hence thesis by A10,FUNCT_1:3;
end;
hence thesis by A8,A9,XBOOLE_1:34;
end;
hence thesis;
end;
thus thesis by A7;
end;
theorem Th26:
for F be sequence of bool NAT st
for x be Element of NAT holds F.x={y where y is Element of NAT:x <= y} holds
#(Tails OrderedNAT)=rng F
proof
let F be sequence of bool NAT such that
A1: for x be Element of NAT holds F.x =
{y where y is Element of NAT:x <= y};
set F1=rng F;
set F2=the set of all uparrow p where p is Element of OrderedNAT;
now
hereby
let t be object;
assume t in F1;
then consider x0 be object such that
A2: x0 in dom F & t=F.x0 by FUNCT_1:def 3;
reconsider x1=x0 as Element of NAT by A2;
reconsider x2=x0 as Element of OrderedNAT by A2;
t={y where y is Element of NAT:x1 <= y} by A1,A2;
then t={x where x is Element of OrderedNAT: x2 <= x} by Lm3;
then t={x where x is Element of NAT:ex p0 be Element of NAT st
x2=p0 & p0 <= x} by Lm4;
then t=uparrow x2 by Th23;
hence t in F2;
end;
let t be object;
assume t in F2;
then consider p0 be Element of OrderedNAT such that
A3: t=uparrow p0;
t={x where x is Element of NAT:ex p1 be Element of NAT st
p0=p1 & p1 <= x} by A3,Th23;
then
A4: t={y where y is Element of OrderedNAT:p0<=y} by Lm4;
reconsider p2=p0 as Element of NAT;
t={x where x is Element of NAT:p2 <= x} by A4,Lm3;
then
A5: t = F.p2 by A1;
dom F=NAT by FUNCT_2:def 1;
hence t in F1 by A5,FUNCT_1:3;
end;
then F1 c= F2 & F2 c= F1;
hence thesis;
end;
theorem Th27:
#(Tails OrderedNAT) is basis of Frechet_Filter(NAT) &
Tails_Filter(OrderedNAT)=Frechet_Filter(NAT)
proof
consider F be sequence of bool NAT such that
A1: for x be Element of NAT holds F.x =
{y where y is Element of NAT:x <= y} by Th21;
set F1=rng F;
set F2=the set of all uparrow p where p is Element of OrderedNAT;
A2: F1=F2 by A1,Th26;
hence #(Tails OrderedNAT) is basis of Frechet_Filter(NAT)
by A1,Th25;
reconsider BFF=#(Tails OrderedNAT) as
basis of Frechet_Filter(NAT) by A1,A2,Th25;
<.#BFF.]=Frechet_Filter(NAT) by Th06;
hence thesis by DefL9;
end;
definition
func base_of_frechet_filter -> filter_base of NAT equals
#(Tails OrderedNAT);
coherence by Th27,Th09;
end;
theorem
NAT in base_of_frechet_filter
proof
reconsider n0=0 as Element of OrderedNAT;
A1: uparrow n0=uparrow {n0};
uparrow {n0}=NAT
proof
NAT c= uparrow {n0}
proof
let t be object;
assume
t in NAT;
then reconsider t0=t as Element of OrderedNAT;
n0 <= t0 & n0 in {n0} by TARSKI:def 1;
hence thesis by WAYBEL_0:def 16;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem
base_of_frechet_filter is basis of Frechet_Filter(NAT) by Th27;
theorem
for X be non empty set,F1,F2 be Filter of X, F be Filter of X st
F is_filter-finer_than F1 & F is_filter-finer_than F2 holds
for M1 be Element of F1,M2 be Element of F2 holds M1/\M2 is non empty
proof
let X be non empty set,F1,F2 be Filter of X, F be Filter of X such that
A1: F is_filter-finer_than F1 and
A2: F is_filter-finer_than F2;
hereby
let M1 be Element of F1,M2 be Element of F2;
M1 in F1 & M2 in F2;
then M1/\M2 in F by A1,A2,CARD_FIL:def 1;
hence M1/\M2 is non empty by CARD_FIL:def 1;
end;
end;
theorem
for X be non empty set,F1,F2 be Filter of X st
for M1 be Element of F1,M2 be Element of F2 holds M1/\M2 is non empty
holds
ex F be Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2
proof
let X be non empty set,F1,F2 be Filter of X;
assume
A1: for M1 be Element of F1,M2 be Element of F2 holds
M1/\M2 is non empty;
set F=the set of all M1/\M2 where M1 is Element of F1,M2 is Element of F2;
take F;
F is non empty Subset-Family of X
proof
set M1=the Element of F1;
set M2=the Element of F2;
A2: M1/\M2 in F;
F c= bool X
proof
let x be object;
assume x in F;
then
consider M1 be Element of F1,M2 be Element of F2 such that
A3: x=M1/\M2;
thus x in bool X by A3;
end;
hence thesis by A2;
end;
then reconsider F as non empty Subset-Family of X;
now
hereby
assume {} in F;
then consider M1 be Element of F1,M2 be Element of F2 such that
A4: {}=M1/\M2;
thus not {} in F by A4,A1;
end;
hereby
let Y1,Y2 be Subset of X;
hereby
assume that
A5: Y1 in F and
A6: Y2 in F;
consider M1 be Element of F1,M2 be Element of F2 such that
A7: Y1=M1/\M2 by A5;
consider M3 be Element of F1,M4 be Element of F2 such that
A8: Y2=M3/\M4 by A6;
Y1/\Y2=M1/\(M2/\(M3/\M4)) by A7,A8,XBOOLE_1:16;
then Y1/\Y2=M1/\(M3/\(M4/\M2)) by XBOOLE_1:16;
then
A9: Y1 /\ Y2 = (M1/\M3)/\(M2/\M4) by XBOOLE_1:16;
M1/\M3 is Element of F1 & M2/\M4 is Element of F2 by CARD_FIL:def 1;
hence Y1 /\ Y2 in F by A9;
end;
assume that
A10: Y1 in F and
A11: Y1 c= Y2;
consider M1 be Element of F1,M2 be Element of F2 such that
A12: Y1=M1/\M2 by A10;
Y2\/(M1/\M2)=Y2 by A11,A12,XBOOLE_1:12;
then
A13: Y2=(M1\/Y2)/\(M2\/Y2) by XBOOLE_1:24;
M1 c= M1\/Y2 & M2 c= M2\/Y2 by XBOOLE_1:7;
then M1\/Y2 is Element of F1 & M2\/Y2 is Element of F2
by CARD_FIL:def 1;
hence Y2 in F by A13;
end;
end;
then reconsider F0=F as Filter of X by CARD_FIL:def 1;
A14:
X in F1 & X in F2 by CARD_FIL:5;
F1 c= F0
proof
let x be object;
assume
A15: x in F1;
then reconsider x as Subset of X;
x=x/\X by XBOOLE_1:17,XBOOLE_1:19;
hence thesis by A14,A15;
end;
then
A16:F0 is_filter-finer_than F1;
F2 c= F0
proof
let x be object;
assume
A17: x in F2;
then reconsider x as Subset of X;
x=x/\X by XBOOLE_1:17,XBOOLE_1:19;
hence thesis by A14,A17;
end;
then F0 is_filter-finer_than F2;
hence thesis by A16;
end;
definition
let X be set;
let x be Subset of X;
func PLO2bis(x) -> Element of BoolePoset X equals
x;
coherence by LATTICE3:def 1;
end;
theorem Th28:
for X being infinite set holds
X in the set of all X\A where A is finite Subset of X
proof
let X be infinite set;
set Z={};
Z is finite Subset of X
proof
{} c= X;
hence thesis;
end;
then reconsider Z as finite Subset of X;
X\Z in {X\A where A is finite Subset of X:not contradiction};
hence thesis;
end;
theorem Th29:
for X be set, A be Subset of X holds
{B where B is Element of BoolePoset X: A c= B} =
{B where B is Subset of X: A c= B}
proof
let X be set, A be Subset of X;
set C = {B where B is Element of BoolePoset X: A c= B};
set D = {B where B is Subset of X: A c= B};
now
hereby
let x be object;
assume x in C;
then consider b0 be Element of BoolePoset X such that
A1: x=b0 and
A2: A c= b0;
x is Subset of X by A1,WAYBEL_8:26;
hence x in D by A1,A2;
end;
let x be object;
assume x in D;
then consider b0 be Subset of X such that
A3: x=b0 and
A4: A c= b0;
x is Element of BoolePoset X by A3,WAYBEL_8:26;
hence x in C by A3,A4;
end;
then C c= D & D c= C;
hence thesis;
end;
theorem
for X be set,a be Element of BoolePoset X holds
uparrow a = {Y where Y is Subset of X : a c=Y} by WAYBEL15:2;
theorem
for X be set, A be Subset of X holds
{B where B is Element of BoolePoset X: A c= B} =
uparrow PLO2bis A
proof
let X be set,A be Subset of X;
reconsider Z=PLO2bis A as Element of BoolePoset X;
set S1={Y where Y is Subset of X : Z c=Y};
set S2={B where B is Subset of X: A c= B};
{B where B is Element of BoolePoset X: A c= B} =
{B where B is Subset of X: A c= B} by Th29;
hence thesis by WAYBEL15:2;
end;
theorem
for X be non empty set, F be Filter of X holds
union F = X by CARD_FIL:5,ZFMISC_1:74;
theorem
for X be infinite set holds
the set of all X\A where A is finite Subset of X is Filter of X
proof
let X be infinite set;
set FF=the set of all X\A where A is finite Subset of X;
now
let x be object;
assume x in FF;
then consider a1 be finite Subset of X such that
A1: x=X\a1;
thus x in bool X by A1;
end;
then FF c= bool X;
then reconsider FF as non empty Subset-Family of X by Th28;
A2: not {} in FF
proof
assume {} in FF;
then consider a be finite Subset of X such that
A3: {}=X\a;
X c= a by A3,XBOOLE_1:37;
hence contradiction;
end;
A4: for Y1,Y2 be Subset of X st Y1 in FF & Y2 in FF holds
Y1/\Y2 in FF
proof
let Y1,Y2 be Subset of X such that
A5: Y1 in FF and
A6: Y2 in FF;
consider a1 be finite Subset of X such that
A7: Y1=X\a1 by A5;
consider a2 be finite Subset of X such that
A8: Y2=X\a2 by A6;
Y1/\Y2=X\(a1\/a2) by A7,A8,XBOOLE_1:53;
hence thesis;
end;
for Y1,Y2 be Subset of X st Y1 in FF & Y1 c= Y2 holds Y2 in FF
proof
let Y1,Y2 be Subset of X such that
A9: Y1 in FF and
A10: Y1 c= Y2;
consider a1 be finite Subset of X such that
A11: Y1=X\a1 by A9;
X\Y2 c= X\(X\a1) by A10,A11,XBOOLE_1:34;
then
A12: X\Y2 c= X/\a1 by XBOOLE_1:48;
X\(X\Y2)=X/\Y2 & X/\Y2 c= Y2 by XBOOLE_1:17,XBOOLE_1:48;
then
X\(X\Y2) = Y2 by XBOOLE_1:28;
hence thesis by A12;
end;
hence thesis by A2,A4,CARD_FIL:def 1;
end;
theorem
for X being set holds bool X is Filter of BoolePoset X by WAYBEL16:11;
theorem
for X being set holds {X} is Filter of BoolePoset X by WAYBEL16:12;
theorem
for X being non empty set holds {X} is Filter of X by CARD_FIL:4;
theorem Th30Thm70:
for A be Element of BoolePoset X holds
{Y where Y is Subset of X : A c= Y} is Filter of BoolePoset X
proof
let A be Element of BoolePoset X;
{Y where Y is Subset of X: A c= Y} = uparrow A by WAYBEL15:2;
hence thesis;
end;
theorem
for A be Element of BoolePoset X holds
{B where B is Element of BoolePoset X:A c= B} is Filter of BoolePoset X
proof
let A be Element of BoolePoset X;
reconsider A as Subset of X by WAYBEL_8:26;
{B where B is Element of BoolePoset X:A c=B}=
{B where B is Subset of X: A c= B} by Th29;
hence thesis by Th30Thm70;
end;
theorem
for X be non empty set, B be non empty Subset of BoolePoset X holds
(for x,y be Element of B ex z be Element of B st z c= x/\y)
iff B is filtered
proof
let X be non empty set,
B be non empty Subset of BoolePoset X;
hereby
assume
A1: (for x,y be Element of B ex z be Element of B st z c= x/\y);
for x,y being Element of BoolePoset X st x in B & y in B
ex z being Element of BoolePoset X st z in B & z<=x & z<=y
proof
let x,y be Element of BoolePoset X such that
A2: x in B & y in B;
reconsider x,y as Element of B by A2;
consider z0 be Element of B such that
A3: z0 c= x/\y by A1;
reconsider z0 as Element of BoolePoset X;
take z0;
x/\y c= x & x/\y c=y by XBOOLE_1:17;
then z0 c= x & z0 c= y by A3;
hence thesis by YELLOW_1:2;
end;
hence B is filtered;
end;
assume
A4: B is filtered;
for x,y be Element of B ex z be Element of B st z c= x/\y
proof
let x,y be Element of B;
consider z0 be Element of BoolePoset X such that
A5: z0 in B and
A6: z0 <= x and
A7: z0 <= y by A4;
A8: z0 c= x & z0 c= y by A6,A7,YELLOW_1:2;
reconsider z0 as Element of B by A5;
take z0;
thus thesis by A8,XBOOLE_1:19;
end;
hence thesis;
end;
theorem Th31:
for X be non empty set, F being non empty Subset of BooleLatt X holds
F is Filter of BooleLatt X iff
(for p,q being Element of F holds p/\q in F) &
(for p being Element of F, q be Element of BooleLatt X st
p c= q holds q in F)
proof
let X be non empty set,F be non empty Subset of BooleLatt X;
hereby
assume
A1: F is Filter of BooleLatt X; then
A2: for p,q being Element of BooleLatt X st p in F & p [= q holds
q in F by FILTER_0:9;
now
let p,q be Element of BooleLatt X;
now
assume p in F & q in F;
then p"/\"q in F by A1,FILTER_0:9;
hence p/\q in F;
end;
hence (p in F & q in F implies p/\q in F) &
(p in F & p c= q implies q in F) by A2,LATTICE3:2;
end;
hence (for p,q being Element of F holds p/\q in F) &
(for p be Element of F,q be Element of BooleLatt X st
p c= q holds q in F);
end;
assume that
A3: for p,q being Element of F holds p/\q in F and
A4: for p be Element of F, q be Element of BooleLatt X st p c= q holds q in F;
A5: (for p,q being Element of BooleLatt X st p in F & q in F holds
p"/\"q in F) by A3;
for p,q being Element of BooleLatt X st p in F & p [= q holds
q in F by A4,LATTICE3:2;
hence F is Filter of BooleLatt X by A5,FILTER_0:9;
end;
theorem Th32:
for X be non empty set,F be non empty Subset of BooleLatt X holds
F is Filter of BooleLatt X iff
for Y1,Y2 be Subset of X holds
(Y1 in F & Y2 in F implies Y1/\Y2 in F) &
(Y1 in F & Y1 c= Y2 implies Y2 in F)
proof
let X be non empty set,F be non empty Subset of BooleLatt X;
hereby
assume
A1: F is Filter of BooleLatt X;
hereby
let Y1,Y2 be Subset of X;
Y1 is Element of the carrier of BooleLatt X & Y2 is
Element of the carrier of BooleLatt X by LATTICE3:def 1;
hence (Y1 in F & Y2 in F implies Y1/\Y2 in F) &
(Y1 in F & Y1 c= Y2 implies Y2 in F) by A1,Th31;
end;
end;
assume that
A2: for Y1,Y2 be Subset of X holds
(Y1 in F & Y2 in F implies Y1/\Y2 in F) &
(Y1 in F & Y1 c= Y2 implies Y2 in F);
now
hereby
let p,q be Element of F;
reconsider p1=p,q1= q as Subset of X by LATTICE3:def 1;
p1 in F & q1 in F implies p1/\q1 in F by A2;
hence p/\q in F;
end;
let p be Element of F,q being Element of BooleLatt X such that
A3: p c= q;
reconsider p1=p,q1=q as Subset of X by LATTICE3:def 1;
p1 in F & p1 c= q &
(p1 in F & p1 c= q1 implies q1 in F) by A2,A3;
hence q in F;
end;
hence F is Filter of BooleLatt X by Th31;
end;
theorem Th33:
for X be non empty set, FF be non empty Subset-Family of X st
FF is Filter of BooleLatt X holds
FF is Filter of BoolePoset X
proof
let X be non empty set,FF be non empty Subset-Family of X such that
A1: FF is Filter of BooleLatt X;
now
set Z=LattPOSet BooleLatt X;
reconsider FF as Subset of Z by A1;
A2: FF is filtered
proof
for x,y being Element of Z st x in FF & y in FF holds
ex z being Element of Z st z in FF & z <= x & z <= y
proof
let x,y be Element of Z such that
A3: x in FF & y in FF;
reconsider x1=x,y1=y as Element of BooleLatt X;
set z = x1"/\" y1;
A4: now
x1 /\ y1 c= x1 & x1 /\ y1 c= y1 by XBOOLE_1:17;
hence z% <= x1% & z% <= y1% by LATTICE3:2,LATTICE3:7;
end;
x/\y in FF by A1,A3,Th31;
hence thesis by A4;
end;
hence thesis;
end;
FF is upper
proof
for x,y be Element of Z st x in FF & x <= y holds y in FF
proof
let x,y be Element of Z such that
A5: x in FF & x <= y;
reconsider x,y as Element of BooleLatt X;
A6: x% <= y% by A5;
x in FF & x c= y by A5,A6,LATTICE3:2,LATTICE3:7;
hence thesis by A1,Th31;
end;
hence thesis;
end;
hence thesis by A2;
end;
hence thesis;
end;
theorem Th34:
for X be non empty set,F be Filter of BoolePoset X holds
F is Filter of BooleLatt X
proof
let X be non empty set,F be Filter of BoolePoset X;
now
let Y1,Y2 be Subset of X;
hereby
assume that
A1: Y1 in F and
A2: Y2 in F;
reconsider Z1=Y1,Z2=Y2 as Element of BoolePoset X by LATTICE3:def 1;
A3: Z1 "/\" Z2 in F by A1,A2,WAYBEL_0:41;
set W = Z1 "/\" Z2;
reconsider Z1,Z2 as Element of BooleLatt X;
thus Y1 /\ Y2 in F by A3,YELLOW_1:17;
end;
hereby
assume that
A4: Y1 in F and
A5: Y1 c= Y2;
reconsider Z1=Y1,Z2=Y2 as Element of BoolePoset X by LATTICE3:def 1;
Z1 <= Z2 by YELLOW_1:2,A5;
hence Y2 in F by A4,WAYBEL_0:def 20;
end;
end;
hence thesis by Th32;
end;
theorem Th35:
for X be non empty set,F be non empty Subset of BooleLatt X holds
F is with_non-empty_elements & F is Filter of BooleLatt X iff
F is Filter of X
proof
let X be non empty set,
F be non empty Subset of BooleLatt X;
hereby
assume that
A1: F is with_non-empty_elements and
A2: F is Filter of BooleLatt X;
A3: F is non empty Subset-Family of X by LATTICE3:def 1;
for Y1,Y2 be Subset of X holds
(Y1 in F & Y2 in F implies Y1/\Y2 in F) &
(Y1 in F & Y1 c= Y2 implies Y2 in F) by A2,Th32;
hence F is Filter of X by A1,A3,CARD_FIL:def 1;
end;
assume F is Filter of X;
then F is with_non-empty_elements &
for Y1,Y2 be Subset of X holds
(Y1 in F & Y2 in F implies Y1/\Y2 in F) &
(Y1 in F & Y1 c= Y2 implies Y2 in F) by CARD_FIL:def 1;
hence F is with_non-empty_elements &
F is Filter of BooleLatt X by Th32;
end;
theorem Th36:
for X be non empty set, F be proper Filter of BoolePoset X holds
F is Filter of X
proof
let X be non empty set,
F be proper Filter of BoolePoset X;
A1: F is with_non-empty_elements
proof
assume not F is with_non-empty_elements;
then Bottom BoolePoset X in F by YELLOW_1:18;
hence contradiction by WAYBEL_7:4;
end;
reconsider F as non empty Subset of BooleLatt X;
thus thesis by A1,Th34,Th35;
end;
theorem
for T being non empty TopSpace,
x being Point of T holds
NeighborhoodSystem x is Filter of the carrier of T by Th36;
definition
let T be non empty TopSpace, F be proper Filter of BoolePoset [#]T;
func BOOL2F F -> Filter of the carrier of T equals
F;
coherence by Th36;
end;
definition
let T be non empty TopSpace, F1 be Filter of the carrier of T,
F2 be proper Filter of BoolePoset [#]T;
pred F1 is_filter-finer_than F2 means
BOOL2F F2 c= F1;
end;
begin :: Limit of a Filter
definition
let T be non empty TopSpace,
F be Filter of the carrier of T;
func lim_filter F -> Subset of T equals
{x where x is Point of T:F is_filter-finer_than NeighborhoodSystem x};
correctness
proof
set Z={x where x is Point of T:
F is_filter-finer_than NeighborhoodSystem x};
now
let x be object;
assume x in Z;
then consider x0 be Point of T such that
A1: x=x0 and
F is_filter-finer_than NeighborhoodSystem x0;
thus x in the carrier of T by A1;
end;
then Z c= the carrier of T;
hence thesis;
end;
end;
definition
let T being non empty TopSpace,
B be filter_base of the carrier of T;
func Lim B ->Subset of T equals
lim_filter <.B.);
correctness;
end;
theorem Th37:
for T being non empty TopSpace,
F be Filter of the carrier of T
ex F1 be proper Filter of BoolePoset the carrier of T st
F=F1
proof
let T be non empty TopSpace,
F be Filter of the carrier of T;
reconsider F1=F as non empty Subset of BooleLatt the carrier of T
by LATTICE3:def 1;
A1: F1 is Filter of BoolePoset the carrier of T by Th33,Th35;
not {} in F by CARD_FIL:def 1;
then not Bottom BoolePoset the carrier of T in F1 by YELLOW_1:18;
then F1 is proper;
hence thesis by A1;
end;
definition
let T be non empty TopSpace,F be Filter of the carrier of T;
func F2BOOL(F,T) -> proper Filter of BoolePoset [#]T equals
F;
coherence
proof
consider F2 be proper Filter of BoolePoset the carrier of T such that
A1: F=F2 by Th37;
thus thesis by A1;
end;
end;
theorem
for T being non empty TopSpace,x being Point of T,
F be Filter of the carrier of T holds x is_a_convergence_point_of F,T iff
x is_a_convergence_point_of F2BOOL(F,T),T;
theorem
for T being non empty TopSpace,x being Point of T,
F be Filter of the carrier of T holds x is_a_convergence_point_of F,T iff
x in lim_filter F
proof
let T be non empty TopSpace,x be Point of T,
F be Filter of the carrier of T;
consider F2 be proper Filter of BoolePoset the carrier of T such that
A1: F=F2 by Th37;
F is_filter-finer_than NeighborhoodSystem x iff
x in {x where x is Point of T: F is_filter-finer_than NeighborhoodSystem x}
proof
thus F is_filter-finer_than NeighborhoodSystem x implies
x in {x where x is Point of T: F is_filter-finer_than
NeighborhoodSystem x};
assume x in {x where x is Point of T: F is_filter-finer_than
NeighborhoodSystem x};
then consider x0 be Point of T such that
A2: x=x0 and
A3: F is_filter-finer_than NeighborhoodSystem x0;
thus F is_filter-finer_than NeighborhoodSystem x by A2,A3;
end;
hence thesis by A1,YELLOW19:3;
end;
definition
let T be non empty TopSpace,
F be Filter of BoolePoset [#]T;
func lim_filterb F -> Subset of T equals
{x where x is Point of T: NeighborhoodSystem x c= F};
correctness
proof
set Z={x where x is Point of T:NeighborhoodSystem x c= F};
now
let x be object;
assume x in Z;
then consider x0 be Point of T such that
A1: x=x0 and
NeighborhoodSystem x0 c= F;
thus x in the carrier of T by A1;
end;
then Z c= the carrier of T;
hence thesis;
end;
end;
theorem
for T being non empty TopSpace,
F be Filter of the carrier of T holds
lim_filter F = lim_filterb F2BOOL(F,T)
proof
let T be non empty TopSpace, F be Filter of the carrier of T;
now
hereby
let x be object;assume x in lim_filter F;
then consider x0 be Point of T such that
A1: x=x0 and
A2: F is_filter-finer_than NeighborhoodSystem x0;
thus x in lim_filterb F2BOOL(F,T) by A1,A2;
end;
let x be object;assume x in lim_filterb F2BOOL(F,T);
then consider x0 be Point of T such that
A3: x=x0 and
A4: NeighborhoodSystem x0 c= F;
F is_filter-finer_than NeighborhoodSystem x0 by A4;
hence x in lim_filter F by A3;
end;
then lim_filter F c= lim_filterb F2BOOL(F,T) &
lim_filterb F2BOOL(F,T) c= lim_filter F;
hence thesis;
end;
theorem
for T being non empty TopSpace, F being Filter of the carrier of T holds
Lim a_net F2BOOL(F,T)=lim_filter F
proof
let T be non empty TopSpace,F be Filter of the carrier of T;
now
hereby let x be object; assume
A1: x in Lim a_net F2BOOL(F,T);
then reconsider x0=x as Point of T;
F is_filter-finer_than NeighborhoodSystem x0
by A1,YELLOW19:3,YELLOW19:17;
hence x in lim_filter F;
end;
let x be object; assume
A2: x in lim_filter F;
then reconsider x0=x as Point of T;
consider x1 be Point of T such that
A3: x0=x1 and
A4: F is_filter-finer_than NeighborhoodSystem x1 by A2;
thus x in Lim a_net F2BOOL(F,T) by A3,A4,YELLOW19:3,YELLOW19:17;
end;
then Lim a_net F2BOOL(F,T) c= lim_filter F &
lim_filter F c= Lim a_net F2BOOL(F,T);
hence thesis;
end;
theorem Th38:
for T being Hausdorff non empty TopSpace,
F being Filter of the carrier of T,p,q being Point of T st
p in lim_filter F & q in lim_filter F holds p=q
proof
let T be Hausdorff non empty TopSpace,
F be Filter of the carrier of T,
p,q being Point of T such that
A1: p in lim_filter F and
A2: q in lim_filter F;
consider p0 be Point of T such that
A3: p=p0 and
A4: F is_filter-finer_than NeighborhoodSystem p0 by A1;
consider q0 be Point of T such that
A5: q=q0 and
A6: F is_filter-finer_than NeighborhoodSystem q0 by A2;
now
assume p<>q;
then consider G1,G2 being Subset of T such that
A7: G1 is open and
A8: G2 is open and
A9: p in G1 and
A10: q in G2 and
A11: G1 misses G2 by PRE_TOPC:def 10;
G1 in NeighborhoodSystem p &
G2 in NeighborhoodSystem q by A7,A8,A9,A10,CONNSP_2:3,YELLOW19:2;
then {} in F by A3,A4,A5,A6,A11,CARD_FIL:def 1;
hence contradiction by CARD_FIL:def 1;
end;
hence thesis;
end;
registration
let T be Hausdorff non empty TopSpace,
F be Filter of the carrier of T;
cluster lim_filter F -> trivial;
coherence
proof
for p,q being Point of T st p in lim_filter F &
q in lim_filter F holds p=q by Th38;
hence thesis by SUBSET_1:45;
end;
end;
definition
let X be non empty set,T be non empty TopSpace,
f be Function of X,the carrier of T,
F be Filter of X;
func lim_filter(f,F) -> Subset of [#]T equals
lim_filter filter_image(f,F);
coherence;
end;
definition
let T be non empty TopSpace,
L be non empty transitive reflexive RelStr,
f be Function of [#]L,the carrier of T;
func lim_f f -> Subset of [#]T equals
lim_filter filter_image(f,Tails_Filter L);
coherence;
end;
theorem
for T being non empty TopSpace,
L being non empty transitive reflexive RelStr,
f being Function of [#]L,the carrier of T, x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x st
[#]L is directed holds
x in lim_f f iff
for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b
proof
let T be non empty TopSpace, L be non empty transitive reflexive RelStr,
f be Function of [#]L,the carrier of T, x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x such that
A1: [#]L is directed;
hereby
assume x in lim_f f;
then consider x0 be Element of T such that
A2: x=x0 and
A3: filter_image(f,Tails_Filter L) is_filter-finer_than
NeighborhoodSystem x0;
BOOL2F NeighborhoodSystem x is_filter-coarser_than
filter_image(f,Tails_Filter L) by A2,A3;
then
A4: B is_coarser_than f.:#(Tails L) by A1,Th19;
reconsider B1=B as filter_base of [#]T by Th09;
for b be Element of B1 ex i be Element of L st
for j be Element of L st i <=j holds f.j in b by A1,A4,Th20;
hence for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b;
end;
assume
A5: for b be Element of B ex i be Element of L st
for j be Element of L st i <=j holds f.j in b;
reconsider B1=B as filter_base of [#]T by Th09;
for b be Element of B1 ex i be Element of L st
for j be Element of L st i <=j holds f.j in b by A5;
then B is_coarser_than f.:#(Tails L) by A1,Th20;
then BOOL2F NeighborhoodSystem x is_filter-coarser_than
filter_image(f,Tails_Filter L) by A1,Th19;
then x is Element of T & filter_image(f,Tails_Filter L)
is_filter-finer_than NeighborhoodSystem x;
hence x in lim_f f;
end;
definition
let T be non empty TopSpace, s be sequence of T;
func lim_f s -> Subset of T equals
lim_filter elementary_filter(s);
coherence;
end;
theorem
for T be non empty TopSpace, s be sequence of T holds
lim_filter(s,Frechet_Filter(NAT))=lim_f s;
theorem
for T being non empty TopSpace,x being Point of T holds
NeighborhoodSystem x is filter_base of [#]T
proof
let T be non empty TopSpace, x be Point of T;
reconsider Nx=NeighborhoodSystem x as Filter of [#]T by Th36;
Nx is basis of Nx by Th03;
hence thesis by Th09;
end;
theorem
for T being non empty TopSpace,x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
B is filter_base of [#]T by Th09;
theorem
for X be non empty set, s be sequence of X,
B be filter_base of X holds
B is_coarser_than s.:base_of_frechet_filter iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b by Th20;
theorem Th39:
for T being non empty TopSpace,s being sequence of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter(NAT)) iff
B is_coarser_than s.:base_of_frechet_filter
proof
let T be non empty TopSpace, s be sequence of T,
x be Point of T, B be basis of BOOL2F NeighborhoodSystem x;
set F=filter_image(s,Frechet_Filter(NAT));
hereby
assume x in lim_filter(s,Frechet_Filter(NAT));
then consider x0 be Element of T such that
A1: x=x0 and
A2: F is_filter-finer_than NeighborhoodSystem x0;
BOOL2F NeighborhoodSystem x is_filter-coarser_than F by A1,A2;
hence B is_coarser_than s.:base_of_frechet_filter
by Th19,Th27;
end;
assume
A3: B is_coarser_than s.:base_of_frechet_filter;
BOOL2F NeighborhoodSystem x is_filter-coarser_than F
by A3,Th19,Th27;
then F is_filter-finer_than NeighborhoodSystem x;
hence x in lim_filter(s,Frechet_Filter(NAT));
end;
theorem Th40:
for T being non empty TopSpace,s being sequence of [#]T, x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
B is_coarser_than s.:base_of_frechet_filter iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b
proof
let T be non empty TopSpace,s be sequence of [#]T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
reconsider B as filter_base of [#]T by Th09;
B is_coarser_than s.:base_of_frechet_filter iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b by Th20;
hence thesis;
end;
theorem Th41:
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_filter(s,Frechet_Filter(NAT)) iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
x in lim_filter(s,Frechet_Filter(NAT)) iff
B is_coarser_than s.:base_of_frechet_filter by Th39;
hence thesis by Th40;
end;
theorem Th42:
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_f s iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
x in lim_filter(s,Frechet_Filter(NAT)) iff
for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b by Th41;
hence thesis;
end;
begin :: Nets
definition
let L be 1-sorted,
s be sequence of the carrier of L;
func sequence_to_net(s) -> non empty strict NetStr over L equals
NetStr(# NAT, NATOrd, s #);
coherence;
end;
registration
let L be non empty 1-sorted,
s be sequence of the carrier of L;
cluster sequence_to_net(s) -> non empty;
coherence;
end;
theorem Th43:
for L being non empty 1-sorted, B being set,
s being sequence of the carrier of L holds
sequence_to_net(s) is_eventually_in B iff
ex i being Element of sequence_to_net(s) st for j being Element of
sequence_to_net(s) st i <= j holds (sequence_to_net(s)).j in B;
theorem Th44:
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
(for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b)
iff
(for b be Element of B
ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b)
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
A1: (for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b)
implies
(for b be Element of B
ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b)
proof
assume
A2: for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b;
for b be Element of B
ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b
proof
let b be Element of B;
consider i be Element of OrderedNAT such that
A3: for j be Element of OrderedNAT st i <=j holds s.j in b by A2;
reconsider i0=i as Element of sequence_to_net(s);
for j be Element of sequence_to_net(s) st
i0 <= j holds (sequence_to_net(s)).j in b
proof
let j be Element of sequence_to_net(s);
assume
A4: i0<=j;
reconsider j0=j as Element of OrderedNAT;
(the mapping of sequence_to_net(s)).j=s.j0 & i<=j0 by A4;
hence thesis by A3;
end;
hence thesis;
end;
hence thesis;
end;
(for b be Element of B
ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b)
implies
(for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b)
proof
assume
A5: for b be Element of B ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b;
(for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b)
proof
let b be Element of B;
consider i be Element of sequence_to_net(s) such that
A6: for j be Element of sequence_to_net(s) st i <=j holds
(sequence_to_net(s)).j in b by A5;
reconsider i0=i as Element of OrderedNAT;
for j be Element of OrderedNAT st i0 <=j holds s.j in b
proof
let j be Element of OrderedNAT;
assume
A7: i0 <=j;
reconsider j0=j as Element of sequence_to_net(s);
(the mapping of sequence_to_net(s)).j0=s.j & i<=j0 by A7;
then (sequence_to_net(s)).j0 in b & i <= j0 by A6;
hence thesis;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by A1;
end;
theorem
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_f s iff for b be Element of B holds
sequence_to_net(s) is_eventually_in b
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
hereby
assume x in lim_f s;
then for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b by Th42;
hence for b be Element of B holds sequence_to_net(s) is_eventually_in b
by Th44;
end;
assume for b be Element of B holds sequence_to_net(s) is_eventually_in b;
then (for b be Element of B
ex i be Element of sequence_to_net(s) st
for j be Element of sequence_to_net(s) st
i <=j holds (sequence_to_net(s)).j in b) by Th43;
then for b be Element of B ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b by Th44;
hence x in lim_f s by Th42;
end;
theorem Th45:
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T,
B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_f s iff
for b be Element of B ex i be Element of NAT st
for j be Element of NAT st i <=j holds s.j in b
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
now
hereby
assume
A1: x in lim_filter(s,Frechet_Filter(NAT));
now
let b be Element of B;
consider i0 be Element of OrderedNAT such that
A2: for j be Element of OrderedNAT st i0 <= j holds s.j in b
by A1,Th41;
reconsider i1=i0 as Element of NAT;
now
let j be Element of NAT;
assume
A3: i1<=j;
reconsider j1=j as Element of OrderedNAT;
i0<=j1 by A3;
hence s.j in b by A2;
end;
hence ex i be Element of NAT st
for j be Element of NAT st i <=j holds s.j in b;
end;
hence for b be Element of B ex i be Element of NAT st
for j be Element of NAT st i <=j holds s.j in b;
end;
assume
A4: for b be Element of B ex i be Element of NAT st
for j be Element of NAT st i <=j holds s.j in b;
now
let b be Element of B;
consider i0 be Element of NAT such that
A5: for j be Element of NAT st i0<=j holds s.j in b by A4;
reconsider i1=i0 as Element of OrderedNAT;
now
let j be Element of OrderedNAT;
assume
A6: i1 <= j;
consider x,y be Element of NAT such that
A7: [i1,j]=[x,y] and
A8: x<=y by A6;
i1=x & j=y & x<=y by A7,A8,XTUPLE_0:1;
hence s.j in b by A5;
end;
hence ex i be Element of OrderedNAT st
for j be Element of OrderedNAT st i <=j holds s.j in b;
end;
hence x in lim_filter(s,Frechet_Filter(NAT)) by Th41;
end;
hence thesis;
end;
theorem
for T being non empty TopSpace,s being sequence of the carrier of T,
x being Point of T, B being basis of BOOL2F NeighborhoodSystem x holds
x in lim_f s iff
for b be Element of B ex i be Nat st
for j be Nat st i <= j holds s.j in b
proof
let T be non empty TopSpace,s be sequence of the carrier of T,
x be Point of T,
B be basis of BOOL2F NeighborhoodSystem x;
hereby
assume
A1: x in lim_f s;
now
let b be Element of B;
consider i0 be Element of NAT such that
A2: for j be Element of NAT st i0 <=j holds s.j in b by A1,Th45;
reconsider i1=i0 as Nat;
take i1;
now
let k be Nat;
assume
A3: i1<=k;
reconsider k0=k as Element of NAT by ORDINAL1:def 12;
i0 <= k0 by A3;
hence s.k in b by A2;
end;
hence for k be Nat st i1 <= k holds s.k in b;
end;
hence for b be Element of B ex i be Nat st
for j be Nat st i <=j holds s.j in b;
end;
assume
A4: for b be Element of B ex i be Nat st
for j be Nat st i <= j holds s.j in b;
now
let b be Element of B;
consider i0 be Nat such that
A5: for j be Nat st i0<=j holds s.j in b by A4;
reconsider i1=i0 as Element of NAT by ORDINAL1:def 12;
take i1;
thus for j be Element of NAT st i1 <= j holds s.j in b by A5;
end;
hence x in lim_f s by Th45;
end;