:: Extended Natural Numbers and Counters
:: by Sebastian Koch
::
:: Received October 25, 2020
:: Copyright (c) 2020-2025 Association of Mizar Users

definition

func ExtNAT -> Subset of ExtREAL equals :: COUNTERS:def 1
NAT \/ {+infty};

coherence
NAT \/ {+infty} is Subset of ExtREAL

proof end;

end;

:: deftheorem defines ExtNAT COUNTERS:def 1 :
ExtNAT = NAT \/ {+infty};

theorem Th1: :: COUNTERS:1

( NAT c< ExtNAT & ExtNAT c< ExtREAL )

proof end;

registration

cluster ExtNAT -> non empty infinite ;

coherence
( not ExtNAT is empty & not ExtNAT is finite ) by Th1, FINSET_1:1, XBOOLE_0:def 8;

end;

definition

let x be object ;

attr x is ext-natural means :Def1: :: COUNTERS:def 2
x in ExtNAT ;

end;

:: deftheorem Def1 defines ext-natural COUNTERS:def 2 :
for x being object holds
( x is ext-natural iff x in ExtNAT );

registration

cluster +infty -> non natural ext-natural ;

coherence
( +infty is ext-natural & not +infty is natural ) by ZFMISC_1:136;

cluster ext-natural -> ext-real for object ;

coherence
for b₁ being object st b₁ is ext-natural holds
b₁ is ext-real ;

cluster natural -> ext-natural for object ;

coherence
for b₁ being object st b₁ is natural holds
b₁ is ext-natural

proof end;

cluster finite ext-natural -> natural for set ;

coherence
for b₁ being set st b₁ is finite & b₁ is ext-natural holds
b₁ is natural

proof end;

end;

registration

cluster zero ext-natural for object ;

existence
ex b₁ being object st
( b₁ is zero & b₁ is ext-natural )

proof end;

cluster non zero ext-natural for object ;

existence
ex b₁ being object st
( not b₁ is zero & b₁ is ext-natural )

proof end;

cluster ext-natural for set ;

existence
ex b₁ being number st b₁ is ext-natural

proof end;

cluster -> ext-natural for Element of ExtNAT ;

coherence
for b₁ being Element of ExtNAT holds b₁ is ext-natural ;

end;

definition

mode ExtNat is ext-natural ExtReal;

end;

registration

cluster non natural ext-real ext-natural -> non zero for object ;

coherence
for b₁ being ExtNat st not b₁ is natural holds
not b₁ is zero ;

end;

registration

cluster non natural ext-real ext-natural for object ;

correctness
existence
not for b₁ being ExtNat holds b₁ is natural ;

proof end;

end;

registration

let x be ExtNat;

reduce In (x,ExtNAT) to x;

reducibility
In (x,ExtNAT) = x by Def1, SUBSET_1:def 8;

end;

registration

ExtNat ex b₁ being set st
for b₂ being ExtNat holds b₂ in b₁

proof end;

end;

theorem Th3: :: COUNTERS:2

for x being object holds
( x is ExtNat iff ( x is Nat or x = +infty ) )

proof end;

registration

cluster zero -> ext-natural for object ;

coherence
for b₁ being object st b₁ is zero holds
b₁ is ext-natural ;

cluster ext-real ext-natural -> non negative for object ;

coherence
for b₁ being ExtReal st b₁ is ext-natural holds
not b₁ is negative by Th3;

end;

registration

cluster ext-real ext-natural -> non negative for object ;

coherence
for b₁ being ExtNat holds not b₁ is negative ;

cluster non zero ext-real ext-natural -> positive for object ;

coherence
for b₁ being ExtNat st not b₁ is zero holds
b₁ is positive ;

end;

registration

let N, M be ExtNat;

cluster min (N,M) -> ext-natural ;

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

cluster max (N,M) -> ext-natural ;

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

cluster N + M -> ext-natural ;

coherence
N + M is ext-natural

proof end;

cluster N * M -> ext-natural ;

coherence
N * M is ext-natural

proof end;

end;

theorem :: COUNTERS:3

for N being ExtNat holds 0 <= N ;

theorem :: COUNTERS:4

for N being ExtNat st 0 <> N holds
0 < N ;

