:: Convergent Filter Bases
:: by Roland Coghetto
::
:: Received June 30, 2015
:: Copyright (c) 2015-2021 Association of Mizar Users


definition
let X be set ;
let SFX be Subset-Family of X;
attr SFX is upper means :def1: :: CARDFIL2:def 1
 for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX;
end;

:: deftheorem def1 defines upper CARDFIL2:def 1 :
for X being set
for SFX being Subset-Family of X holds
( SFX is upper iff for Y1, Y2 being Subset of X st Y1 in SFX & Y1 c= Y2 holds
Y2 in SFX );

registration
let X be set ;
cluster non empty cap-closed for Element of bool (bool X);
existence
not for b1 being cap-closed Subset-Family of X holds b1 is empty
proof end;
end;

registration
let X be set ;
cluster non empty cap-closed upper for Element of bool (bool X);
existence
ex b1 being non empty cap-closed Subset-Family of X st b1 is upper
proof end;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements cap-closed upper for Element of bool (bool X);
existence
ex b1 being non empty cap-closed upper Subset-Family of X st b1 is with_non-empty_elements
proof end;
end;

Lm01: for X being non empty set
for SFX being non empty with_non-empty_elements cap-closed upper Subset-Family of X holds SFX is Filter of X
proof end;

Lm02: for X being non empty set
for FX being Filter of X holds FX is non empty with_non-empty_elements cap-closed upper Subset-Family of X
proof end;

theorem :: CARDFIL2:1
for X being non empty set
for SFX being Subset-Family of X holds
( SFX is non empty with_non-empty_elements cap-closed upper Subset-Family of X iff SFX is Filter of X ) by Lm01, Lm02;

theorem :: CARDFIL2:2
for X1, X2 being non empty set
for F1 being Filter of X1
for F2 being Filter of X2 holds { [:f1,f2:] where f1 is Element of F1, f2 is Element of F2 : verum } is non empty Subset-Family of [:X1,X2:]
proof end;

definition
let X be non empty set ;
attr X is cap-finite-closed means :: CARDFIL2:def 2
 for SX being non empty finite Subset of X holds meet SX in X;
end;

:: deftheorem defines cap-finite-closed CARDFIL2:def 2 :
for X being non empty set holds
( X is cap-finite-closed iff for SX being non empty finite Subset of X holds meet SX in X );

registration
cluster non empty cap-finite-closed for set ;
existence
ex b1 being non empty set st b1 is cap-finite-closed
proof end;
end;

theorem Th01: :: CARDFIL2:3
for X being non empty set st X is cap-finite-closed holds
X is cap-closed
proof end;

registration
cluster non empty cap-finite-closed -> non empty cap-closed for set ;
coherence
for b1 being non empty set st b1 is cap-finite-closed holds
b1 is cap-closed by Th01;
end;

theorem Th02: :: CARDFIL2:4
for X being set
for SFX being Subset-Family of X holds
( ( SFX is cap-closed & X in SFX ) iff FinMeetCl SFX c= SFX )
proof end;

theorem :: CARDFIL2:5
for X being non empty set
for A being non empty Subset of X holds { B where B is Subset of X : A c= B } is Filter of X
proof end;

registration
let X be non empty set ;
cluster -> cap-closed for Filter of X;
coherence
for b1 being Filter of X holds b1 is cap-closed by CARD_FIL:def 1;
end;

theorem :: CARDFIL2:6
for X being set
for B being Subset-Family of X st B = {X} holds
B is upper
proof end;

theorem :: CARDFIL2:7
for X being non empty set
for F being Filter of X holds F <> bool X
proof end;

definition
let X be non empty set ;
func Filt X -> non empty set equals :: CARDFIL2:def 3
 { F where F is Filter of X : verum } ;
correctness
coherence
{ F where F is Filter of X : verum } is non empty set ;
proof end;
end;

:: deftheorem defines Filt CARDFIL2:def 3 :
for X being non empty set holds Filt X = { F where F is Filter of X : verum } ;

definition
let X, I be non empty set ;
let M be Filt X -valued ManySortedSet of I;
func Filter_Intersection M -> Filter of X equals :: CARDFIL2:def 4
 meet (rng M);
