:: by Roland Coghetto

::

:: Received June 30, 2015

:: Copyright (c) 2015-2017 Association of Mizar Users

:: 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 );

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 ;

existence

not for b_{1} being cap-closed Subset-Family of X holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let X be set ;

existence

ex b_{1} being non empty cap-closed Subset-Family of X st b_{1} is upper

end;
existence

ex b

proof end;

registration

let X be non empty set ;

existence

ex b_{1} being non empty cap-closed upper Subset-Family of X st b_{1} is with_non-empty_elements

end;
existence

ex b

proof 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;

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:]

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 ;

end;
attr X is cap-finite-closed means :: CARDFIL2:def 2

for SX being non empty finite Subset of X holds meet SX in X;

for SX being non empty finite Subset of X holds meet SX in X;

:: 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 );

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

coherence

for b_{1} being non empty set st b_{1} is cap-finite-closed holds

b_{1} is cap-closed
by Th01;

end;
for b

b

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 )

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

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 ;

coherence

for b_{1} being Filter of X holds b_{1} is cap-closed
by CARD_FIL:def 1;

end;
coherence

for b

definition

let X be non empty set ;

correctness

coherence

{ F where F is Filter of X : verum } is non empty set ;

end;
correctness

coherence

{ F where F is Filter of X : verum } is non empty set ;

proof end;

:: deftheorem defines Filt CARDFIL2:def 3 :

for X being non empty set holds Filt X = { F where F is Filter of X : verum } ;

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;

coherence

meet (rng M) is Filter of X

end;
let M be Filt X -valued ManySortedSet of I;

coherence

meet (rng M) is Filter of X

proof end;

:: deftheorem defines Filter_Intersection CARDFIL2:def 4 :

for X, I being non empty set

for M being Filt b_{1} -valued ManySortedSet of I holds Filter_Intersection M = meet (rng M);

for X, I being non empty set

for M being Filt b

definition

let X be non empty set ;

let F1, F2 be Filter of X;

reflexivity

for F1 being Filter of X holds F1 c= F1 ;

reflexivity

for F1 being Filter of X holds F1 c= F1 ;

end;
let F1, F2 be Filter of X;

reflexivity

for F1 being Filter of X holds F1 c= F1 ;

reflexivity

for F1 being Filter of X holds F1 c= F1 ;

:: 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 );

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 );

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:9

for X, I being non empty set

for M being Filt b_{1} -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

for M being Filt b

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

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 )

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;

end;
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;

for f being Element of F ex b being Element of B st b c= f;

:: 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 );

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 )

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;

existence

ex b_{1} being non empty Subset of F st b_{1} is filter_basis

end;
let F be Filter of X;

existence

ex b

proof end;

definition
end;

definition

let X be set ;

let B be Subset-Family of X;

ex b_{1} being Subset-Family of X st

for x being Subset of X holds

( x in b_{1} iff ex b being Element of B st b c= x )

uniqueness

for b_{1}, b_{2} being Subset-Family of X st ( for x being Subset of X holds

( x in b_{1} iff ex b being Element of B st b c= x ) ) & ( for x being Subset of X holds

( x in b_{2} iff ex b being Element of B st b c= x ) ) holds

b_{1} = b_{2};

end;
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 for x being Subset of X holds

( x in it iff ex b being Element of B st b c= x );

ex b

for x being Subset of X holds

( x in b

proof end;

correctness uniqueness

for b

( x in b

( x in b

b

proof end;

:: deftheorem def3 defines <. CARDFIL2:def 8 :

for X being set

for B, b_{3} being Subset-Family of X holds

( b_{3} = <.B.] iff for x being Subset of X holds

( x in b_{3} iff ex b being Element of B st b c= x ) );

for X being set

for B, b

( b

( x in b

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 }

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 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

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;

definition

let X be set ;

let B1, B2 be Subset-Family of X;

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;
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 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 ) );

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 ) ) ;

:: 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 ) ) );

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.]

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;

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;

coherence

B is non empty Subset-Family of X by XBOOLE_1:1;

end;
let F be Filter of X;

let B be non empty Subset of F;

coherence

B is non empty Subset-Family of X by XBOOLE_1:1;

:: 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;

for X being non empty set

for F being Filter of X

for B being non empty Subset of F holds # B = B;

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

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

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

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;

end;
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;

for b1, b2 being Element of B ex b being Element of B st b c= b1 /\ b2;

:: 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 );

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 ;

existence

ex b_{1} being non empty Subset-Family of X st b_{1} is quasi_basis

end;
existence

ex b

proof end;

registration

let X be non empty set ;

existence

ex b_{1} being non empty quasi_basis Subset-Family of X st b_{1} is with_non-empty_elements

end;
existence

ex b

proof 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;
mode filter_base of X is non empty with_non-empty_elements quasi_basis Subset-Family of X;

definition
end;

:: deftheorem defines <. CARDFIL2:def 12 :

for X being non empty set

for B being filter_base of X holds <.B.) = <.B.];

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

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

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 )

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

for F being Filter of X

for B being basis of F holds B is filter_base of X

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

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

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 )

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 } )

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;

coherence

