:: by Sebastian Koch

::

:: Received October 25, 2020

:: Copyright (c) 2020-2021 Association of Mizar Users

registration
end;

:: deftheorem Def1 defines ext-natural COUNTERS:def 2 :

for x being object holds

( x is ext-natural iff x in ExtNAT );

for x being object holds

( x is ext-natural iff x in ExtNAT );

registration

coherence

+infty is ext-natural by ZFMISC_1:136;

coherence

for b_{1} being object st b_{1} is ext-natural holds

b_{1} is ext-real
;

coherence

for b_{1} being object st b_{1} is natural holds

b_{1} is ext-natural

for b_{1} being set st b_{1} is finite & b_{1} is ext-natural holds

b_{1} is natural

end;
+infty is ext-natural by ZFMISC_1:136;

coherence

for b

b

coherence

for b

b

proof end;

coherence for b

b

proof end;

registration

existence

ex b_{1} being object st

( b_{1} is zero & b_{1} is ext-natural )

ex b_{1} being object st

( not b_{1} is zero & b_{1} is ext-natural )

ex b_{1} being number st b_{1} is ext-natural

for b_{1} being Element of ExtNAT holds b_{1} is ext-natural
;

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

existence ex b

proof end;

coherence for b

registration
end;

registration
end;

registration

coherence

for b_{1} being object st b_{1} is zero holds

b_{1} is ext-natural
;

coherence

for b_{1} being ExtReal st b_{1} is ext-natural holds

not b_{1} is negative
by Th3;

end;
for b

b

coherence

for b

not b

registration

coherence

for b_{1} being ExtNat holds not b_{1} is negative
;

coherence

for b_{1} being ExtNat st not b_{1} is zero holds

b_{1} is positive
;

end;
for b

coherence

for b

b

registration

let N, M be ExtNat;

coherence

min (N,M) is ext-natural by XXREAL_0:def 9;

coherence

max (N,M) is ext-natural by XXREAL_0:def 10;

coherence

N + M is ext-natural

N * M is ext-natural

end;
coherence

min (N,M) is ext-natural by XXREAL_0:def 9;

coherence

max (N,M) is ext-natural by XXREAL_0:def 10;

coherence

N + M is ext-natural

proof end;

coherence N * M is ext-natural

proof end;

registration

let M be ExtNat;

let N be non zero ExtNat;

coherence

not M + N is zero ;

coherence

not N + M is zero ;

end;
let N be non zero ExtNat;

coherence

not M + N is zero ;

coherence

not N + M is zero ;

definition

let X be set ;

end;
attr X is ext-natural-membered means :Def2: :: COUNTERS:def 3

for x being object st x in X holds

x is ext-natural ;

for x being object st x in X holds

x is ext-natural ;

:: deftheorem Def2 defines ext-natural-membered COUNTERS:def 3 :

for X being set holds

( X is ext-natural-membered iff for x being object st x in X holds

x is ext-natural );

for X being set holds

( X is ext-natural-membered iff for x being object st x in X holds

x is ext-natural );

registration

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is ext-natural-membered
;

coherence

for b_{1} being set st b_{1} is natural-membered holds

b_{1} is ext-natural-membered
;

coherence

for b_{1} being set st b_{1} is ext-natural-membered holds

b_{1} is ext-real-membered

ExtNAT is ext-natural-membered ;

end;
for b

b

coherence

for b

b

coherence

for b

b

proof end;

coherence ExtNAT is ext-natural-membered ;

registration
end;

registration

let X be ext-natural-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is ext-natural

end;
coherence

for b

proof end;

theorem :: COUNTERS:26

registration

let X be ext-natural-membered set ;

coherence

for b_{1} being Subset of X holds b_{1} is ext-natural-membered
;

end;
coherence

for b

registration

let N be ExtNat;

coherence

{N} is ext-natural-membered by TARSKI:def 1;

let M be ExtNat;

coherence

{N,M} is ext-natural-membered

coherence

{N,M,K} is ext-natural-membered

end;
coherence

{N} is ext-natural-membered by TARSKI:def 1;

let M be ExtNat;

coherence

{N,M} is ext-natural-membered

proof end;

let K be ExtNat;coherence

{N,M,K} is ext-natural-membered

proof end;

registration
end;

registration

let X be ext-natural-membered set ;

let Y be set ;

coherence

X /\ Y is ext-natural-membered

X \ Y is ext-natural-membered ;

end;
let Y be set ;

coherence

X /\ Y is ext-natural-membered

proof end;

coherence X \ Y is ext-natural-membered ;

registration
end;

definition

let X be ext-natural-membered set ;

let Y be set ;