coherence
meet (rng M) is Filter of X
proof end;
end;

:: deftheorem defines Filter_Intersection CARDFIL2:def 4 :
for X, I being non empty set
for M being Filt b1 -valued ManySortedSet of I holds Filter_Intersection M = meet (rng M);

definition
let X be non empty set ;
let F1, F2 be Filter of X;
pred F1 is_filter-coarser_than F2 means :: CARDFIL2:def 5
F1 c= F2;
reflexivity
for F1 being Filter of X holds F1 c= F1 ;
pred F1 is_filter-finer_than F2 means :: CARDFIL2:def 6
F2 c= F1;
reflexivity
for F1 being Filter of X holds F1 c= F1 ;
end;

:: deftheorem defines is_filter-coarser_than CARDFIL2:def 5 :
for X being non empty set
for F1, F2 being Filter of X holds
( F1 is_filter-coarser_than F2 iff F1 c= F2 );

:: deftheorem defines is_filter-finer_than CARDFIL2:def 6 :
for X being non empty set
for F1, F2 being Filter of X holds
( F1 is_filter-finer_than F2 iff F2 c= F1 );

theorem :: CARDFIL2:8
for X being non empty set
for F, FX being Filter of X st FX = {X} holds
FX is_coarser_than F
proof end;

theorem :: CARDFIL2:9
for X, I being non empty set
for M being Filt b1 -valued ManySortedSet of I
for i being Element of I
for F being Filter of X st F = M . i holds
Filter_Intersection M is_filter-coarser_than F
proof end;

theorem :: CARDFIL2:10
for X being set
for S being Subset-Family of X st FinMeetCl S is with_non-empty_elements holds
S is with_non-empty_elements
proof end;

theorem :: CARDFIL2:11
for X being non empty set
for G being Subset-Family of X
for F being Filter of X st G c= F holds
( FinMeetCl G c= F & FinMeetCl G is with_non-empty_elements )
proof 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: :: CARDFIL2:def 7
 for f being Element of F ex b being Element of B st b c= f;
end;

:: deftheorem def2 defines filter_basis CARDFIL2:def 7 :
for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds
( B is filter_basis iff for f being Element of F ex b being Element of B st b c= f );

theorem :: CARDFIL2:12
for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds
( F is_coarser_than B iff B is filter_basis )
proof end;

registration
let X be non empty set ;
let F be Filter of X;
cluster non empty filter_basis for Element of bool F;
existence
ex b1 being non empty Subset of F st b1 is filter_basis
proof end;
end;

definition
let X be non empty set ;
let F be Filter of X;
mode basis of F is non empty filter_basis Subset of F;
end;

theorem Th03: :: CARDFIL2:13
for X being non empty set
for F being Filter of X holds F is basis of F
proof end;

definition
let X be set ;
let B be Subset-Family of X;
func <.B.] -> Subset-Family of X means :def3: :: CARDFIL2:def 8
 for x being Subset of X holds
( x in it iff ex b being Element of B st b c= x );
existence
ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex b being Element of B st b c= x )
proof end;
correctness
uniqueness
for b1, b2 being Subset-Family of X st ( for x being Subset of X holds
( x in b1 iff ex b being Element of B st b c= x ) ) & ( for x being Subset of X holds
( x in b2 iff ex b being Element of B st b c= x ) ) holds
b1 = b2;
proof end;
end;

:: deftheorem def3 defines <. CARDFIL2:def 8 :
for X being set
for B, b3 being Subset-Family of X holds
( b3 = <.B.] iff for x being Subset of X holds
( x in b3 iff ex b being Element of B st b c= x ) );

theorem :: CARDFIL2:14
for X being set
for S being Subset-Family of X holds <.S.] = { x where x is Subset of X : ex b being Element of S st b c= x }
proof end;

theorem :: CARDFIL2:15
for X being set
for B being empty Subset-Family of X holds <.B.] = bool X
proof end;

theorem :: CARDFIL2:16
for X being set
for B being Subset-Family of X st {} in B holds
<.B.] = bool X
proof end;

