:: CARD_FIL semantic presentation

definition

let X, Y be set ;
:: original: \
redefine func X \ Y -> Subset of X;
coherence by XBOOLE_1:36;

end;

theorem Th1: :: CARD_FIL:1

for x being set
for X being infinite set holds Card {x} <` Card X

proof end;

registration

let X be infinite set ;
cluster Card X -> infinite ;
coherence by CARD_4:1;

end;

scheme :: CARD_FIL:sch 1
ElemProp{ F₁() -> non empty set , F₂() -> set , P₁[ set ] } :

P₁[F₂()]

provided

A1: F₂() in { y where y is Element of F₁() : P₁[y] }

proof end;

theorem Th2: :: CARD_FIL:2

for X being non empty set holds
( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )

proof end;

definition

let X be non empty set ;
mode Filter of X -> non empty Subset-Family of X means :Def1: :: CARD_FIL:def 1
( not {} in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 /\ Y2 in it ) & ( Y1 in it & Y1 c= Y2 implies Y2 in it ) ) ) );
existence

proof end;

end;

:: deftheorem Def1 defines Filter CARD_FIL:def 1 :

theorem :: CARD_FIL:3

for X being non empty set
for F being set holds
( F is Filter of X iff ( F is non empty Subset-Family of X & not {} in F & ( 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 ) ) ) ) ) by Def1;

theorem Th4: :: CARD_FIL:4

for X being non empty set holds {X} is Filter of X

proof end;

theorem Th5: :: CARD_FIL:5

for X being non empty set
for F being Filter of X holds X in F

proof end;

theorem Th6: :: CARD_FIL:6

for X being non empty set
for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F

proof end;

theorem Th7: :: CARD_FIL:7

for X being non empty set
for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )

proof end;

notation

let X be non empty set ;
let S be Subset-Family of X;
synonym dual S for COMPLEMENT S;

end;

registration

let X be non empty set ;
let S be non empty Subset-Family of X;
cluster dual S -> non empty ;
coherence by SETFAM_1:46;

end;

theorem :: CARD_FIL:8

for X being non empty set
for S being non empty Subset-Family of X holds dual S = { Y where Y is Subset of X : Y ` in S }

proof end;

theorem Th9: :: CARD_FIL:9