theorem :: COUNTERS:5

for N being ExtNat holds 0 < N + 1 ;

theorem Th5: :: COUNTERS:6

for N, M being ExtNat st M in NAT & N <= M holds
N in NAT

proof end;

theorem :: COUNTERS:7

for N, M being ExtNat st N < M holds
N in NAT

proof end;

theorem :: COUNTERS:8

for N, M, K being ExtNat st N <= M holds
N * K <= M * K by XXREAL_3:71;

theorem :: COUNTERS:9

for N being ExtNat holds
( N = 0 or ex K being ExtNat st N = K + 1 )

proof end;

theorem :: COUNTERS:10

for N, M being ExtNat st N + M = 0 holds
( N = 0 & M = 0 ) ;

registration

let M be ExtNat;
let N be non zero ExtNat;

cluster M + N -> non zero ;

coherence
not M + N is zero ;

cluster N + M -> non zero ;

coherence
not N + M is zero ;

end;

theorem Th10: :: COUNTERS:11

for N, M being ExtNat holds
( not N <= M + 1 or N <= M or N = M + 1 )

proof end;

theorem :: COUNTERS:12

for N, M being ExtNat st N <= M & M <= N + 1 & not N = M holds
M = N + 1

proof end;

theorem :: COUNTERS:13

for N, M being ExtNat st N <= M holds
ex K being ExtNat st M = N + K

proof end;

theorem :: COUNTERS:14

for N, M being ExtNat holds N <= N + M

proof end;

theorem :: COUNTERS:15

for N, M, K being ExtNat st N <= M holds
N <= M + K

proof end;

theorem Th4c: :: COUNTERS:16

for N being ExtNat st N < 1 holds
N = 0

proof end;

theorem :: COUNTERS:17

for N, M being ExtNat st N * M = 1 holds
N = 1

proof end;

theorem :: COUNTERS:18

for N, K being ExtNat holds
( K < K + N iff ( 1 <= N & K <> +infty ) )

proof end;

theorem :: COUNTERS:19

for N, M, K being ExtNat st K <> 0 & N = M * K holds
M <= N

proof end;

theorem :: COUNTERS:20

for N, M, K being ExtNat st M <= N holds
M * K <= N * K by XXREAL_3:71;

theorem :: COUNTERS:21

for N, M, K being ExtNat holds (K + M) + N = K + (M + N) by XXREAL_3:29;

theorem :: COUNTERS:22

for N, M, K being ExtNat holds K * (N + M) = (K * N) + (K * M)

proof end;

definition

let X be set ;

attr X is ext-natural-membered means :Def2: :: COUNTERS:def 3
for x being object st x in X holds
x is ext-natural ;

end;

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

registration

cluster empty -> ext-natural-membered for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is ext-natural-membered ;

cluster natural-membered -> ext-natural-membered for set ;

coherence
for b₁ being set st b₁ is natural-membered holds
b₁ is ext-natural-membered ;

cluster ext-natural-membered -> ext-real-membered for set ;

coherence
for b₁ being set st b₁ is ext-natural-membered holds
b₁ is ext-real-membered

proof end;

cluster ExtNAT -> ext-natural-membered ;

coherence
ExtNAT is ext-natural-membered ;

end;

registration

cluster non empty ext-natural-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is ext-natural-membered )

proof end;

end;

theorem ThSubset: :: COUNTERS:23

for X being set holds
( X is ext-natural-membered iff X c= ExtNAT )

proof end;

registration

let X be ext-natural-membered set ;

cluster -> ext-natural for Element of X;

coherence
for b₁ being Element of X holds b₁ is ext-natural

proof end;

end;

theorem ThEx: :: COUNTERS:24

for X being non empty ext-natural-membered set ex N being ExtNat st N in X

proof end;

theorem :: COUNTERS:25

for X being ext-natural-membered set st ( for N being ExtNat holds N in X ) holds
X = ExtNAT

proof end;

theorem :: COUNTERS:26

for X being ext-natural-membered set
for Y being set st Y c= X holds
Y is ext-natural-membered ;

registration

let X be ext-natural-membered set ;

cluster -> ext-natural-membered for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is ext-natural-membered ;

end;

registration

let N be ExtNat;