theorem Th04: :: CARDFIL2:17
for X being set
for B being non empty Subset-Family of X
for L being Subset of (BoolePoset X) st B = L holds
<.B.] = uparrow L
proof end;

theorem :: CARDFIL2:18
for X being set
for B being 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 :: CARDFIL2:def 9
( ( for b1 being Element of B1 ex b2 being Element of B2 st b2 c= b1 ) & ( for b2 being Element of B2 ex b1 being Element of B1 st b1 c= b2 ) );
reflexivity
for B1 being Subset-Family of X holds
( ( for b1 being Element of B1 ex b2 being Element of B1 st b2 c= b1 ) & ( for b2 being Element of B1 ex b1 being Element of B1 st b1 c= b2 ) ) ;
symmetry
for B1, B2 being Subset-Family of X st ( for b1 being Element of B1 ex b2 being Element of B2 st b2 c= b1 ) & ( for b2 being Element of B2 ex b1 being Element of B1 st b1 c= b2 ) holds
( ( for b1 being Element of B2 ex b2 being Element of B1 st b2 c= b1 ) & ( for b2 being Element of B1 ex b1 being Element of B2 st b1 c= b2 ) ) ;
end;

:: deftheorem defines are_equivalent_generators CARDFIL2:def 9 :
for X being set
for B1, B2 being Subset-Family of X holds
( B1,B2 are_equivalent_generators iff ( ( for b1 being Element of B1 ex b2 being Element of B2 st b2 c= b1 ) & ( for b2 being Element of B2 ex b1 being Element of B1 st b1 c= b2 ) ) );

theorem Th05: :: CARDFIL2:19
for X being set
for B1, B2 being Subset-Family of X st B1,B2 are_equivalent_generators holds
<.B1.] c= <.B2.]
proof end;

theorem :: CARDFIL2:20
for X being set
for B1, B2 being 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 :: CARDFIL2:def 10
B;
coherence
B is non empty Subset-Family of X by XBOOLE_1:1;
end;

:: deftheorem defines # CARDFIL2:def 10 :
for X being non empty set
for F being Filter of X
for B being non empty Subset of F holds # B = B;

theorem Th06: :: CARDFIL2:21
for X being non empty set
for F being Filter of X
for B being basis of F holds F = <.(# B).]
proof end;

theorem Th07: :: CARDFIL2:22
for X being non empty set
for F being Filter of X
for B being Subset-Family of X st F = <.B.] holds
B is basis of F
proof end;

theorem :: CARDFIL2:23
for X being non empty set
for F being Filter of X
for B being basis of F
for S being Subset-Family of X
for S1 being Subset of F st S = S1 & # B,S are_equivalent_generators holds
S1 is basis of F
proof end;

theorem :: CARDFIL2:24
for X being non empty set
for F being Filter of X
for B1, B2 being basis of F holds # B1, # B2 are_equivalent_generators
proof end;

definition
let X be set ;
let B be Subset-Family of X;
attr B is quasi_basis means :def4: :: CARDFIL2:def 11
 for b1, b2 being Element of B ex b being Element of B st b c= b1 /\ b2;
end;

:: deftheorem def4 defines quasi_basis CARDFIL2:def 11 :
for X being set
for B being Subset-Family of X holds
( B is quasi_basis iff for b1, b2 being Element of B ex b being Element of B st b c= b1 /\ b2 );

registration
let X be non empty set ;
cluster non empty quasi_basis for Element of bool (bool X);
existence
ex b1 being non empty Subset-Family of X st b1 is quasi_basis
proof end;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements quasi_basis for Element of bool (bool X);
existence
ex b1 being non empty quasi_basis Subset-Family of X st b1 is with_non-empty_elements
proof end;
end;

definition
let X be non empty set ;
mode filter_base of X is non empty with_non-empty_elements quasi_basis Subset-Family of X;
end;

theorem Th08: :: CARDFIL2:25
for X being non empty set
for B being filter_base of X holds <.B.] is Filter of X
proof end;

definition
let X be non empty set ;
let B be filter_base of X;
func <.B.) -> Filter of X equals :: CARDFIL2:def 12
<.B.];
coherence
<.B.] is Filter of X by Th08;
end;