compatibility

( X c= Y iff for N being ExtNat st N in X holds

N in Y )

end;
let Y be set ;

compatibility

( X c= Y iff for N being ExtNat st N in X holds

N in Y )

proof end;

:: deftheorem defines c= COUNTERS:def 4 :

for X being ext-natural-membered set

for Y being set holds

( X c= Y iff for N being ExtNat st N in X holds

N in Y );

for X being ext-natural-membered set

for Y being set holds

( X c= Y iff for N being ExtNat st N in X holds

N in Y );

definition

let X, Y be ext-natural-membered set ;

compatibility

( X = Y iff for N being ExtNat holds

( N in X iff N in Y ) )

end;
compatibility

( X = Y iff for N being ExtNat holds

( N in X iff N in Y ) )

proof end;

:: deftheorem defines = COUNTERS:def 5 :

for X, Y being ext-natural-membered set holds

( X = Y iff for N being ExtNat holds

( N in X iff N in Y ) );

for X, Y being ext-natural-membered set holds

( X = Y iff for N being ExtNat holds

( N in X iff N in Y ) );

definition

let X, Y be ext-natural-membered set ;

( X misses Y iff for N being ExtNat holds

( not N in X or not N in Y ) )

end;
redefine pred X misses Y means :: COUNTERS:def 6

for N being ExtNat holds

( not N in X or not N in Y );

compatibility for N being ExtNat holds

( not N in X or not N in Y );

( X misses Y iff for N being ExtNat holds

( not N in X or not N in Y ) )

proof end;

:: deftheorem defines misses COUNTERS:def 6 :

for X, Y being ext-natural-membered set holds

( X misses Y iff for N being ExtNat holds

( not N in X or not N in Y ) );

for X, Y being ext-natural-membered set holds

( X misses Y iff for N being ExtNat holds

( not N in X or not N in Y ) );

theorem :: COUNTERS:27

for F being set st ( for X being set st X in F holds

X is ext-natural-membered ) holds

union F is ext-natural-membered

X is ext-natural-membered ) holds

union F is ext-natural-membered

proof end;

definition

let X be ext-natural-membered set ;

for b_{1} being object holds

( b_{1} is UpperBound of X iff for N being ExtNat st N in X holds

N <= b_{1} )

for b_{1} being object holds

( b_{1} is LowerBound of X iff for N being ExtNat st N in X holds

b_{1} <= N )

end;
redefine mode UpperBound of X means :DefU: :: COUNTERS:def 7

for N being ExtNat st N in X holds

N <= it;

compatibility for N being ExtNat st N in X holds

N <= it;

for b