{ M where M is Subset of Y : f " M in F } is Filter of Y;

end;
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 { M where M is Subset of Y : f " M in F } ;

coherence

{ M where M is Subset of Y : f " M in F } is Filter of Y;

proof 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 } ;

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) )

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

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) )

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.)

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 )

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

definition

let L be non empty RelStr ;

{ (uparrow i) where i is Element of L : verum } is non empty Subset-Family of L

end;
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 } ;

{ (uparrow i) where i is Element of L : verum } is non empty Subset-Family of L

proof 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 } ;

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

<.(Tails L).] is Filter of [#] L

proof end;

definition

let L be non empty reflexive transitive RelStr ;

assume A1: [#] L is directed ;

coherence

<.(Tails L).] is Filter of [#] L by A1, Th14;

end;
assume A1: [#] L is directed ;

coherence

<.(Tails L).] is Filter of [#] L by A1, Th14;

:: 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).];

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)

Tails L is basis of (Tails_Filter L)

proof end;

definition
end;

:: deftheorem defines # CARDFIL2:def 16 :

for L being RelStr

for x being Subset-Family of L holds # x = x;

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)))

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

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

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)) )

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 )

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;

coherence

filter_image (s,(Frechet_Filter NAT)) is Filter of X;

;

end;
let s be sequence of X;

func elementary_filter s -> Filter of X equals :: CARDFIL2:def 17

filter_image (s,(Frechet_Filter NAT));

correctness filter_image (s,(Frechet_Filter NAT));

coherence

filter_image (s,(Frechet_Filter NAT)) is Filter of X;

;

:: 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));

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 }

for x being Element of NAT holds F . x = { y where y is Element of NAT : x <= y }

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

( p = p0 & p0 <= x ) } = uparrow p

proof end;

registration
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)

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

# (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;

:: deftheorem defines base_of_frechet_filter CARDFIL2:def 18 :

base_of_frechet_filter = # (Tails OrderedNAT);

base_of_frechet_filter = # (Tails OrderedNAT);

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

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 )

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
end;

:: deftheorem defines PLO2bis CARDFIL2:def 19 :

for X being set

for x being Subset of X holds PLO2bis x = x;

for X being set

for x being Subset of X holds PLO2bis x = x;

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 }

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;

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)

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

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)

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)

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 )

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 ) ) )

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 ) ) )

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)

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 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 )

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 :: CARDFIL2:77

definition

let T be non empty TopSpace;

let F be proper Filter of (BoolePoset ([#] T));

coherence

F is Filter of the carrier of T by Th36;

end;
let F be proper Filter of (BoolePoset ([#] T));

coherence

F is Filter of the carrier of T by Th36;

:: deftheorem defines BOOL2F CARDFIL2:def 20 :

for T being non empty TopSpace

for F being proper Filter of (BoolePoset ([#] T)) holds BOOL2F F = F;

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));

end;
let F1 be Filter of the carrier of T;

let F2 be proper Filter of (BoolePoset ([#] T));

:: 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 );

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;

coherence

{ x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } is Subset of T;

end;
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 { x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } ;

coherence

{ x where x is Point of T : F is_filter-finer_than NeighborhoodSystem x } is Subset of T;

proof 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 } ;

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;

correctness

coherence

lim_filter <.B.) is Subset of T;

;

end;
let B be filter_base of the carrier of T;

correctness

coherence

lim_filter <.B.) is Subset of T;

;

:: 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.);

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

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;

coherence

F is proper Filter of (BoolePoset ([#] T))

end;
let F be Filter of the carrier of T;

coherence

F is proper Filter of (BoolePoset ([#] T))

proof 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;

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 ) ;

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 )

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));

coherence

{ x where x is Point of T : NeighborhoodSystem x c= F } is Subset of T;

end;
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 { x where x is Point of T : NeighborhoodSystem x c= F } ;

coherence

{ x where x is Point of T : NeighborhoodSystem x c= F } is Subset of T;

proof 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 } ;

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))

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

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

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;

coherence

lim_filter F is trivial

end;
let F be Filter of the carrier of T;

coherence

lim_filter F is trivial

proof 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;

lim_filter (filter_image (f,F)) is Subset of ([#] T) ;

end;
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));

lim_filter (filter_image (f,F)) is Subset of ([#] T) ;

:: 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));

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;

lim_filter (filter_image (f,(Tails_Filter L))) is Subset of ([#] T) ;

end;
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)));

lim_filter (filter_image (f,(Tails_Filter L))) is Subset of ([#] T) ;

:: 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)));

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 )

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;

coherence

lim_filter (elementary_filter s) is Subset of T ;

end;
let s be sequence of T;

coherence

lim_filter (elementary_filter s) is Subset of T ;

:: 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);

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 ;

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)

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;

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;

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 )

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 )

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 )

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 )

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;

NetStr(# NAT,NATOrd,s #) is non empty strict NetStr over L ;

end;
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 #);

NetStr(# NAT,NATOrd,s #) is non empty strict NetStr over L ;

:: 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 #);

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;

coherence

not sequence_to_net s is empty ;

end;
let s be sequence of the carrier of L;

coherence

not sequence_to_net s is empty ;

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 ) ;

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 )

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 )

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 )

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 )

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;