:: deftheorem defines <. CARDFIL2:def 12 :
for X being non empty set
for B being filter_base of X holds <.B.) = <.B.];

theorem :: CARDFIL2:26
for X being non empty set
for B1, B2 being filter_base of X st <.B1.) = <.B2.) holds
B1,B2 are_equivalent_generators
proof end;

theorem :: CARDFIL2:27
for X being non empty set
for FB being filter_base of X
for F being Filter of X st FB c= F holds
<.FB.) is_coarser_than F
proof end;

theorem :: CARDFIL2:28
for X being non empty set
for G being Subset-Family of X st FinMeetCl G is with_non-empty_elements holds
( FinMeetCl G is filter_base of X & ex F being Filter of X st FinMeetCl G c= F )
proof end;

theorem Th09: :: CARDFIL2:29
for X being non empty set
for F being Filter of X
for B being basis of F holds B is filter_base of X
proof end;

theorem Th10: :: CARDFIL2:30
for X being non empty set
for B being filter_base of X holds B is basis of <.B.)
proof end;

theorem :: CARDFIL2:31
for X being non empty set
for F being Filter of X
for B being basis of F
for L being Subset of (BoolePoset X) st L = # B holds
F = uparrow L
proof end;

theorem :: CARDFIL2:32
for X being non empty set
for B being filter_base of X
for L being Subset of (BoolePoset X) st L = B holds
<.B.) = uparrow L by Th04;

theorem Th11: :: CARDFIL2:33
for X being non empty set
for F1, F2 being Filter of X
for B1 being basis of F1
for B2 being basis of F2 holds
( F1 is_filter-coarser_than F2 iff B1 is_coarser_than B2 )
proof end;

theorem Th12: :: CARDFIL2:34
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X
for B being 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 end;

definition
let X, Y be non empty set ;
let f be Function of X,Y;
let 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 } ;
correctness
coherence
{ M where M is Subset of Y : f " M in F } is Filter of Y;
proof end;
end;

:: deftheorem defines filter_image CARDFIL2:def 13 :
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X holds filter_image (f,F) = { M where M is Subset of Y : f " M in F } ;

theorem Th13: :: CARDFIL2:35
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X holds
( f .: F is filter_base of Y & <.(f .: F).] = filter_image (f,F) )
proof end;

theorem :: CARDFIL2:36
for X being non empty set
for B being filter_base of X st B = <.B.) holds
B is Filter of X ;

theorem Th13bThmBA2: :: CARDFIL2:37
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X
for B being basis of F holds
( f .: (# B) is basis of (filter_image (f,F)) & <.(f .: (# B)).] = filter_image (f,F) )
proof end;

theorem :: CARDFIL2:38
for X, Y being non empty set
for f being Function of X,Y
for B1, B2 being filter_base of X st B1 is_coarser_than B2 holds
<.B1.) is_filter-coarser_than <.B2.)
proof end;

theorem :: CARDFIL2:39
for X, Y being non empty set
for f being Function of X,Y
for F being Filter of X holds
( f .: F is Filter of Y iff Y = rng f )
proof end;

theorem :: CARDFIL2:40
for X being non empty set
for A being non empty Subset of X
for F being Filter of A
for B being 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 :: CARDFIL2:def 14
 { (uparrow i) where i is Element of L : verum } ;
coherence
{ (uparrow i) where i is Element of L : verum } is non empty Subset-Family of L
proof end;
end;

:: deftheorem defines Tails CARDFIL2:def 14 :
for L being non empty RelStr holds Tails L = { (uparrow i) where i is Element of L : verum } ;