for X being non empty set
for S being non empty Subset-Family of X holds dual S = { (Y ` ) where Y is Subset of X : Y in S }

proof end;

definition

let X be non empty set ;
mode Ideal of X -> non empty Subset-Family of X means :Def2: :: CARD_FIL:def 2
( not X in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 \/ Y2 in it ) & ( Y1 in it & Y2 c= Y1 implies Y2 in it ) ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines Ideal CARD_FIL:def 2 :

definition

let X be non empty set ;
let F be Filter of X;
:: original: dual
redefine func dual F -> Ideal of X;
coherence

proof end;

end;

theorem Th10: :: CARD_FIL:10

for X being non empty set
for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )

proof end;

theorem Th11: :: CARD_FIL:11

for X being non empty set
for I being Ideal of X holds {} in I

proof end;

definition

let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
pred S is_multiplicative_with N means :Def3: :: CARD_FIL:def 3
for S1 being non empty set st S1 c= S & Card S1 <` N holds
meet S1 in S;

end;

:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def 3 :

definition

let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
pred S is_additive_with N means :Def4: :: CARD_FIL:def 4
for S1 being non empty set st S1 c= S & Card S1 <` N holds
union S1 in S;

end;

:: deftheorem Def4 defines is_additive_with CARD_FIL:def 4 :

notation

let X be non empty set ;
let N be Cardinal;
let F be Filter of X;
synonym F is_complete_with N for F is_multiplicative_with N;

end;

notation

let X be non empty set ;
let N be Cardinal;
let I be Ideal of X;
synonym I is_complete_with N for I is_additive_with N;

end;

theorem Th12: :: CARD_FIL:12

for N being Cardinal
for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N

proof end;

definition

let X be non empty set ;
let F be Filter of X;
attr F is uniform means :Def5: :: CARD_FIL:def 5
for Y being Subset of X st Y in F holds
Card Y = Card X;
attr F is principal means :Def6: :: CARD_FIL:def 6
ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) );
attr F is being_ultrafilter means :Def7: :: CARD_FIL:def 7
for Y being Subset of X holds
( Y in F or X \ Y in F );

end;

:: deftheorem Def5 defines uniform CARD_FIL:def 5 :

:: deftheorem Def6 defines principal CARD_FIL:def 6 :

:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def 7 :

definition

let X be non empty set ;
let F be Filter of X;
let Z be Subset of X;
func Extend_Filter F,Z -> non empty Subset-Family of X equals :: CARD_FIL:def 8
{ Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in { (Y1 /\ Z) where Y1 is Subset of X : Y1 in F } & Y2 c= Y ) } ;
coherence

proof end;

end;

:: deftheorem defines Extend_Filter CARD_FIL:def 8 :

theorem Th13: :: CARD_FIL:13

for X being non empty set
for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter F,Z iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )

proof end;

theorem Th14: :: CARD_FIL:14

for X being non empty set
for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter F,Z & Extend_Filter F,Z is Filter of X & F c= Extend_Filter F,Z )

proof end;

definition

let X be non empty set ;
func Filters X -> non empty Subset-Family of (bool X) equals :: CARD_FIL:def 9
{ S where S is Subset-Family of X : S is Filter of X } ;
coherence

proof end;

end;

:: deftheorem defines Filters CARD_FIL:def 9 :

theorem Th15: :: CARD_FIL:15

for X being non empty set
for S being set holds
( S in Filters X iff S is Filter of X )

proof end;

theorem Th16: :: CARD_FIL:16

for X being non empty set
for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X

proof end;

theorem Th17: :: CARD_FIL:17

for X being non empty set
for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )

proof end;

definition

let X be infinite set ;
func Frechet_Filter X -> Filter of X equals :: CARD_FIL:def 10
{ Y where Y is Subset of X : Card (X \ Y) <` Card X } ;
coherence

proof end;

end;

:: deftheorem defines Frechet_Filter CARD_FIL:def 10 :

definition

let X be infinite set ;
func Frechet_Ideal X -> Ideal of X equals :: CARD_FIL:def 11
dual (Frechet_Filter X);
coherence ;

end;

:: deftheorem defines Frechet_Ideal CARD_FIL:def 11 :

theorem Th18: :: CARD_FIL:18

for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff Card (X \ Y) <` Card X )

proof end;

theorem Th19: :: CARD_FIL:19

for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Ideal X iff Card Y <` Card X )

proof end;

theorem Th20: :: CARD_FIL:20

for X being infinite set
for F being Filter of X st Frechet_Filter X c= F holds
F is uniform

proof end;

theorem :: CARD_FIL:21

for X being infinite set
for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf

proof end;

registration

let X be infinite set ;
cluster non empty non principal being_ultrafilter Filter of X;
existence

proof end;

end;

registration

let X be infinite set ;
cluster uniform being_ultrafilter -> non principal Filter of X;
coherence

proof end;

end;

theorem Th22: :: CARD_FIL:22

for X being infinite set
for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )

proof end;

theorem Th23: :: CARD_FIL:23

for X being infinite set
for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with Card X holds
F is uniform

proof end;

theorem Th24: :: CARD_FIL:24