cluster {N} -> ext-natural-membered ;

coherence
{N} is ext-natural-membered by TARSKI:def 1;
let M be ExtNat;

cluster {N,M} -> ext-natural-membered ;

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

proof end;

let K be ExtNat;

cluster {N,M,K} -> ext-natural-membered ;

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

proof end;

end;

registration

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

cluster X \/ Y -> ext-natural-membered ;

coherence
X \/ Y is ext-natural-membered

proof end;

end;

registration

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

cluster X /\ Y -> ext-natural-membered ;

coherence
X /\ Y is ext-natural-membered

proof end;

cluster X \ Y -> ext-natural-membered ;

coherence
X \ Y is ext-natural-membered ;

end;

registration

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

cluster X \+\ Y -> ext-natural-membered ;

coherence
X \+\ Y is ext-natural-membered

proof end;

end;

definition

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

redefine pred X c= Y means :: COUNTERS:def 4
for N being ExtNat st N in X holds
N in Y;

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

proof end;

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

definition

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

redefine pred X = Y means :: COUNTERS:def 5
for N being ExtNat holds
( N in X iff N in Y );

compatibility
( X = Y iff for N being ExtNat holds
( N in X iff N in Y ) )

proof end;

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

definition

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

redefine pred X misses Y means :: COUNTERS:def 6
for N being ExtNat holds
( not N in X or not N in Y );

compatibility
( X misses Y iff for N being ExtNat holds
( not N in X or not N in Y ) )

proof end;

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

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

proof end;

theorem :: COUNTERS:28

for F, X being set st X in F & X is ext-natural-membered holds
meet F is ext-natural-membered

proof end;

scheme :: COUNTERS:sch 1
ENMSeparation{ P₁[ object ] } :

ex X being ext-natural-membered set st
for N being ExtNat holds
( N in X iff P₁[N] )

proof end;

definition

let X be ext-natural-membered set ;

redefine mode UpperBound of X means :DefU: :: COUNTERS:def 7
for N being ExtNat st N in X holds
N <= it;