( b

N <= b

proof end;

redefine mode LowerBound of X means :DefL: :: COUNTERS:def 8

for N being ExtNat st N in X holds

it <= N;

compatibility for N being ExtNat st N in X holds

it <= N;

for b

( b

b

proof end;

:: deftheorem DefU defines UpperBound COUNTERS:def 7 :

for X being ext-natural-membered set

for b_{2} being object holds

( b_{2} is UpperBound of X iff for N being ExtNat st N in X holds

N <= b_{2} );

for X being ext-natural-membered set

for b

( b

N <= b

:: deftheorem DefL defines LowerBound COUNTERS:def 8 :

for X being ext-natural-membered set

for b_{2} being object holds

( b_{2} is LowerBound of X iff for N being ExtNat st N in X holds

b_{2} <= N );

for X being ext-natural-membered set

for b

( b

b

registration

coherence

for b_{1} being ext-natural-membered set holds b_{1} is bounded_below

for b_{1} being ext-natural-membered set st not b_{1} is empty holds

b_{1} is left_end

end;
for b

proof end;

coherence for b

b

proof end;

registration

let X be ext-natural-membered set ;

existence

ex b_{1} being UpperBound of X st b_{1} is ext-natural

ex b_{1} being LowerBound of X st b_{1} is ext-natural

inf X is ext-natural

end;
existence

ex b

proof end;

existence ex b

proof end;

coherence inf X is ext-natural

proof end;

registration
end;

registration

coherence

for b_{1} being ext-natural-membered set st not b_{1} is empty & b_{1} is bounded_above holds

b_{1} is right_end

end;
for b

b

proof end;

definition

let X be left_end ext-natural-membered set ;

inf X is ExtNat ;

compatibility

for b_{1} being ExtNat holds

( b_{1} = inf X iff ( b_{1} in X & ( for N being ExtNat st N in X holds

b_{1} <= N ) ) )

end;
:: original: inf

redefine func min X -> ExtNat means :: COUNTERS:def 9

( it in X & ( for N being ExtNat st N in X holds

it <= N ) );

coherence redefine func min X -> ExtNat means :: COUNTERS:def 9

( it in X & ( for N being ExtNat st N in X holds

it <= N ) );

inf X is ExtNat ;

compatibility

for b

( b

b

proof end;

:: deftheorem defines min COUNTERS:def 9 :

for X being left_end ext-natural-membered set

for b_{2} being ExtNat holds

( b_{2} = min X iff ( b_{2} in X & ( for N being ExtNat st N in X holds

b_{2} <= N ) ) );

for X being left_end ext-natural-membered set

for b

( b

b

definition

let X be right_end ext-natural-membered set ;

sup X is ExtNat ;

compatibility

for b_{1} being ExtNat holds

( b_{1} = sup X iff ( b_{1} in X & ( for N being ExtNat st N in X holds

N <= b_{1} ) ) )

end;
:: original: sup

redefine func max X -> ExtNat means :: COUNTERS:def 10

( it in X & ( for N being ExtNat st N in X holds

N <= it ) );

coherence redefine func max X -> ExtNat means :: COUNTERS:def 10

( it in X & ( for N being ExtNat st N in X holds

N <= it ) );

sup X is ExtNat ;

compatibility

for b

( b

N <= b

proof end;

:: deftheorem defines max COUNTERS:def 10 :

for X being right_end ext-natural-membered set

for b_{2} being ExtNat holds

( b_{2} = max X iff ( b_{2} in X & ( for N being ExtNat st N in X holds

N <= b_{2} ) ) );

for X being right_end ext-natural-membered set

for b

( b

N <= b

definition
end;

:: deftheorem defines ext-natural-valued COUNTERS:def 11 :

for R being Relation holds

( R is ext-natural-valued iff rng R c= ExtNAT );

for R being Relation holds

( R is ext-natural-valued iff rng R c= ExtNAT );

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is ext-natural-valued

for b_{1} being Relation st b_{1} is natural-valued holds

b_{1} is ext-natural-valued

for b_{1} being Relation st b_{1} is ext-natural-valued holds

( b_{1} is ExtNAT -valued & b_{1} is ext-real-valued )
by RELAT_1:def 19, XBOOLE_1:1, VALUED_0:def 2;

coherence

for b_{1} being Relation st b_{1} is ExtNAT -valued holds

b_{1} is ext-natural-valued
by RELAT_1:def 19;

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

( b

coherence

for b

b

theorem :: COUNTERS:29

for R being Relation

for S being ext-natural-valued Relation st R c= S holds

R is ext-natural-valued ;

for S being ext-natural-valued Relation st R c= S holds

R is ext-natural-valued ;

registration

let R be ext-natural-valued Relation;

coherence

for b_{1} being Subset of R holds b_{1} is ext-natural-valued
;

end;
coherence

for b

registration

let R be ext-natural-valued Relation;

let S be Relation;

coherence

R /\ S is ext-natural-valued ;

coherence

R \ S is ext-natural-valued ;

coherence

S * R is ext-natural-valued ;

end;
let S be Relation;

coherence

R /\ S is ext-natural-valued ;

coherence

R \ S is ext-natural-valued ;

coherence

S * R is ext-natural-valued ;

registration
end;

registration

let R be ext-natural-valued Relation;

let X be set ;

coherence

R .: X is ext-natural-membered

R | X is ext-natural-valued ;

coherence

X |` R is ext-natural-valued ;

end;
let X be set ;

coherence

R .: X is ext-natural-membered

proof end;

coherence R | X is ext-natural-valued ;

coherence

X |` R is ext-natural-valued ;

registration

let R be ext-natural-valued Relation;

let x be object ;

coherence

Im (R,x) is ext-natural-membered

end;
let x be object ;

coherence

Im (R,x) is ext-natural-membered

proof end;

registration
end;

definition

let f be Function;

( f is ext-natural-valued iff for x being object st x in dom f holds

f . x is ext-natural )

end;
redefine attr f is ext-natural-valued means :: COUNTERS:def 12

for x being object st x in dom f holds

f . x is ext-natural ;

compatibility for x being object st x in dom f holds

f . x is ext-natural ;

( f is ext-natural-valued iff for x being object st x in dom f holds

f . x is ext-natural )

proof end;

:: deftheorem defines ext-natural-valued COUNTERS:def 12 :

for f being Function holds

( f is ext-natural-valued iff for x being object st x in dom f holds

f . x is ext-natural );

for f being Function holds

( f is ext-natural-valued iff for x being object st x in dom f holds

f . x is ext-natural );

theorem ThFunc1: :: COUNTERS:30

for f being Function holds

( f is ext-natural-valued iff for x being object holds f . x is ext-natural )

( f is ext-natural-valued iff for x being object holds f . x is ext-natural )

proof end;

registration
end;

registration
end;

registration
end;

registration

let Z be set ;

let X be ext-natural-membered set ;

coherence

for b_{1} being Relation of Z,X holds b_{1} is ext-natural-valued

end;
let X be ext-natural-membered set ;

coherence

for b

proof end;

registration

let Z be set ;

let X be ext-natural-membered set ;

coherence

for b_{1} being Relation of Z,X st b_{1} = [:Z,X:] holds

b_{1} is ext-natural-valued
;

end;
let X be ext-natural-membered set ;

coherence

for b

b

registration

existence

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is constant & b_{1} is ext-natural-valued )

end;
ex b

( not b

proof end;

theorem :: COUNTERS:31

for f being constant non empty ext-natural-valued Function ex N being ExtNat st

for x being object st x in dom f holds

f . x = N

for x being object st x in dom f holds

f . x = N

proof end;

:: into ORDINAL1 ?

theorem Th2: :: COUNTERS:32

for f being Function holds

( f is Ordinal-yielding iff for x being object st x in dom f holds

f . x is Ordinal )

( f is Ordinal-yielding iff for x being object st x in dom f holds

f . x is Ordinal )

proof end;

:: into ORDINAL1 ?

registration
end;

:: into ORDINAL1 ? ::: generalize in ORDINAL2

registration
end;

:: into ORDINAL4 ?

:: into CARD_1 ? ::: version of CARD_1:64

:: generalization of CARD_1:64

:: into CARD_1 ?

:: into CARD_1 ?

:: into CARD_1 ?

registration
end;

:: into CARD_2 ?

registration
end;

:: into CARD_2 ?

:: into CARD_2 ?

:: into CARD_3 ?

registration

let f be Cardinal-yielding Function;

let g be Function;

coherence

f * g is Cardinal-yielding

end;
let g be Function;

coherence

f * g is Cardinal-yielding

proof end;

:: into CARD_3 ?

registration

coherence

for b_{1} being Function st b_{1} is natural-valued holds

b_{1} is Cardinal-yielding

end;
for b

b

proof end;

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

registration

coherence

for b_{1} being Function st b_{1} is Cardinal-yielding holds

b_{1} is Ordinal-yielding

end;
for b

b

proof end;

:: into CARD_3 ?

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

:: into CARD_3 ?

registration
end;

:: into CARD_3 ?

:: into CARD_3 ?

registration
end;

:: into CARD_3 or AFINSQ_1 ?

registration

let c1 be Cardinal;

coherence

<%c1%> is Cardinal-yielding

coherence

<%c1,c2%> is Cardinal-yielding

coherence

<%c1,c2,c3%> is Cardinal-yielding

end;
coherence

<%c1%> is Cardinal-yielding

proof end;

let c2 be Cardinal;coherence

<%c1,c2%> is Cardinal-yielding

proof end;

let c3 be Cardinal;coherence

<%c1,c2,c3%> is Cardinal-yielding

proof end;

:: into CARD_3 or AFINSQ_1 ?

:: into AFINSQ_1 ?

registration

let A be infinite Ordinal;

coherence

not <%A%> is natural-valued

coherence

not <%A,x%> is natural-valued

not <%x,A%> is natural-valued

coherence

not <%A,x,y%> is natural-valued

not <%x,A,y%> is natural-valued

not <%x,y,A%> is natural-valued

end;
coherence

not <%A%> is natural-valued

proof end;

let x be object ;coherence

not <%A,x%> is natural-valued

proof end;

coherence not <%x,A%> is natural-valued

proof end;

let y be object ;coherence

not <%A,x,y%> is natural-valued

proof end;

coherence not <%x,A,y%> is natural-valued

proof end;

coherence not <%x,y,A%> is natural-valued

proof end;

:: into AFINSQ_1 ?

registration

ex b_{1} being XFinSequence st

( not b_{1} is empty & b_{1} is non-empty & b_{1} is natural-valued )

coherence

<%x%> is one-to-one
end;

cluster Relation-like non-empty omega -defined Sequence-like Function-like non empty finite natural-valued countable V182() for set ;

existence ex b

( not b

proof end;

let x be object ;coherence

<%x%> is one-to-one

proof end;

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

registration

let x be object ;

coherence

<%x%> is trivial ;

let y be object ;

coherence

not <%x,y%> is trivial

coherence

not <%x,y,z%> is trivial

end;
coherence

<%x%> is trivial ;

let y be object ;

coherence

not <%x,y%> is trivial

proof end;

let z be object ;coherence

not <%x,y,z%> is trivial

proof end;

:: into AFINSQ_1 ?

registration

ex b_{1} being XFinSequence st

( not b_{1} is empty & b_{1} is trivial )

ex b_{1} being XFinSequence of D st

( not b_{1} is empty & b_{1} is trivial )
end;

cluster Relation-like omega -defined Sequence-like Function-like non empty trivial finite countable V182() for set ;

existence ex b

( not b

proof end;

let D be non empty set ;
cluster Relation-like omega -defined D -valued Sequence-like Function-like non empty trivial finite countable V182() for set ;

existence ex b

( not b

proof end;

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

theorem :: COUNTERS:42

for D being non empty set

for p being non empty trivial Sequence of D ex x being Element of D st p = <%x%>

for p being non empty trivial Sequence of D ex x being Element of D st p = <%x%>

proof end;

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: into AFINSQ_1 ?

:: deftheorem Def1 defines with_cardinal_domain COUNTERS:def 13 :

for R being Relation holds

( R is with_cardinal_domain iff ex c being Cardinal st dom R = c );

for R being Relation holds

( R is with_cardinal_domain iff ex c being Cardinal st dom R = c );

registration

coherence

for b_{1} being Relation st b_{1} is empty holds

b_{1} is with_cardinal_domain
;

coherence

for b_{1} being Relation st b_{1} is finite & b_{1} is Sequence-like holds

b_{1} is with_cardinal_domain

for b_{1} being Relation st b_{1} is with_cardinal_domain holds

b_{1} is Sequence-like
by ORDINAL1:def 7;

let c be Cardinal;

coherence

for b_{1} being ManySortedSet of c holds b_{1} is with_cardinal_domain
by PARTFUN1:def 2;

let x be object ;

coherence

c --> x is with_cardinal_domain ;

end;
for b

b

coherence

for b

b

proof end;

coherence for b

b

let c be Cardinal;

coherence

for b

let x be object ;

coherence

c --> x is with_cardinal_domain ;

registration

let X be set ;

for b_{1} being Denumeration of X holds b_{1} is with_cardinal_domain

end;
cluster Function-like one-to-one quasi_total onto -> with_cardinal_domain for Element of bool [:(card X),X:];

coherence for b

proof end;

registration
end;

registration

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is trivial & b_{1} is non-empty & b_{1} is with_cardinal_domain & b_{1} is Cardinal-yielding )

ex b_{1} being Function st

( not b_{1} is empty & not b_{1} is trivial & b_{1} is non-empty & b_{1} is finite & b_{1} is with_cardinal_domain & b_{1} is Cardinal-yielding )

ex b_{1} being Function st

( not b_{1} is empty & b_{1} is non-empty & b_{1} is infinite & b_{1} is with_cardinal_domain & b_{1} is natural-valued )

ex b_{1} being Function st

( not b_{1} is trivial & b_{1} is non-empty & b_{1} is with_cardinal_domain & b_{1} is Cardinal-yielding & not b_{1} is natural-valued )
end;

cluster Relation-like non-empty Function-like non empty trivial Cardinal-yielding with_cardinal_domain for set ;

existence ex b

( not b

proof end;

cluster Relation-like non-empty Function-like non empty non trivial finite Cardinal-yielding with_cardinal_domain for set ;

existence ex b

( not b

proof end;

cluster Relation-like non-empty Function-like non empty infinite natural-valued with_cardinal_domain for set ;

existence ex b

( not b

proof end;

cluster Relation-like non-empty Function-like non trivial non natural-valued Cardinal-yielding with_cardinal_domain for set ;

existence ex b

( not b

proof end;

registration
end;

registration

let R be with_cardinal_domain Relation;

let P be rng R -defined total Relation;

coherence

R * P is with_cardinal_domain

end;
let P be rng R -defined total Relation;

coherence

R * P is with_cardinal_domain

proof end;

registration

let g be Function;

let f be Denumeration of (dom g);

coherence

g * f is with_cardinal_domain

end;
let f be Denumeration of (dom g);

coherence

g * f is with_cardinal_domain

proof end;

registration

let f be with_cardinal_domain Function;

let p be Permutation of (dom f);

coherence

f * p is with_cardinal_domain

end;
let p be Permutation of (dom f);

coherence

f * p is with_cardinal_domain

proof end;

registration

let p be XFinSequence;

let B be with_cardinal_domain Sequence;

coherence

p ^ B is with_cardinal_domain

end;
let B be with_cardinal_domain Sequence;

coherence

p ^ B is with_cardinal_domain

proof end;

definition
end;