:: 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 b₁ being cap-closed Subset-Family of X holds b₁ is empty

proof end;

end;

registration

let X be set ;

cluster non empty cap-closed upper for Element of bool (bool X);

existence
ex b₁ being non empty cap-closed Subset-Family of X st b₁ 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 b₁ being non empty cap-closed upper Subset-Family of X st b₁ 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 b₁ being non empty set st b₁ 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 b₁ being non empty set st b₁ is cap-finite-closed holds
b₁ 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 b₁ being Filter of X holds b₁ 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 b₁ -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 b₁ -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 b₁ being non empty Subset of F st b₁ 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 b₁ being Subset-Family of X st
for x being Subset of X holds
( x in b₁ iff ex b being Element of B st b c= x )

proof end;

correctness
uniqueness
for b₁, b₂ being Subset-Family of X st ( for x being Subset of X holds
( x in b₁ iff ex b being Element of B st b c= x ) ) & ( for x being Subset of X holds
( x in b₂ iff ex b being Element of B st b c= x ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem def3 defines <. CARDFIL2:def 8 :
for X being set
for B, b₃ being Subset-Family of X holds
( b₃ = <.B.] iff for x being Subset of X holds
( x in b₃ 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 b₁ being non empty Subset-Family of X st b₁ 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 b₁ being non empty quasi_basis Subset-Family of X st b₁ 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;