compatibility
for b₁ being object holds
( b₁ is UpperBound of X iff for N being ExtNat st N in X holds
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 b₁ being object holds
( b₁ is LowerBound of X iff for N being ExtNat st N in X holds
b₁ <= N )

proof end;

end;

:: deftheorem DefU defines UpperBound COUNTERS:def 7 :
for X being ext-natural-membered set
for b₂ being object holds
( b₂ is UpperBound of X iff for N being ExtNat st N in X holds
N <= b₂ );

:: deftheorem DefL defines LowerBound COUNTERS:def 8 :
for X being ext-natural-membered set
for b₂ being object holds
( b₂ is LowerBound of X iff for N being ExtNat st N in X holds
b₂ <= N );

registration

cluster ext-natural-membered -> bounded_below ext-natural-membered for set ;

coherence
for b₁ being ext-natural-membered set holds b₁ is bounded_below

proof end;

cluster non empty ext-natural-membered -> left_end ext-natural-membered for set ;

coherence
for b₁ being ext-natural-membered set st not b₁ is empty holds
b₁ is left_end

proof end;

end;

registration

let X be ext-natural-membered set ;

cluster ext-real ext-natural for UpperBound of X;

existence
ex b₁ being UpperBound of X st b₁ is ext-natural

proof end;

cluster ext-real ext-natural for LowerBound of X;

existence
ex b₁ being LowerBound of X st b₁ is ext-natural

proof end;

cluster inf X -> ext-natural ;

coherence
inf X is ext-natural

proof end;

end;

registration

let X be non empty ext-natural-membered set ;

cluster sup X -> ext-natural ;

coherence
sup X is ext-natural

proof end;

end;

registration

cluster non empty bounded_above ext-natural-membered -> right_end ext-natural-membered for set ;

coherence
for b₁ being ext-natural-membered set st not b₁ is empty & b₁ is bounded_above holds
b₁ is right_end

proof end;

end;

definition

let X be left_end ext-natural-membered set ;

:: 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
inf X is ExtNat ;
compatibility
for b₁ being ExtNat holds
( b₁ = inf X iff ( b₁ in X & ( for N being ExtNat st N in X holds
b₁ <= N ) ) )

proof end;

end;

:: deftheorem defines min COUNTERS:def 9 :
for X being left_end ext-natural-membered set
for b₂ being ExtNat holds
( b₂ = min X iff ( b₂ in X & ( for N being ExtNat st N in X holds
b₂ <= N ) ) );

definition

let X be right_end ext-natural-membered set ;

:: 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
sup X is ExtNat ;
compatibility
for b₁ being ExtNat holds
( b₁ = sup X iff ( b₁ in X & ( for N being ExtNat st N in X holds
N <= b₁ ) ) )

proof end;

end;

:: deftheorem defines max COUNTERS:def 10 :
for X being right_end ext-natural-membered set
for b₂ being ExtNat holds
( b₂ = max X iff ( b₂ in X & ( for N being ExtNat st N in X holds
N <= b₂ ) ) );

definition

let R be Relation;

attr R is ext-natural-valued means :: COUNTERS:def 11
rng R c= ExtNAT ;

end;

:: deftheorem defines ext-natural-valued COUNTERS:def 11 :
for R being Relation holds
( R is ext-natural-valued iff rng R c= ExtNAT );

registration

cluster Relation-like empty -> ext-natural-valued for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is ext-natural-valued

proof end;

cluster Relation-like natural-valued -> ext-natural-valued for set ;

coherence
for b₁ being Relation st b₁ is natural-valued holds
b₁ is ext-natural-valued

proof end;

cluster Relation-like ext-natural-valued -> ExtNAT -valued ext-real-valued for set ;

coherence
for b₁ being Relation st b₁ is ext-natural-valued holds
( b₁ is ExtNAT -valued & b₁ is ext-real-valued ) by RELAT_1:def 19, XBOOLE_1:1, VALUED_0:def 2;

cluster Relation-like ExtNAT -valued -> ext-natural-valued for set ;

coherence
for b₁ being Relation st b₁ is ExtNAT -valued holds
b₁ is ext-natural-valued by RELAT_1:def 19;

end;

registration

cluster Relation-like Function-like ext-natural-valued for set ;

existence
ex b₁ being Function st b₁ is ext-natural-valued

proof end;

end;

registration

let R be ext-natural-valued Relation;

cluster rng R -> ext-natural-membered ;

coherence
rng R is ext-natural-membered ;

end;

theorem :: COUNTERS:29

for R being Relation
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;

cluster -> ext-natural-valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is ext-natural-valued ;

end;

registration

let R, S be ext-natural-valued Relation;

cluster R \/ S -> ext-natural-valued ;

coherence
R \/ S is ext-natural-valued ;

end;

registration

let R be ext-natural-valued Relation;
let S be Relation;

cluster R /\ S -> ext-natural-valued ;

coherence
R /\ S is ext-natural-valued ;

cluster R \ S -> ext-natural-valued ;

coherence
R \ S is ext-natural-valued ;

cluster S * R -> ext-natural-valued ;

coherence
S * R is ext-natural-valued ;

end;

registration

let R, S be ext-natural-valued Relation;

cluster R \+\ S -> ext-natural-valued ;

coherence
R \+\ S is ext-natural-valued

proof end;

end;

registration

let R be ext-natural-valued Relation;
let X be set ;

cluster R .: X -> ext-natural-membered ;

coherence
R .: X is ext-natural-membered

proof end;

cluster R | X -> ext-natural-valued ;

coherence
R | X is ext-natural-valued ;

cluster X |` R -> ext-natural-valued ;

coherence
X |` R is ext-natural-valued ;

end;

registration

let R be ext-natural-valued Relation;
let x be object ;

cluster Im (R,x) -> ext-natural-membered ;

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

proof end;

end;

registration

let X be ext-natural-membered set ;

cluster id X -> ext-natural-valued ;

coherence
id X is ext-natural-valued by ThSubset;

end;

definition

let f be Function;

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
( f is ext-natural-valued iff for x being object st x in dom f holds
f . x is ext-natural )

proof end;

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

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 )

proof end;

registration

let f be ext-natural-valued Function;
let x be object ;

cluster f . x -> ext-natural ;

coherence
f . x is ext-natural by ThFunc1;

end;

registration

let X be set ;
let N be ExtNat;

