List of theorems referencing the symbol FINITE

(223) Theorem 183: [0 is a finite cardinal] Ord(0) & Finite(0) & Card(0)
(224) Theorem 184: [A subset of a finite set is finite] (Finite(S) & (S incs T)) •imp Finite(T)
(225) Theorem 185: [One-one maps preserve finiteness] one_1_map(F) •imp ((Finite(domain(F))) •imp (Finite(range(F))))
(226) Theorem 186: [One-one maps preserve finiteness, 2] one_1_map(F) •imp (Finite(domain(F)) •eq Finite(range(F)))
(227) Theorem 187: [A single_valued map with finite domain has a finite range] (Svm(F) & Finite(domain(F))) •imp Finite(range(F))
(228) Theorem finite_image.1: [Any image of a finite set is finite] Finite({e(x): x in s0})
(229) Theorem 188: [A set is finite if and only if its cardinality is finite] Finite(S) •eq Finite(#S)
(230) Theorem 189: [Proper subsets of a finite set have fewer elements] (Finite(S) & (T •incin S) & (T /= S)) •imp (#T in #S)
(231) Theorem 190: [A set is finite if and only if it is not the single-valued image of any of its finite subsets] Finite(S) •eq (not(EXISTS f in OM | (Svm(f) & (range(f) = S) & (domain(f) •incin S) & (S /= domain(f)))))
(232) Theorem 191: [Members of a finite ordinal are finite] (Ord(S) & Finite(S) & (T in S)) •imp Finite(T)
(233) Theorem 192: [Any infinite ordinal is larger than any finite ordinal] (Ord(S) & Ord(T) & (not Finite(S)) & Finite(T)) •imp (T in S)
(235) Theorem 194: [Adding one element to a finite set leaves it finite] Finite(S) •eq Finite(S + {X})
(236) Theorem 195: [Finiteness of successor set] Finite(S) •imp Finite(next(S))
(237) Theorem 196: [Singletons are finite] Finite({S})
(238) Theorem 197: [Doubletons are finite] Finite({S,T})
(239) Theorem 198: [The basic infinite set is not finite] not(Finite(s_inf))
(240) Theorem 199: [Infinite cardinality theorem] not Finite(#s_inf)
(241) Theorem 200: [All finite ordinals are cardinals] (Ord(X) & Finite(X)) •imp Card(X)
(246) Theorem setformer_meet_join.5: [Setformer finiteness implication, two-variable case] Finite({[u,v]: u in s, v in t | R(u,v)}) •imp Finite({h(u,v): u in s, v in t | R(u,v)})
(247) Theorem 201: [The set of integers is an infinite ordinal consisting of all finite ordinals] Ord(Za) & (not Finite(Za)) & ((Card(X) & Finite(X)) •eq (X in Za))
(248) Theorem 202: [All integers are finite ordinals and cardinals] (X in Za) •imp ((X = #X) & Card(X) & Ord(X) & Finite(X))
(274) Theorem 228: [Strict monotonicity of finite cardinality] (Finite(N) & (M •incin N) & (M /= N)) •imp (#M in #N)
(276) Theorem 229: [The union of finite sets is finite] (Finite(N) & Finite(M)) •eq Finite(N + M)
(277) Theorem 230: [Removal of an initial segment from Za yields an infinite set] (N in Za) •imp (not Finite(Za - N))
(278) Theorem 231: [The union of finitely many finite sets is finite] ((FORALL x in S | Finite(x)) & Finite(S)) •imp Finite(Un(S))
(279) Theorem 232: [An arithmetic sum is finite if its two terms are finite] Finite(N •PLUS M) •eq Finite(N + M)
(280) Theorem 233: [An arithmetic sum is finite if and only if both its terms are finite] (Finite(N) & Finite(M)) •eq Finite(N •PLUS M)
(283) Theorem 236: [existence of an in-maximal set in any finite set] (EXISTS v | Finite(F) •imp (((F = 0) or (v in F)) & ({y in (F-{v}) | v in Ult_membs({y})} = 0)))
(300) Theorem 253: [The arithmetic product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •TIMES M)
(301) Theorem 254: [The Cartesian product of two finite sets is finite] (Finite(N) & Finite(M)) •imp Finite(N •PROD M)
(302) Theorem 255: [If the product of two nonzero terms is finite, so are the terms] ((Finite(N) & Finite(M)) or N = 0 or M = 0) •eq Finite(N •TIMES M)
(303) Theorem 256: [A set is finite if and only if its powerset is finite] Finite(N) •eq Finite(pow(N))
(343) Theorem 296: [Cardinality of set difference] (Finite(N) & (N incs M)) •imp (#(N - M) = #(#N - #M))
(350) Theorem 303: [The union set of a finite collection of integers is an integer] ((M •incin Za) & Finite(M)) •imp (((M /= 0) •imp (Un(M) in M)) & (Un(M) in Za))
(363) Theorem unsigned_integer_bynd.1: [Every finite set of unsigned integers has an upper bound] (bynd_thryvar in Za) & (Za incs bynd_thryvar) & Ord(bynd_thryvar) & (FORALL i in Za | (Q1(i) •imp (i in bynd_thryvar))) & (not Finite(Za - bynd_thryvar))
(364) Theorem cauchyseq_lemma.1: (not Finite({i * j : i in (Za - n0), j in (Za - n0) | R(i,j)}))
(370) Theorem 319: [Other properties of finite sequences] (F in Fin_seqs(S)) •imp ((domain(F) = #domain(F)) & (domain(F) = #F) & (#F in Za) & Finite(F))
(388) Theorem subseq.4: (domain(h_thryvar) /= Za) •imp Finite(g)
(431) Theorem 338: ['One-more' lemma] (not Finite(S)) •imp (#S = #(S + {C}))
(432) Theorem 339: ['Few-more' lemma] ((not Finite(S)) & Finite(T)) •imp (#S = #(S + T))
(433) Theorem 340: [Any infinite cardinal is a limit ordinal] ((not Finite(S)) & (X in #S)) •imp (X + {X} in #S)
(434) Theorem 341: [If ordinal S dominates the members of an ordinal T, #S is no less than #T] (Ord(S) & Ord(T) & (not Finite(S)) & (FORALL u in T | #u in #S)) •imp (#T •incin #S)
(437) Theorem 344: (Card(O1) & Card(O2) & (not Finite(O1 + O2))) •imp (EXISTS f in OM | one_1_map(f) & Ord(domain(f)) & (range(f) = (O1 •PROD O2)) & (FORALL x in domain(f) | (EXISTS y in (O1 + O2) | range(f •ON x) •incin (y •PROD y))))
(438) Theorem 345: [Cardinal Doubling Theorem] (not Finite(S)) •imp (#(S •PROD {0,1}) = #S)
(439) Theorem 346: [The sum of two infinite quantities is their maximum] (not Finite(S)) •imp ((S •PLUS T) = #S + #T)
(440) Theorem 347: [The cardinality of the union of two infinite quantities is the cardinality of the larger] (not Finite(S)) •imp (#(S + T) = #S + #T)
(441) Theorem 348: [Cardinal Square Theorem] (not Finite(S)) •imp (#(S •PROD S) = #S)
(504) Theorem 394: ((FORALL v in X | Finite(v)) & (U •incin X) & (U /= 0)) •imp (EXISTS w in U | (FORALL y in U | not((y •incin w) & (y /= w))))
(507) Theorem finite_recursive_fcn.1: (FORALL s,t | (EXISTS h | (FORALL x | ((x •incin s) & Finite(x)) •imp (h~[x] = f3({g4(h~[y],y,x,t): y •incin x | (y /= x) & P4(h~[y],y,x,t)},x,t)))))
(507+) Theorem finite_recursive_fcn.a: (FORALL s,t | (FORALL x | ((x •incin s) & Finite(x)) •imp (hsko(s,t)~[x] = f3({g4(hsko(s,t)~[y],y,x,t): y •incin x | (y /= x) & P4(hsko(s,t)~[y],y,x,t)},x,t))))
(508) Theorem finite_recursive_fcn.2: (FORALL x | ((x •incin S) & Finite(x)) •imp (hsko(S,T)~[x] = f3({g4(hsko(S,T)~[y],y,x,T): y •incin x | (y /= x) & P4(hsko(S,T)~[y],y,x,T)},x,T)))
(509) Theorem finite_recursive_fcn.3: Finite(S) •imp (h2_thryvar(S,T) = f3({g4(h2_thryvar(y,T),y,S,T): y •incin S | (y /= S) & P4(h2_thryvar(y,T),y,S,T)},S,T))
(510) Theorem finite_tailrecursive_fcn.0: (FORALL s,t | Finite(s) •imp (h2_thryvar(s,t) = if ({g3(h2_thryvar(y,t),s,t): y •incin s | (y /= s) & (y = sl(s))} = 0) then f(t) else arb({g3(h2_thryvar(y,t),s,t): y •incin s | (y /= s) & (y = sl(s))}) end if))
(511) Theorem finite_tailrecursive_fcn.1: Finite(S) •imp (h2_thryvar(S,T) = if (S = 0) then f(T) else g3(h2_thryvar(sl(S), T), S,T) end if)
(512) Theorem finite_tailrecursive_fcn1.1: (FORALL s,t | Finite(s) •imp (h2_thryvar(s,t) = if (s = 0) then f(t) else g3(h2_thryvar(s - {arb(s)}, t), s,t) end if))
(513) Theorem finite_tailrecursive_fcn2.0: (FORALL s,t | Finite(s) •imp (h(s,t) = if s = 0 then f0 else g2(h(s - {arb(s)},t),s) end if))
(514) Theorem finite_tailrecursive_fcn2.1: Finite(S) •imp (h1_thryvar(S) = if S = 0 then f0 else g2(h1_thryvar(S - {arb(S)}),S) end if)
(515) Theorem sigma_theory0: [Recursive formula for generalized sum] (FORALL x | Finite(x) •imp (sigma_thryvar(x) = if x = 0 then e else pluz(sigma_thryvar(x - {arb(x)}),cdr(arb(x))) end if))
(517+) Theorem sigma_theory3: [Sum value belongs to closed range of map] (Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) in s)
(518) Theorem sigma_theory4: [Removal of single element from domain of a sum] ((C in F) & Finite(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F - {C}),cdr(C)))
(519) Theorem sigma_theory5: [The generalized sum of a union map is a sum of sums] (Finite(F) & Is_map(F) & (range(F) •incin s)) •imp (sigma_thryvar(F) = pluz(sigma_thryvar(F •ON (domain(F) * T)), sigma_thryvar(F •ON (domain(F) - T))))
(520) Theorem sigma_theory6: [Rearrangement-of-sums theorem] (Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,sigma_thryvar(F •ON (G •INV_IM {y}))]: y in range(G)}))
(520+) Theorem sigma_theory7: [Sum permutation theorem] (Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin s)) •imp (sigma_thryvar(F) = sigma_thryvar({[y,F~[inv(G)~[y]]]: y in range(G)}))
(533) Theorem linear_order_12: (FORALL f | (Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) in next(s0))) & (FORALL x | (cdr(x) in next(s0)) •imp (min_over_thryvar({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f •ON (domain(f) * t)),min_over_thryvar(f •ON (domain(f) - t))))) & (FORALL c,f | ((c in f) & Finite(f) & (range(f) •incin next(s0))) •imp (min_over_thryvar(f) = smaller_thryvar(min_over_thryvar(f - {c}),cdr(c))))
(534) Theorem linear_order_13: (Svm(F) & (range(F) •incin s0) & Finite(F)) •imp (((P in F) •imp (min_over_thryvar({P}) = (F~[car(P)]))) & (min_over_thryvar(F) = smaller_thryvar(min_over_thryvar(F •ON (domain(F) * A)),min_over_thryvar(F •ON (domain(F) - A)))))
(535) Theorem linear_order_14: (Svm(F) & (range(F) •incin s0) & Finite(F) & (F /= 0)) •imp (min_over_thryvar(F) in range(F))
(539) Theorem linear_order_18: (Finite(T) & (X in T) & (T •incin s0)) •imp ((max_thryvar(T) in T) & ((X = max_thryvar(T)) or (arg1_bef_arg2(X,max_thryvar(T)))))
(541) Theorem linear_order_20: (FORALL x, y | larger_thryvar(x,y) = if ((x notin s0) & (y notin s0)) then s0 elseif (x notin s0) then y elseif (y notin s0) then x elseif arg1_aft_arg2(x,y) then x else y end if) & (FORALL x, y | larger_thryvar(x,y) = larger_thryvar(y,x)) & (FORALL x, y | ({x,y} •incin s0) •imp (larger_thryvar(x,y) in {x,y})) & (FORALL x | (x in next(s0)) •imp (larger_thryvar(x,s0) = x)) & (FORALL x, y, z | larger_thryvar(x,larger_thryvar(y,z)) = larger_thryvar(larger_thryvar(x,y),z)) & (FORALL x, y | ((x in next(s0)) & (y in next(s0))) •imp (larger_thryvar(x,y) in next(s0))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin s0) & Finite(f)) •imp (((p in f) •imp (max_over_thryvar({p}) = (f~[car(p)]))) & (max_over_thryvar(f) = larger_thryvar(max_over_thryvar(f •ON (domain(f) * a)),max_over_thryvar(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin s0) & Finite(f) & (f /= 0)) •imp (max_over_thryvar(f) in range(f))) & (FORALL x, y | ({x,y} •incin s0) •imp ((larger_thryvar(x,y) = x) •eq (arg1_aft_arg2(x,y) or (x = y)))) & (FORALL t | lbs_thryvar(t) = {x in s0 | (FORALL y in (t * s0) | larger_thryvar(y,x) = y)}) & (FORALL t | min_thryvar(t) = arb({s0} + (t * lbs_thryvar(t)))) & (FORALL t | glb_thryvar(t) = arb({s0} + {x in lbs_thryvar(t) | lbs_thryvar(t) •incin lbs_thryvar({x})})) & (lbs_thryvar(0) = s0) & (min_thryvar(0) = s0) & (FORALL t | (lbs_thryvar(t) •incin s0) & (lbs_thryvar(t) = lbs_thryvar(t * s0)) & (min_thryvar(t) = min_thryvar(t * s0))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin s0)) •imp ((min_thryvar(t) in t) & ((x = min_thryvar(t)) or (arg1_aft_arg2(x,min_thryvar(t))))))
(643) Theorem 496: (FORALL x, y | smaller_Ra(x,y) = if ((x notin Ra) & (y notin Ra)) then Ra elseif (x notin Ra) then y elseif (y notin Ra) then x elseif (x •Ra_LT y) then x else y end if) & (FORALL x, y | smaller_Ra(x,y) = smaller_Ra(y,x)) & (FORALL x, y | ({x,y} •incin Ra) •imp (smaller_Ra(x,y) in {x,y})) & (FORALL x | (x in next(Ra)) •imp (smaller_Ra(x,Ra) = x)) & (FORALL x, y, z | smaller_Ra(x,smaller_Ra(y,z)) = smaller_Ra(smaller_Ra(x,y),z)) & (FORALL x, y | ((x in next(Ra)) & (y in next(Ra))) •imp (smaller_Ra(x,y) in next(Ra))) & (FORALL f,p,a | (Svm(f) & (range(f) •incin Ra) & Finite(f)) •imp (((p in f) •imp (min_over_Ra({p}) = (f~[car(p)]))) & (min_over_Ra(f) = smaller_Ra(min_over_Ra(f •ON (domain(f) * a)),min_over_Ra(f •ON (domain(f) - a)))))) & (FORALL f | (Svm(f) & (range(f) •incin Ra) & Finite(f) & (f /= 0)) •imp (min_over_Ra(f) in range(f))) & (FORALL x, y | ({x,y} •incin Ra) •imp ((smaller_Ra(x,y) = x) •eq ((x •Ra_LT y) or (x = y)))) & (FORALL t | ubs_Ra(t) = {x in Ra | (FORALL y in (t * Ra) | smaller_Ra(y,x) = y)}) & (FORALL t | max_Ra(t) = arb({Ra} + (t * ubs_Ra(t)))) & (FORALL t | lub_Ra(t) = arb({Ra} + {x in ubs_Ra(t) | ubs_Ra(t) •incin ubs_Ra({x})})) & (ubs_Ra(0) = Ra) & (max_Ra(0) = Ra) & (FORALL t | (ubs_Ra(t) •incin Ra) & (ubs_Ra(t) = ubs_Ra(t * Ra)) & (max_Ra(t) = max_Ra(t * Ra))) & (FORALL t, x | (Finite(t) & (x in t) & (t •incin Ra)) •imp ((max_Ra(t) in t) & ((x = max_Ra(t)) or ((x •Ra_LT max_Ra(t))))))
(668) Theorem 522: [Reformulation of condition for sequence equivalence] ({F,G} •incin RaSeq) •imp (Ra_eqseq(F,G) •eq (FORALL eps in Ra | (eps •Ra_GT Ra_0) •imp Finite({x : x in Za | Ra_ABS((F~[x]) •Ra_MINUS (G~[x])) •Ra_GT eps})))
(681) Theorem 530: ((F in RaCauchy) & (G in Subseqs(F)) & (not Finite(G))) •imp ((G in RaCauchy) & Ra_eqseq(F,G))
(689) Theorem 538: ((S •incin Ra) & Finite(S)) •imp (EXISTS u in Ra | (FORALL y in S | u •Ra_GE y))
(690) Theorem 539: [Every finite set of integers has a strict upper bound] ((S •incin Za) & Finite(S)) •imp (EXISTS u in Za | (FORALL y in S | y in u))
(694) Theorem 543: ((G in RaCauchy) & (not Ra_eqseq(G,Ra0Seq))) •imp (EXISTS eps in Ra | (eps •Ra_GT Ra_0) & Finite({i in Za | eps •Ra_GE Ra_ABS(G~[i])}))
(864) Theorem 710a: [The images of rationals via the embedding form a dense subset of the reals, 1] ((X in Re) & (Eps in Ra) & (Eps •Ra_GT Ra_0)) •imp (EXISTS y in Ra | Finite({m in Za | Ra_ABS(((arb(X))~[m]) •Ra_MINUS y) •Ra_GE Eps}) )
(896) Theorem 741: (FORALL s, x | (Finite(s) •imp (ToThe1(s,x) = if (s = 0) then R_1 else ToThe1(s - {arb(s)},x) •R_TIMES x end if)))
(900) Theorem 745: (R_SIGMA(0) = R_0) & (FORALL x in OM | (cdr(x) in Re) •imp (R_SIGMA({x}) = cdr(x))) & (FORALL f in OM | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) in Re)) & (FORALL f in OM, c in f | (Finite(f) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA(f - {c}) •R_PLUS cdr(c))) & (FORALL f in OM | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (FORALL t | R_SIGMA(f) = R_SIGMA(f •ON (domain(f) * t)) •R_PLUS R_SIGMA(f •ON (domain(f) - t)))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & Svm(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,R_SIGMA(f •ON (g •INV_IM {y}))]: y in range(g)}))) & (FORALL f in OM, g | (Finite(f) & Svm(f) & one_1_map(g) & (domain(f) = domain(g)) & (range(f) •incin Re)) •imp (R_SIGMA(f) = R_SIGMA({[y,f~[inv(g)~[y]]]: y in range(g)})))
(901) Theorem 746: (R_SIGMA(0) = R_0) & ((cdr(X) in Re) •imp (R_SIGMA({X}) = cdr(X))) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) in Re)) & ((Finite(F) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA(F - {c}) •R_PLUS cdr(c))) & ((Finite(F) & Is_map(F) & (range(F) •incin Re)) •imp R_SIGMA(F) = R_SIGMA(F •ON (domain(F) * T)) •R_PLUS R_SIGMA(F •ON (domain(F) - T))) & ((Finite(F) & Svm(F) & Svm(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,R_SIGMA(F •ON (G •INV_IM {y}))]: y in range(G)}))) & ((Finite(F) & Svm(F) & one_1_map(G) & (domain(F) = domain(G)) & (range(F) •incin Re)) •imp (R_SIGMA(F) = R_SIGMA({[y,F~[inv(G)~[y]]]: y in range(G)})))
(914) Theorem 759: (BoundedClosedRe(S) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T})) & (FORALL ends in T | ends in (Re •PROD Re))) •imp (EXISTS T1 | (T1 •incin T) & Finite(T1) & (S •incin Un({OI(car(ends),cdr(ends)): ends in T1})))
(947) Theorem real_sigma0: (FORALL f | (Finite(f) & (range(f) •incin Re)) •imp (Sig(f) in Re)) & (FORALL x | (cdr(x) in Re) •imp (Sig({x}) = cdr(x))) & (FORALL f,t | (Finite(f) & Is_map(f) & (range(f) •incin Re)) •imp (Sig(f) = (Sig(f •ON (domain(f) * t)) •R_PLUS Sig(f •ON (domain(f) - t)))))
(948) Theorem real_sigma: (Svm(F) & (range(F) •incin Re) & Finite(F)) •imp ((Sig(F) in Re) & ((P in F) •imp (Sig({P}) = (F~[car(P)]))) & (Sig(F) = (Sig(F •ON (domain(F) * A)) •R_PLUS Sig(F •ON (domain(F) - A)))))
(955) Theorem real_function_sigma: (Svm(ser) & (range(ser) •incin RF) & Finite(ser)) •imp ((FSig(ser) in RF & (p in ser) •imp (Sig({p}) = ser(car(p)))) &(FORALL a | Sig(ser) = Sig(ser •ON (domain(ser) * a)) •R_PLUS Sig(ser •ON domain(ser) - a)))