theorem Th14: :: CARDFIL2:41
for L being non empty reflexive transitive RelStr st [#] L is directed holds
<.(Tails L).] is Filter of [#] L
proof end;

definition
let L be non empty reflexive transitive RelStr ;
assume A1: [#] L is directed ;
func Tails_Filter L -> Filter of [#] L equals :DefL9: :: CARDFIL2:def 15
<.(Tails L).];
coherence
<.(Tails L).] is Filter of [#] L by A1, Th14;
end;

:: deftheorem DefL9 defines Tails_Filter CARDFIL2:def 15 :
for L being non empty reflexive transitive RelStr st [#] L is directed holds
Tails_Filter L = <.(Tails L).];

theorem Th15: :: CARDFIL2:42
for L being non empty reflexive transitive RelStr st [#] L is directed holds
Tails L is basis of (Tails_Filter L)
proof end;

definition
let L be RelStr ;
let x be Subset-Family of L;
func # x -> Subset-Family of ([#] L) equals :: CARDFIL2:def 16
x;
coherence
x is Subset-Family of ([#] L) ;
end;

:: deftheorem defines # CARDFIL2:def 16 :
for L being RelStr
for x being Subset-Family of L holds # x = x;

theorem Th16: :: CARDFIL2:43
for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X st [#] L is directed holds
f .: (# (Tails L)) is basis of (filter_image (f,(Tails_Filter L)))
proof end;

theorem Th17: :: CARDFIL2:44
for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for x being Subset of X st [#] L is directed & x in f .: (# (Tails L)) holds
ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x
proof end;

theorem Th18: :: CARDFIL2:45
for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for x being Subset of X st [#] L is directed & ex j being Element of L st
for i being Element of L st i >= j holds
f . i in x holds
ex b being Element of Tails L st f .: b c= x
proof end;

theorem Th19: :: CARDFIL2:46
for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for F being Filter of X
for B being 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 end;

theorem Th20: :: CARDFIL2:47
for X being non empty set
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L),X
for B being filter_base of X st [#] L is directed holds
( B is_coarser_than f .: (# (Tails L)) iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
proof end;

definition
let X be non empty set ;
let s be sequence of X;
func elementary_filter s -> Filter of X equals :: CARDFIL2:def 17
 filter_image (s,(Frechet_Filter NAT));
correctness
coherence
filter_image (s,(Frechet_Filter NAT)) is Filter of X;
;
end;

:: deftheorem defines elementary_filter CARDFIL2:def 17 :
for X being non empty set
for s being sequence of X holds elementary_filter s = filter_image (s,(Frechet_Filter NAT));

theorem Th21: :: CARDFIL2:48
ex F being sequence of (bool NAT) st
for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y }
proof end;

theorem Th22: :: CARDFIL2:49
for n being natural number holds NAT \ { t where t is Element of NAT : n <= t } is finite
proof end;

Lm3: for p being Element of OrderedNAT
for p0 being 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 end;

Lm4: for p being Element of OrderedNAT holds { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = { x where x is Element of OrderedNAT : p <= x }
proof end;

theorem Th23: :: CARDFIL2:50
for p being Element of OrderedNAT holds { x where x is Element of NAT : ex p0 being Element of NAT st
( p = p0 & p0 <= x ) } = uparrow p
proof end;

registration
cluster [#] OrderedNAT -> directed ;
coherence
[#] OrderedNAT is directed ;
cluster OrderedNAT -> reflexive ;
coherence
OrderedNAT is reflexive by DICKSON:def 3;
end;

theorem Th24: :: CARDFIL2:51
for X being denumerable set holds Frechet_Filter X = { (X \ A) where A is finite Subset of X : verum }
proof end;

theorem Th25: :: CARDFIL2:52
for F being sequence of (bool NAT) st ( for x being 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 end;

theorem Th26: :: CARDFIL2:53
for F being sequence of (bool NAT) st ( for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y } ) holds
# (Tails OrderedNAT) = rng F
proof end;

theorem Th27: :: CARDFIL2:54
( # (Tails OrderedNAT) is basis of (Frechet_Filter NAT) & Tails_Filter OrderedNAT = Frechet_Filter NAT )
proof end;

definition
func base_of_frechet_filter -> filter_base of NAT equals :: CARDFIL2:def 18
 # (Tails OrderedNAT);
coherence
# (Tails OrderedNAT) is filter_base of NAT by Th27, Th09;
end;

:: deftheorem defines base_of_frechet_filter CARDFIL2:def 18 :
base_of_frechet_filter = # (Tails OrderedNAT);

theorem :: CARDFIL2:55
NAT in base_of_frechet_filter
proof end;

theorem :: CARDFIL2:56
base_of_frechet_filter is basis of (Frechet_Filter NAT) by Th27;

theorem :: CARDFIL2:57
for X being non empty set
for F1, F2, F being Filter of X st F is_filter-finer_than F1 & F is_filter-finer_than F2 holds
for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty
proof end;

theorem :: CARDFIL2:58
for X being non empty set
for F1, F2 being Filter of X st ( for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty ) holds
ex F being Filter of X st
( F is_filter-finer_than F1 & F is_filter-finer_than F2 )
proof end;

definition
let X be set ;
let x be Subset of X;
func PLO2bis x -> Element of (BoolePoset X) equals :: CARDFIL2:def 19
x;
coherence
x is Element of (BoolePoset X) by LATTICE3:def 1;
end;

:: deftheorem defines PLO2bis CARDFIL2:def 19 :
for X being set
for x being Subset of X holds PLO2bis x = x;

theorem Th28: :: CARDFIL2:59
for X being infinite set holds X in { (X \ A) where A is finite Subset of X : verum }
proof end;

theorem Th29: :: CARDFIL2:60
for X being set
for A being 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 end;

theorem :: CARDFIL2:61
for X being set
for a being Element of (BoolePoset X) holds uparrow a = { Y where Y is Subset of X : a c= Y } by WAYBEL15:2;

theorem :: CARDFIL2:62
for X being set
for A being Subset of X holds { B where B is Element of (BoolePoset X) : A c= B } = uparrow (PLO2bis A)
proof end;

theorem :: CARDFIL2:63
for X being non empty set
for F being Filter of X holds union F = X by CARD_FIL:5, ZFMISC_1:74;

theorem :: CARDFIL2:64
for X being infinite set holds { (X \ A) where A is finite Subset of X : verum } is Filter of X
proof end;

theorem :: CARDFIL2:65
for X being set holds bool X is Filter of (BoolePoset X) by WAYBEL16:11;

theorem :: CARDFIL2:66
for X being set holds {X} is Filter of (BoolePoset X) by WAYBEL16:12;

theorem :: CARDFIL2:67
for X being non empty set holds {X} is Filter of X by CARD_FIL:4;

theorem Th30Thm70: :: CARDFIL2:68
for X being non empty set
for A being Element of (BoolePoset X) holds { Y where Y is Subset of X : A c= Y } is Filter of (BoolePoset X)
proof end;

theorem :: CARDFIL2:69
for X being non empty set
for A being Element of (BoolePoset X) holds { B where B is Element of (BoolePoset X) : A c= B } is Filter of (BoolePoset X)
proof end;

theorem :: CARDFIL2:70
for X being non empty set
for B being non empty Subset of (BoolePoset X) holds
( ( for x, y being Element of B ex z being Element of B st z c= x /\ y ) iff B is filtered )
proof end;

theorem Th31: :: CARDFIL2:71
for X being non empty set
for 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
for q being Element of (BooleLatt X) st p c= q holds
q in F ) ) )
proof end;

theorem Th32: :: CARDFIL2:72
for X being non empty set
for F being non empty Subset of (BooleLatt X) holds
( F is Filter of (BooleLatt X) iff for Y1, Y2 being 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 end;

theorem Th33: :: CARDFIL2:73
for X being non empty set
for FF being non empty Subset-Family of X st FF is Filter of (BooleLatt X) holds
FF is Filter of (BoolePoset X)
proof end;

theorem Th34: :: CARDFIL2:74
for X being non empty set
for F being Filter of (BoolePoset X) holds F is Filter of (BooleLatt X)
proof end;

theorem Th35: :: CARDFIL2:75
for X being non empty set
for F being 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 end;

theorem Th36: :: CARDFIL2:76
for X being non empty set
for F being proper Filter of (BoolePoset X) holds F is Filter of X
proof end;

theorem :: CARDFIL2:77
for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x is Filter of the carrier of T by Th36;

definition
let T be non empty TopSpace;
let F be proper Filter of (BoolePoset ([#] T));
func BOOL2F F -> Filter of the carrier of T equals :: CARDFIL2:def 20
F;
coherence
F is Filter of the carrier of T by Th36;
end;

:: deftheorem defines BOOL2F CARDFIL2:def 20 :
for T being non empty TopSpace
for F being proper Filter of (BoolePoset ([#] T)) holds BOOL2F F = F;

definition
let T be non empty TopSpace;
let F1 be Filter of the carrier of T;
let F2 be proper Filter of (BoolePoset ([#] T));
pred F1 is_filter-finer_than F2 means :: CARDFIL2:def 21
 BOOL2F F2 c= F1;
end;

:: deftheorem defines is_filter-finer_than CARDFIL2:def 21 :
for T being non empty TopSpace
for F1 being Filter of the carrier of T
for F2 being proper Filter of (BoolePoset ([#] T)) holds
( F1 is_filter-finer_than F2 iff BOOL2F F2 c= F1 );

definition
let T be non empty TopSpace;
let 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 } ;
correctness
coherence
{ x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } is Subset of T;
proof end;
end;

:: deftheorem defines lim_filter CARDFIL2:def 22 :
for T being non empty TopSpace
for F being Filter of the carrier of T holds lim_filter F = { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;

definition
let T be non empty TopSpace;
let B be filter_base of the carrier of T;
func Lim B -> Subset of T equals :: CARDFIL2:def 23
 lim_filter <.B.);
correctness
coherence
lim_filter <.B.) is Subset of T;
;
end;

:: deftheorem defines Lim CARDFIL2:def 23 :
for T being non empty TopSpace
for B being filter_base of the carrier of T holds Lim B = lim_filter <.B.);

theorem Th37: :: CARDFIL2:78
for T being non empty TopSpace
for F being Filter of the carrier of T ex F1 being proper Filter of (BoolePoset the carrier of T) st F = F1
proof end;

definition
let T be non empty TopSpace;
let F be Filter of the carrier of T;
func F2BOOL (F,T) -> proper Filter of (BoolePoset ([#] T)) equals :: CARDFIL2:def 24
F;
coherence
F is proper Filter of (BoolePoset ([#] T))
proof end;
end;

:: deftheorem defines F2BOOL CARDFIL2:def 24 :
for T being non empty TopSpace
for F being Filter of the carrier of T holds F2BOOL (F,T) = F;

theorem :: CARDFIL2:79
for T being non empty TopSpace
for x being Point of T
for F being 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
for x being Point of T
for F being Filter of the carrier of T holds
( x is_a_convergence_point_of F,T iff x in lim_filter F )
proof end;

definition
let T be non empty TopSpace;
let 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 } ;
correctness
coherence
{ x where x is Point of T : NeighborhoodSystem x c= F } is Subset of T;
proof end;
end;

:: deftheorem defines lim_filterb CARDFIL2:def 25 :
for T being non empty TopSpace
for F being Filter of (BoolePoset ([#] T)) holds lim_filterb F = { x where x is Point of T : NeighborhoodSystem x c= F } ;

theorem :: CARDFIL2:81
for T being non empty TopSpace
for F being Filter of the carrier of T holds lim_filter F = lim_filterb (F2BOOL (F,T))
proof end;

theorem :: CARDFIL2:82
for T being non empty TopSpace
for F being Filter of the carrier of T holds Lim (a_net (F2BOOL (F,T))) = lim_filter F
proof end;

theorem Th38: :: CARDFIL2:83
for T being non empty Hausdorff TopSpace
for F being Filter of the carrier of T
for p, q being Point of T st p in lim_filter F & q in lim_filter F holds
p = q
proof end;

registration
let T be non empty Hausdorff TopSpace;
let F be Filter of the carrier of T;
cluster lim_filter F -> trivial ;
coherence
lim_filter F is trivial
proof end;
end;

definition
let X be non empty set ;
let T be non empty TopSpace;
let f be Function of X, the carrier of T;
let F be Filter of X;
func lim_filter (f,F) -> Subset of ([#] T) equals :: CARDFIL2:def 26
 lim_filter (filter_image (f,F));
coherence
lim_filter (filter_image (f,F)) is Subset of ([#] T) ;
end;

:: deftheorem defines lim_filter CARDFIL2:def 26 :
for X being non empty set
for T being non empty TopSpace
for f being Function of X, the carrier of T
for F being Filter of X holds lim_filter (f,F) = lim_filter (filter_image (f,F));

definition
let T be non empty TopSpace;
let L be non empty reflexive transitive RelStr ;
let 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)));
coherence
lim_filter (filter_image (f,(Tails_Filter L))) is Subset of ([#] T) ;
end;

:: deftheorem defines lim_f CARDFIL2:def 27 :
for T being non empty TopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T holds lim_f f = lim_filter (filter_image (f,(Tails_Filter L)));

theorem :: CARDFIL2:84
for T being non empty TopSpace
for L being non empty reflexive transitive RelStr
for f being Function of ([#] L), the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) st [#] L is directed holds
( x in lim_f f iff for b being Element of B ex i being Element of L st
for j being Element of L st i <= j holds
f . j in b )
proof end;

definition
let T be non empty TopSpace;
let s be sequence of T;
func lim_f s -> Subset of T equals :: CARDFIL2:def 28
 lim_filter (elementary_filter s);
coherence
lim_filter (elementary_filter s) is Subset of T ;
end;

:: deftheorem defines lim_f CARDFIL2:def 28 :
for T being non empty TopSpace
for s being sequence of T holds lim_f s = lim_filter (elementary_filter s);

theorem :: CARDFIL2:85
for T being non empty TopSpace
for s being sequence of T holds lim_filter (s,(Frechet_Filter NAT)) = lim_f s ;

theorem :: CARDFIL2:86
for T being non empty TopSpace
for x being Point of T holds NeighborhoodSystem x is filter_base of ([#] T)
proof end;

theorem :: CARDFIL2:87
for T being non empty TopSpace
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds B is filter_base of ([#] T) by Th09;

theorem :: CARDFIL2:88
for X being non empty set
for s being sequence of X
for B being filter_base of X holds
( B is_coarser_than s .: base_of_frechet_filter iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) by Th20;

theorem Th39: :: CARDFIL2:89
for T being non empty TopSpace
for s being sequence of T
for x being Point of T
for 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 end;

theorem Th40: :: CARDFIL2:90
for T being non empty TopSpace
for s being sequence of ([#] T)
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( B is_coarser_than s .: base_of_frechet_filter iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b )
proof end;

theorem Th41: :: CARDFIL2:91
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_filter (s,(Frechet_Filter NAT)) iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b )
proof end;

theorem Th42: :: CARDFIL2:92
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b )
proof end;

definition
let L be 1-sorted ;
let 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 #);
coherence
NetStr(# NAT,NATOrd,s #) is non empty strict NetStr over L ;
end;

:: deftheorem defines sequence_to_net CARDFIL2:def 29 :
for L being 1-sorted
for s being sequence of the carrier of L holds sequence_to_net s = NetStr(# NAT,NATOrd,s #);

registration
let L be non empty 1-sorted ;
let s be sequence of the carrier of L;
cluster sequence_to_net s -> non empty strict ;
coherence
not sequence_to_net s is empty ;
end;

theorem Th43: :: CARDFIL2:93
for L being non empty 1-sorted
for B being set
for 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: :: CARDFIL2:94
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( ( for b being Element of B ex i being Element of OrderedNAT st
for j being Element of OrderedNAT st i <= j holds
s . j in b ) iff for b being Element of B 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 )
proof end;

theorem :: CARDFIL2:95
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B holds sequence_to_net s is_eventually_in b )
proof end;

theorem Th45: :: CARDFIL2:96
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Element of NAT st
for j being Element of NAT st i <= j holds
s . j in b )
proof end;

theorem :: CARDFIL2:97
for T being non empty TopSpace
for s being sequence of the carrier of T
for x being Point of T
for B being basis of (BOOL2F (NeighborhoodSystem x)) holds
( x in lim_f s iff for b being Element of B ex i being Nat st
for j being Nat st i <= j holds
s . j in b )
proof end;