cluster X --> N -> ext-natural-valued ;

coherence
X --> N is ext-natural-valued

proof end;

end;

registration

let f, g be ext-natural-valued Function;

cluster f +* g -> ext-natural-valued ;

coherence
f +* g is ext-natural-valued

proof end;

end;

registration

let x be object ;
let N be ExtNat;

cluster x .--> N -> ext-natural-valued ;

coherence
x .--> N is ext-natural-valued

proof end;

end;

registration

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

cluster -> ext-natural-valued for Element of bool [:Z,X:];

coherence
for b₁ being Relation of Z,X holds b₁ is ext-natural-valued

proof end;

end;

registration

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

cluster [:Z,X:] -> ext-natural-valued for Relation of Z,X;

coherence
for b₁ being Relation of Z,X st b₁ = [:Z,X:] holds
b₁ is ext-natural-valued ;

end;

registration

cluster Relation-like Function-like constant non empty ext-natural-valued for set ;

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is constant & b₁ is ext-natural-valued )

proof end;

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

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 )

proof end;

:: into ORDINAL1 ?

registration

cluster ordinal -> c=-linear for set ;

coherence
for b₁ being set st b₁ is ordinal holds
b₁ is c=-linear

proof end;

end;

:: into ORDINAL1 ? ::: generalize in ORDINAL2

registration

let f be Ordinal-yielding Function;
let x be object ;

cluster f . x -> ordinal ;

coherence
f . x is ordinal

proof end;

end;

:: into ORDINAL4 ?

registration

let A, B be non-empty Sequence;

cluster A ^ B -> non-empty ;

coherence
A ^ B is non-empty

proof end;

end;

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

theorem Th3: :: COUNTERS:33

for X being set
for x being object holds card (X --> x) = card X

proof end;

:: generalization of CARD_1:64
:: into CARD_1 ?

theorem :: COUNTERS:34

for c being Cardinal
for x being object holds card (c --> x) = c

proof end;

:: into CARD_1 ?

registration

let X be trivial set ;

cluster card X -> trivial ;

coherence
card X is trivial

proof end;

end;

:: into CARD_2 ?

registration

let c1 be Cardinal;
let c2 be non empty Cardinal;

cluster c1 +` c2 -> non empty ;

coherence
not c1 +` c2 is empty

proof end;

end;

:: into CARD_2 ?

theorem :: COUNTERS:35

for A being Ordinal holds
( ( A <> 0 & A <> 1 ) iff not A is trivial )

proof end;

:: into CARD_2 ?

theorem ThAdd: :: COUNTERS:36

for A being Ordinal
for B being infinite Cardinal st A in B holds
A +^ B = B

proof end;

:: into CARD_3 ?

registration

let f be Cardinal-yielding Function;
let g be Function;

cluster g * f -> Cardinal-yielding ;

coherence
f * g is Cardinal-yielding

proof end;

end;

:: into CARD_3 ?

registration

cluster Relation-like Function-like natural-valued -> Cardinal-yielding for set ;

coherence
for b₁ being Function st b₁ is natural-valued holds
b₁ is Cardinal-yielding

proof end;

end;

:: into CARD_3 ?

registration

let f be empty Function;

cluster disjoin f -> empty ;

coherence
disjoin f is empty by CARD_3:3;

end;

:: into CARD_3 ?

registration

let f be empty-yielding Function;

cluster disjoin f -> empty-yielding ;

coherence
disjoin f is empty-yielding

proof end;

end;

:: into CARD_3 ?

registration

let f be non empty-yielding Function;

cluster disjoin f -> non empty-yielding ;

coherence
not disjoin f is empty-yielding

proof end;

end;

:: into CARD_3 ?

registration

let f be empty-yielding Function;

cluster Union f -> empty ;

coherence
Union f is empty

proof end;

end;

:: into CARD_3 ?

registration

cluster Relation-like Function-like Cardinal-yielding -> Ordinal-yielding for set ;

coherence
for b₁ being Function st b₁ is Cardinal-yielding holds
b₁ is Ordinal-yielding

proof end;

end;

:: into CARD_3 ?

theorem :: COUNTERS:37

for f being Function
for p being Permutation of (dom f) holds Card (f * p) = (Card f) * p