for N being Cardinal holds nextcard N <=` exp 2,N

proof end;

definition

pred GCH means :Def12: :: CARD_FIL:def 12
for N being Aleph holds nextcard N = exp 2,N;

end;

:: deftheorem Def12 defines GCH CARD_FIL:def 12 :

definition

let IT be Aleph;
attr IT is inaccessible means :Def13: :: CARD_FIL:def 13
( IT is regular & IT is limit );

end;

:: deftheorem Def13 defines inaccessible CARD_FIL:def 13 :

notation

let IT be Aleph;
synonym IT is_inaccessible_cardinal for inaccessible IT;

end;

registration

cluster inaccessible -> limit regular set ;
coherence by Def13;

end;

theorem :: CARD_FIL:25

alef 0 is inaccessible

proof end;

definition

let IT be Aleph;
attr IT is strong_limit means :Def14: :: CARD_FIL:def 14
for N being Cardinal st N <` IT holds
exp 2,N <` IT;

end;

:: deftheorem Def14 defines strong_limit CARD_FIL:def 14 :

notation

let IT be Aleph;
synonym IT is_strong_limit_cardinal for strong_limit IT;

end;

theorem Th26: :: CARD_FIL:26

alef 0 is strong_limit

proof end;

theorem Th27: :: CARD_FIL:27

for M being Aleph st M is strong_limit holds
M is limit

proof end;

registration

cluster strong_limit -> limit set ;
coherence by Th27;

end;

theorem Th28: :: CARD_FIL:28

for M being Aleph st GCH & M is limit holds
M is strong_limit

proof end;

definition

let IT be Aleph;
attr IT is strongly_inaccessible means :Def15: :: CARD_FIL:def 15
( IT is regular & IT is strong_limit );

end;

:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def 15 :

notation

let IT be Aleph;
synonym IT is_strongly_inaccessible_cardinal for strongly_inaccessible IT;

end;

registration

cluster strongly_inaccessible -> limit regular strong_limit set ;
coherence by Def15;

end;

theorem :: CARD_FIL:29

alef 0 is strongly_inaccessible by Def15, Th26, CARD_5:42;

theorem Th30: :: CARD_FIL:30

for M being Aleph st M is strongly_inaccessible holds
M is inaccessible

proof end;

registration

cluster strongly_inaccessible -> limit regular inaccessible set ;
coherence by Th30;

end;

theorem :: CARD_FIL:31

for M being Aleph st GCH & M is inaccessible holds
M is strongly_inaccessible

proof end;

definition

let M be Aleph;
attr M is measurable means :Def16: :: CARD_FIL:def 16
ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter );

end;

:: deftheorem Def16 defines measurable CARD_FIL:def 16 :

notation

let M be Aleph;
synonym M is_measurable_cardinal for measurable M;

end;

theorem Th32: :: CARD_FIL:32

for A being being_limit_ordinal Ordinal
for X being set st X c= A & sup X = A holds
union X = A

proof end;

theorem Th33: :: CARD_FIL:33

for M being Aleph st M is measurable holds
M is regular

proof end;

registration

let M be Aleph;
cluster nextcard M -> non limit ;
coherence

proof end;

end;

registration

cluster infinite non limit set ;
existence

proof end;

end;

registration

cluster non limit -> regular set ;
coherence

proof end;

end;

definition

let M be non limit Cardinal;
func predecessor M -> Cardinal means :Def17: :: CARD_FIL:def 17
M = nextcard it;
existence by CARD_1:def 7;
uniqueness by CARD_4:21;

end;

:: deftheorem Def17 defines predecessor CARD_FIL:def 17 :

registration

let M be non limit Aleph;
cluster predecessor M -> infinite ;
coherence

proof end;

end;

definition

let X be set ;
let N, N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;

end;

definition

let M be non limit Aleph;
let T be Inf_Matrix of (predecessor M),M, bool M;
pred T is_Ulam_Matrix_of M means :Def18: :: CARD_FIL:def 18
( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . N1,K1) /\ (T . N1,K2) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . N1,K1) /\ (T . N2,K1) is empty ) & ( for N1 being Element of predecessor M holds Card (M \ (union { (T . N1,K1) where K1 is Element of M : K1 in M } )) <=` predecessor M ) & ( for K1 being Element of M holds Card (M \ (union { (T . N1,K1) where N1 is Element of predecessor M : N1 in predecessor M } )) <=` predecessor M ) );

end;

:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def 18 :

theorem Th34: :: CARD_FIL:34

for M being non limit Aleph ex T being Inf_Matrix of (predecessor M),M, bool M st T is_Ulam_Matrix_of M

proof end;

theorem Th35: :: CARD_FIL:35

for M being non limit Aleph
for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( Card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )

proof end;

theorem Th36: :: CARD_FIL:36

for X being set
for N being Cardinal st N <=` Card X holds
ex Y being set st
( Y c= X & Card Y = N )

proof end;

theorem Th37: :: CARD_FIL:37

for M being non limit Aleph
for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )

proof end;

theorem Th38: :: CARD_FIL:38

for M being Aleph st M is measurable holds
M is limit

proof end;

theorem :: CARD_FIL:39

for M being Aleph st M is measurable holds
M is inaccessible

proof end;

theorem Th40: :: CARD_FIL:40

for M being Aleph st M is measurable holds
M is strong_limit

proof end;

theorem :: CARD_FIL:41

for M being Aleph st M is measurable holds
M is strongly_inaccessible

proof end;