:: Convergent Filter Bases
:: by Roland Coghetto
::
:: Received June 30, 2015
:: Copyright (c) 2015-2016 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;
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
:: CARDFIL2:def 1
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;
end;
registration
let X be set;
cluster upper for non empty cap-closed Subset-Family of X;
end;
registration
let X be non empty set;
cluster with_non-empty_elements for non empty upper cap-closed
Subset-Family of X;
end;
theorem :: CARDFIL2:1
SFX is non empty with_non-empty_elements upper cap-closed
Subset-Family of X iff SFX is Filter of X;
theorem :: CARDFIL2:2
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:];
definition
let X be non empty set;
attr X is cap-finite-closed means
:: CARDFIL2:def 2
for SX be finite non empty Subset of X holds meet SX in X;
end;
registration
cluster cap-finite-closed for non empty set;
end;
theorem :: CARDFIL2:3
for X being non empty set st X is cap-finite-closed holds
X is cap-closed;
registration
cluster cap-finite-closed -> cap-closed for non empty set;
end;
theorem :: CARDFIL2:4
for X be set,SFX be Subset-Family of X holds SFX is cap-closed & X in SFX iff
FinMeetCl SFX c= SFX;
theorem :: CARDFIL2:5
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;
registration
let X be non empty set;
cluster -> cap-closed for Filter of X;
end;
theorem :: CARDFIL2:6
for X be set, B be Subset-Family of X st B={X} holds
B is upper;
theorem :: CARDFIL2:7
for X be non empty set, F be Filter of X holds F <> bool X;
definition
let X be non empty set;
func Filt X -> non empty set equals
:: CARDFIL2:def 3
the set of all F where F is Filter of X;
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
:: CARDFIL2:def 4
meet rng M;
end;
definition
let X be non empty set, F1,F2 be Filter of X;
pred F1 is_filter-coarser_than F2 means
:: CARDFIL2:def 5
F1 c= F2;
reflexivity;
pred F1 is_filter-finer_than F2 means
:: CARDFIL2:def 6
F2 c= F1;
reflexivity;
end;
theorem :: CARDFIL2:8
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;
theorem :: CARDFIL2:9
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;
theorem :: CARDFIL2:10
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;
theorem :: CARDFIL2:11
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;
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
:: CARDFIL2:def 7
for f be Element of F holds ex b be Element of B st b c=f;
end;
theorem :: CARDFIL2:12
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;
registration
let X be non empty set;
let F be Filter of X;
cluster filter_basis for non empty Subset of F;
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 :: CARDFIL2:13
for X be non empty set,F be Filter of X holds F is basis of F;
definition
let X be set, B be Subset-Family of X;
func <.B.] -> Subset-Family of X means
:: CARDFIL2:def 8
for x being Subset of X holds x in it iff ex b be Element of B st b c=x;
end;
theorem :: CARDFIL2:14
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};
theorem :: CARDFIL2:15
for X be set,B be empty Subset-Family of X holds <.B.]=bool X;
theorem :: CARDFIL2:16
for X be set,B be Subset-Family of X st {} in B holds <.B.]=bool X;
begin :: Filters -- Lattice-theoretical Approach
theorem :: CARDFIL2:17
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;
theorem :: CARDFIL2:18
for X be set, B be Subset-Family of X holds B c= <.B.];
definition
let X be set;
let B1,B2 be Subset-Family of X;
pred B1,B2 are_equivalent_generators means
:: CARDFIL2:def 9
(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 :: CARDFIL2:19
for X be set,B1,B2 be Subset-Family of X st B1,B2 are_equivalent_generators
holds <.B1.] c= <.B2.];
theorem :: CARDFIL2:20
for X be set,B1,B2 be Subset-Family of X st
B1,B2 are_equivalent_generators holds <.B1.]=<.B2.];
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
:: CARDFIL2:def 10
B;
end;
theorem :: CARDFIL2:21
for X be non empty set,F be Filter of X,B be basis of F holds F=<.#B.];
theorem :: CARDFIL2:22
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;
theorem :: CARDFIL2:23
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;
theorem :: CARDFIL2:24
for X be non empty set,F be Filter of X,B1,B2 be basis of F holds
#B1, #B2 are_equivalent_generators;
definition
let X be set;
let B be Subset-Family of X;
attr B is quasi_basis means
:: CARDFIL2:def 11
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;
end;
registration
let X be non empty set;
cluster with_non-empty_elements for non empty quasi_basis Subset-Family of X;
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 :: CARDFIL2:25
for X be non empty set,B be filter_base of X holds <.B.] is Filter of X;
definition
let X be non empty set,B be filter_base of X;
func <.B.) -> Filter of X equals
:: CARDFIL2:def 12
<.B.];
end;
theorem :: CARDFIL2:26
for X be non empty set,B1,B2 be filter_base of X st <.B1.)=<.B2.) holds
B1,B2 are_equivalent_generators;
theorem :: CARDFIL2:27
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;
theorem :: CARDFIL2:28
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;
theorem :: CARDFIL2:29
for X be non empty set, F be Filter of X, B be basis of F holds
B is filter_base of X;
theorem :: CARDFIL2:30
for X be non empty set, B be filter_base of X holds B is basis of <.B.);
theorem :: CARDFIL2:31
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;
theorem :: CARDFIL2:32
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;
theorem :: CARDFIL2:33
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;
theorem :: CARDFIL2:34
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};
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
:: CARDFIL2:def 13
{M where M is Subset of Y : f"(M) in F};
end;
theorem :: CARDFIL2:35
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);
theorem :: CARDFIL2:36
for X be non empty set, B be filter_base of X st B=<.B.) holds
B is Filter of X;
theorem :: CARDFIL2:37
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);
theorem :: CARDFIL2:38
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.);
theorem :: CARDFIL2:39
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;
theorem :: CARDFIL2:40
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};
definition
let L be non empty RelStr;
func Tails L -> non empty Subset-Family of L equals
:: CARDFIL2:def 14
the set of all uparrow i where i is Element of L;
end;
theorem :: CARDFIL2:41
for L be non empty transitive reflexive RelStr st [#]L is directed
holds <.Tails L.] is Filter of [#]L;
definition
let L be non empty transitive reflexive RelStr;
assume
[#]L is directed;
func Tails_Filter(L) -> Filter of [#]L equals
:: CARDFIL2:def 15
<.Tails L.];
end;
theorem :: CARDFIL2:42
for L be non empty transitive reflexive RelStr
st [#]L is directed holds
Tails L is basis of Tails_Filter(L);
definition
let L be RelStr;
let x be Subset-Family of L;
func #x -> Subset-Family of [#]L equals
:: CARDFIL2:def 16
x;
end;
theorem :: CARDFIL2:43
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));
theorem :: CARDFIL2:44
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;
theorem :: CARDFIL2:45
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;
theorem :: CARDFIL2:46
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);
theorem :: CARDFIL2:47
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;
definition
let X be non empty set,
s be sequence of X;
func elementary_filter(s) -> Filter of X equals
:: CARDFIL2:def 17
filter_image(s,Frechet_Filter(NAT));
end;
theorem :: CARDFIL2:48
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};
theorem :: CARDFIL2:49
for n be natural number holds
NAT\{t where t is Element of NAT:n <= t} is finite;
theorem :: CARDFIL2:50
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;
registration
cluster [#]OrderedNAT -> directed;
cluster OrderedNAT -> reflexive;
end;
theorem :: CARDFIL2:51
for X be denumerable set holds
Frechet_Filter (X) = the set of all X\A where A is finite Subset of X;
theorem :: CARDFIL2:52
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);
theorem :: CARDFIL2:53
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;
theorem :: CARDFIL2:54
#(Tails OrderedNAT) is basis of Frechet_Filter(NAT) &
Tails_Filter(OrderedNAT)=Frechet_Filter(NAT);
definition
func base_of_frechet_filter -> filter_base of NAT equals
:: CARDFIL2:def 18
#(Tails OrderedNAT);
end;
theorem :: CARDFIL2:55
NAT in base_of_frechet_filter;
theorem :: CARDFIL2:56
base_of_frechet_filter is basis of Frechet_Filter(NAT);
theorem :: CARDFIL2:57
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;
theorem :: CARDFIL2:58
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;
definition
let X be set;
let x be Subset of X;
func PLO2bis(x) -> Element of BoolePoset X equals
:: CARDFIL2:def 19
x;
end;
theorem :: CARDFIL2:59
for X being infinite set holds
X in the set of all X\A where A is finite Subset of X;
theorem :: CARDFIL2:60
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};
theorem :: CARDFIL2:61
for X be set,a be Element of BoolePoset X holds
uparrow a = {Y where Y is Subset of X : a c=Y};
theorem :: CARDFIL2:62
for X be set, A be Subset of X holds
{B where B is Element of BoolePoset X: A c= B} =
uparrow PLO2bis A;
theorem :: CARDFIL2:63
for X be non empty set, F be Filter of X holds
union F = X;
theorem :: CARDFIL2:64
for X be infinite set holds
the set of all X\A where A is finite Subset of X is Filter of X;
theorem :: CARDFIL2:65
for X being set holds bool X is Filter of BoolePoset X;
theorem :: CARDFIL2:66
for X being set holds {X} is Filter of BoolePoset X;
theorem :: CARDFIL2:67
for X being non empty set holds {X} is Filter of X;
theorem :: CARDFIL2:68
for A be Element of BoolePoset X holds
{Y where Y is Subset of X : A c= Y} is Filter of BoolePoset X;
theorem :: CARDFIL2:69
for A be Element of BoolePoset X holds
{B where B is Element of BoolePoset X:A c= B} is Filter of BoolePoset X;
theorem :: CARDFIL2:70
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;
theorem :: CARDFIL2:71
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);
theorem :: CARDFIL2:72
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);
theorem :: CARDFIL2:73
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;
theorem :: CARDFIL2:74
for X be non empty set,F be Filter of BoolePoset X holds
F is Filter of BooleLatt X;
theorem :: CARDFIL2:75
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;
theorem :: CARDFIL2:76
for X be non empty set, F be proper Filter of BoolePoset X holds
F is Filter of X;
theorem :: CARDFIL2:77
for T being non empty TopSpace,
x being Point of T holds
NeighborhoodSystem x is Filter of the carrier of T;
definition
let T be non empty TopSpace, F be proper Filter of BoolePoset [#]T;
func BOOL2F F -> Filter of the carrier of T equals
:: CARDFIL2:def 20
F;
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
:: CARDFIL2:def 21
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
:: CARDFIL2:def 22
{x where x is Point of T:F is_filter-finer_than NeighborhoodSystem x};
end;
definition
let T being non empty TopSpace,
B be filter_base of the carrier of T;
func Lim B ->Subset of T equals
:: CARDFIL2:def 23
lim_filter <.B.);
end;
theorem :: CARDFIL2:78
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;
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
:: CARDFIL2:def 24
F;
end;
theorem :: CARDFIL2:79
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 :: CARDFIL2:80
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;
definition
let T be non empty TopSpace,
F be Filter of BoolePoset [#]T;
func lim_filterb F -> Subset of T equals
:: CARDFIL2:def 25
{x where x is Point of T: NeighborhoodSystem x c= F};
end;
theorem :: CARDFIL2:81
for T being non empty TopSpace,
F be Filter of the carrier of T holds
lim_filter F = lim_filterb F2BOOL(F,T);
theorem :: CARDFIL2:82
for T being non empty TopSpace, F being Filter of the carrier of T holds
Lim a_net F2BOOL(F,T)=lim_filter F;
theorem :: CARDFIL2:83
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;
registration
let T be Hausdorff non empty TopSpace,
F be Filter of the carrier of T;
cluster lim_filter F -> trivial;
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
:: CARDFIL2:def 26
lim_filter filter_image(f,F);
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
:: CARDFIL2:def 27
lim_filter filter_image(f,Tails_Filter L);
end;
theorem :: CARDFIL2:84
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;
definition
let T be non empty TopSpace, s be sequence of T;
func lim_f s -> Subset of T equals
:: CARDFIL2:def 28
lim_filter elementary_filter(s);
end;
theorem :: CARDFIL2:85
for T be non empty TopSpace, s be sequence of T holds
lim_filter(s,Frechet_Filter(NAT))=lim_f s;
theorem :: CARDFIL2:86
for T being non empty TopSpace,x being Point of T holds
NeighborhoodSystem x is filter_base of [#]T;
theorem :: CARDFIL2:87
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;
theorem :: CARDFIL2:88
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;
theorem :: CARDFIL2:89
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;
theorem :: CARDFIL2:90
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;
theorem :: CARDFIL2:91
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;
theorem :: CARDFIL2:92
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;
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
:: CARDFIL2:def 29
NetStr(# NAT, NATOrd, s #);
end;
registration
let L be non empty 1-sorted,
s be sequence of the carrier of L;
cluster sequence_to_net(s) -> non empty;
end;
theorem :: CARDFIL2:93
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 :: CARDFIL2:94
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);
theorem :: CARDFIL2:95
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;
theorem :: CARDFIL2:96
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;
theorem :: CARDFIL2:97
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;