proof end;

:: into CARD_3 ?

registration

let A be Sequence;

cluster Card A -> Sequence-like ;

coherence
Card A is Sequence-like

proof end;

end;

:: into CARD_3 ?

theorem :: COUNTERS:38

for A, B being Sequence holds Card (A ^ B) = (Card A) ^ (Card B)

proof end;

:: into CARD_3 ?

registration

let f be trivial Function;

cluster Card f -> trivial ;

coherence
Card f is trivial

proof end;

end;

:: into CARD_3 ?

registration

let f be non trivial Function;

cluster Card f -> non trivial ;

coherence
not Card f is trivial

proof end;

end;

:: into CARD_3 ?

registration

let A, B be Cardinal-yielding Sequence;

cluster A ^ B -> Cardinal-yielding ;

coherence
A ^ B is Cardinal-yielding

proof end;

end;

:: into CARD_3 or AFINSQ_1 ?

registration

let c1 be Cardinal;

cluster <%c1%> -> Cardinal-yielding ;

coherence
<%c1%> is Cardinal-yielding

proof end;

let c2 be Cardinal;

cluster <%c1,c2%> -> Cardinal-yielding ;

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

proof end;

let c3 be Cardinal;

cluster <%c1,c2,c3%> -> Cardinal-yielding ;

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

proof end;

end;

:: into CARD_3 or AFINSQ_1 ?

registration

let X1, X2, X3 be non empty set ;

cluster <%X1,X2,X3%> -> non-empty ;

coherence
<%X1,X2,X3%> is non-empty

proof end;

end;

:: into AFINSQ_1 ?

registration

let A be infinite Ordinal;

cluster <%A%> -> non natural-valued ;

coherence
not <%A%> is natural-valued

proof end;

let x be object ;

cluster <%A,x%> -> non natural-valued ;

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

proof end;

cluster <%x,A%> -> non natural-valued ;

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

proof end;

let y be object ;

cluster <%A,x,y%> -> non natural-valued ;

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

proof end;

cluster <%x,A,y%> -> non natural-valued ;

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

proof end;

cluster <%x,y,A%> -> non natural-valued ;

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

proof end;

end;

:: into AFINSQ_1 ?

registration

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

existence
ex b₁ being XFinSequence st
( not b₁ is empty & b₁ is non-empty & b₁ is natural-valued )

proof end;

let x be object ;

cluster <%x%> -> one-to-one ;

coherence
<%x%> is one-to-one

proof end;

end;

theorem :: COUNTERS:39

canceled;

theorem :: COUNTERS:40

canceled;

Th7: for x, y being object holds
( dom <%x,y%> = {0,1} & rng <%x,y%> = {x,y} )
by AFINSQ_1:98;

Th8: for x, y, z being object holds
( dom <%x,y,z%> = {0,1,2} & rng <%x,y,z%> = {x,y,z} )
by AFINSQ_1:99;

:: into AFINSQ_1 ?

registration

let x be object ;

cluster <%x%> -> trivial ;

coherence
<%x%> is trivial ;
let y be object ;

cluster <%x,y%> -> non trivial ;

coherence
not <%x,y%> is trivial

proof end;

let z be object ;

cluster <%x,y,z%> -> non trivial ;

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

proof end;

end;

:: into AFINSQ_1 ?

registration

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

existence
ex b₁ being XFinSequence st
( not b₁ is empty & b₁ is trivial )

proof end;

let D be non empty set ;

cluster Relation-like omega -defined D -valued Sequence-like Function-like non empty trivial finite countable initial for set ;

existence
ex b₁ being XFinSequence of D st
( not b₁ is empty & b₁ is trivial )

proof end;

end;

:: into AFINSQ_1 ?

theorem Th9: :: COUNTERS:41

for p being non empty trivial Sequence ex x being object st p = <%x%>

proof end;

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

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:43

<%0%> = id 1

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:44

<%0,1%> = id 2

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:45

<%0,1,2%> = id 3

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:46

for x, y being object holds <%x,y%> * <%1,0%> = <%y,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:47

for x, y, z being object holds <%x,y,z%> * <%0,2,1%> = <%x,z,y%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:48

for x, y, z being object holds <%x,y,z%> * <%1,0,2%> = <%y,x,z%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:49

for x, y, z being object holds <%x,y,z%> * <%1,2,0%> = <%y,z,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:50

for x, y, z being object holds <%x,y,z%> * <%2,0,1%> = <%z,x,y%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:51

for x, y, z being object holds <%x,y,z%> * <%2,1,0%> = <%z,y,x%>

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:52

for x, y being object st x <> y holds
<%x,y%> is one-to-one

proof end;

:: into AFINSQ_1 ?

theorem :: COUNTERS:53

for x, y, z being object st x <> y & x <> z & y <> z holds
<%x,y,z%> is one-to-one

proof end;

definition

let R be Relation;

attr R is with_cardinal_domain means :Def1: :: COUNTERS:def 13
ex c being Cardinal st dom R = c;

end;

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

registration

cluster Relation-like empty -> with_cardinal_domain for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is with_cardinal_domain ;

cluster Relation-like Sequence-like finite -> with_cardinal_domain for set ;

coherence
for b₁ being Relation st b₁ is finite & b₁ is Sequence-like holds
b₁ is with_cardinal_domain

proof end;

cluster Relation-like with_cardinal_domain -> Sequence-like for set ;

coherence
for b₁ being Relation st b₁ is with_cardinal_domain holds
b₁ is Sequence-like by ORDINAL1:def 7;
let c be Cardinal;

cluster Relation-like c -defined Function-like total -> with_cardinal_domain for set ;

coherence
for b₁ being ManySortedSet of c holds b₁ is with_cardinal_domain by PARTFUN1:def 2;
let x be object ;

cluster c --> x -> with_cardinal_domain ;

coherence
c --> x is with_cardinal_domain ;

end;

registration

let X be set ;

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

coherence
for b₁ being Denumeration of X holds b₁ is with_cardinal_domain

proof end;

end;

registration

let c be Cardinal;

cluster Function-like quasi_total bijective -> with_cardinal_domain for Element of bool [:c,c:];

coherence
for b₁ being Permutation of c holds b₁ is with_cardinal_domain ;

end;

registration

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

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is trivial & b₁ is non-empty & b₁ is with_cardinal_domain & b₁ is Cardinal-yielding )

proof end;

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

existence
ex b₁ being Function st
( not b₁ is empty & not b₁ is trivial & b₁ is non-empty & b₁ is finite & b₁ is with_cardinal_domain & b₁ is Cardinal-yielding )

proof end;

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

existence
ex b₁ being Function st
( not b₁ is empty & b₁ is non-empty & b₁ is infinite & b₁ is with_cardinal_domain & b₁ is natural-valued )

proof end;

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

existence
ex b₁ being Function st
( not b₁ is trivial & b₁ is non-empty & b₁ is with_cardinal_domain & b₁ is Cardinal-yielding & not b₁ is natural-valued )

proof end;

end;

registration

let R be with_cardinal_domain Relation;

cluster dom R -> cardinal ;

coherence
dom R is cardinal

proof end;

end;

registration

let f be with_cardinal_domain Function;

identify dom f with card f;

correctness
compatibility
dom f = card f;

proof end;

end;

registration

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

cluster R * P -> with_cardinal_domain ;

coherence
R * P is with_cardinal_domain

proof end;

end;

registration

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

cluster f * g -> with_cardinal_domain ;

coherence
g * f is with_cardinal_domain

proof end;

end;

registration

let f be with_cardinal_domain Function;
let p be Permutation of (dom f);

cluster p * f -> with_cardinal_domain ;

coherence
f * p is with_cardinal_domain

proof end;

end;

theorem Th56: :: COUNTERS:54

for A, B being with_cardinal_domain Sequence st dom A in dom B holds
A ^ B is with_cardinal_domain

proof end;

registration

let p be XFinSequence;
let B be with_cardinal_domain Sequence;

cluster p ^ B -> with_cardinal_domain ;

coherence
p ^ B is with_cardinal_domain

proof end;

end;

definition

mode Counters is non empty Cardinal-yielding with_cardinal_domain Function;

end;

definition

mode Counters+ is non-empty non empty Cardinal-yielding with_cardinal_domain Function;

end;