List of theorems referencing the symbol SVM

(43) Theorem Svm_test.1: [Single-valuedness test] ((x_thryvar in s) & (y_thryvar in s) & (a(x_thryvar) = a(y_thryvar)) & (b(x_thryvar) /= b(y_thryvar))) or Svm({[a(x),b(x)]: x in s})
(44) Theorem Svm_test_2.1: [Single-valuedness test, two-variable case] ((x_thryvar in s) & (y_thryvar in t) & (xp_thryvar in s) & (yp_thryvar in t) & (a2(x_thryvar,y_thryvar) = a2(xp_thryvar,yp_thryvar)) & (b2(x_thryvar,y_thryvar) /= b2(xp_thryvar,yp_thryvar))) or Svm({[a2(x,y),b2(x,y)]: x in s, y in t | P2(x,y)})
(45) Theorem Svm_test_3.1: [Single-valuedness test, three-variable case] ((x_thryvar in s) & (y_thryvar in t) & (z_thryvar in u) & (xp_thryvar in s) & (yp_thryvar in t) & (zp_thryvar in u) & P3(x_thryvar,y_thryvar,z_thryvar) & P3(xp_thryvar,yp_thryvar,zp_thryvar) & (a3(x_thryvar,y_thryvar,z_thryvar) = a3(xp_thryvar,yp_thryvar,zp_thryvar)) & (b3(x_thryvar,y_thryvar,z_thryvar) /= b3(xp_thryvar,yp_thryvar,zp_thryvar))) or Svm({[a3(x,y,w),b3(x,y,w)]: x in s, y in t, w in u | P3(x,y,w)})
(74) Theorem 53: [Single-valued map subsets are single-valued] ((G •incin F) & Svm(F)) •imp Svm(G)
(78) Theorem 57: [Restrictions of single-valed maps are single-valued] Svm(F) •imp Svm(F •ON S)
(80) Theorem 59: [The null set as a map] Is_map(0) & Svm(0) & (one_1_map(0)) & (range(0) = 0) & (domain(0) = 0)
(101) Theorem fcn_symbol.7: [?] Svm(g)
(102) Theorem 72: [Form of a single-valued map] Svm(F) •eq (F = {[x,F~[x]]: x in domain(F)})
(103) Theorem 73: [Form of a single-valued map range] Svm(F) •imp (F = {[x,F~[x]]: x in domain(F)} & (range(F) = {F~[x]: x in domain(F)}))
(104) Theorem 74: [Map image formula] (Svm(F) & (X in F)) •imp (F~[car(X)] = cdr(X))
(108) Theorem Must_be_svm.1: [Single-valued map former] Svm({[x,b(x)]: x in s}) & (domain({[x,b(x)]: x in s}) = s) & (range({[x,b(x)]: x in s}) = {b(x): x in s}) & ((u in s) •imp ({[x,b(x)]: x in s}~[u] = b(u)))
(109) Theorem Must_be_svm_2.1: [Single-valued map former, two-variable case] Svm({[[x,y],b2(x,y)]: x in s, y in t | P2(x,y)})
(119) Theorem 87: [Union of single_valued maps] (Svm(F) & Svm(G) & (domain(F) * domain(G) = 0)) •imp Svm(F + G)
(123) Theorem 91: [Singletons as maps] Svm({[X,Y]}) & one_1_map({[X,Y]}) & (({[X,Y]}~[X]) = Y)
(151) Theorem 112: [Composition with the inverse map] Svm(F) •imp (F @ inv(F) = ident(range(F)))
(153) Theorem 114: [Product of inverses lemma] (Is_map(F) & Is_map(G) & (domain(F) •incin range(G)) & Svm(F @ G)) •imp Svm(F)
(155) Theorem 116: [One-one-ness and singlevaluedness] one_1_map(F) •eq (Svm(F) & Svm(inv(F)))
(157) Theorem 118: [Single-valued map restrictions as setformers] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F) | x in S}) & (domain(F •ON S) = {x: x in domain(F) | x in S}) & (range(F •ON S) = {F~[x]: x in domain(F) | x in S}))
(160) Theorem 121: [Single-valued map restrictions as setformers, 2] Svm(F) •imp (((F •ON S) = {[x,F~[x]]: x in domain(F •ON S)}) & (range(F •ON S) = {F~[x]: x in domain(F •ON S)}))
(162) Theorem 123: [Composition of single-valued maps] (Svm(F) & Svm(G)) •imp Svm(F @ G)
(163) Theorem 124: [Images under single-valued map composition] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp ((F @ G)~[X] = F~[G~[X]])
(164) Theorem 125: [Single-valued map ranges and domains as set formers] (Svm(F) & Svm(G) & (X in domain(G)) & (range(G) •incin domain(F))) •imp (((F @ G)~[X] = F~[G~[X]]) & (F @ G = {[x,F~[G~[x]]]: x in domain(G)}) & (range(F @ G) = {F~[G~[x]]: x in domain(G)}))
(165) Theorem 126: [Image under single-valued map] (Svm(F) & (G •incin F) & (X in domain(G))) •imp (F~[X]=G~[X])
(168) Theorem 129: [Elements are defined uniquely by their one-one images] Svm(F) •imp (one_1_map(F) •eq (FORALL x in domain(F), y in domain(F) | ((F~[x] = F~[y]) •imp (x = y))))
(172) Theorem 133: [Single-valued maps have 1-1 partial inverses] Svm(F) •imp (EXISTS h | ((domain(h) = range(F)) & (range(h) •incin domain(F)) & one_1_map(h)) & (FORALL x in range(F) | (F~[h~[x]] = x)))
(205) Theorem 166: [Single-valued mapping cannot increase cardinality] Svm(F) •imp (#range(F) •incin #domain(F))
(208) Theorem 169: [The cardinality of a single-valued map equals the cardinality of its domain] Svm(F) •imp (#domain(F) = #F)
(209) Theorem 170: [Cardinality of restriction maps] (Svm(F) & (domain(F) incs A)) •imp (#(F •ON A) = #A)
(211) Theorem 171: [Condition for existence of a single-valued map between two sets] (#S incs #T) •eq (T = 0 or (EXISTS f in OM | Svm(f) & (domain(f) = S) & (range(f) = T)))
(213) Theorem 173: [Range-decomposition of a map domain] ((S * R = 0) & Svm(G)) •imp (((G •INV_IM S) * (G •INV_IM R)) = 0)
(216) Theorem 176: [Single-valued inverse image as a setformer] Svm(inv(G)) •imp (G •INV_IM R = {inv(G)~[w]: w in (R * range(G))})
(219) Theorem 179: [Range of a single-valued map restricted to an inverse image] Svm(G) •imp (range(G •ON (G •INV_IM A)) = range(G) * A)
(220) Theorem 180: [Inverse images by a single-valued map] Svm(G) •imp ((G •ON (G •INV_IM A)) •INV_IM B = (G •INV_IM A) * (G •INV_IM B))
(227) Theorem 187: [A single_valued map with finite domain has a finite range] (Svm(F) & Finite(domain(F))) •imp Finite(range(F))
(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)))))
(369) Theorem 318: [Finite sequences are single_valued maps with integer domains] (F in Fin_seqs(S)) •eq (Svm(F) & (domain(F) in Za) & (range(F) •incin S))
(371) Theorem 320: [Two single-valued functions with common domain are equal if all their values are equal] (Svm(F) & Svm(G) & (domain(F) = S) & (domain(G) = S) & (FORALL n0 in S | F~[n0] = G~[n0])) •imp (F = G)
(372) Theorem 321: [Two functions from a collection of single-valued functions with common domain are equal if all their values are equal] ((S /= 0) & (FORALL h in Mapset | ((domain(h) = S) & Svm(h)))) •imp ((FORALL n in S | ((F in Mapset) & (G in Mapset) & (F~[n] = G~[n]))) •imp (F = G))
(373) Theorem 322: [The shift-map of an integer is single-valued and maps Za into Za] ((M in Za) & (N in Za)) •imp (Svm(Shift(M)) & (domain(Shift(M)) = Za) & (range(Shift(M)) •incin Za) & (Shift(M)~[N] = M •PLUS N))
(379) Theorem 328: [Properties of finite and shifted finite sequences] ((F in Fin_seqs(S)) & (G in Fin_seqs(S))) •imp (Svm({[car(x) •PLUS #F, cdr(x)]: x in G}) & (domain(F) * domain({[car(x) •PLUS #F, cdr(x)]: x in G}) = 0))
(387) Theorem subseq.3: Svm(g) & (g •incin (domain(f) •PROD range(f))) & (domain(g) in (next(Za) * next(domain(f))))
(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)}))
(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))
(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))))))
(671) Theorem pointwiseU.2: Svm(h) & (domain(h) = d) & (range(h) •incin r)
(674) Theorem pointwise.2: Svm(h) & (domain(h) = d) & (range(h) •incin r)
(678) Theorem 527: (F in RaSeq) •imp ((domain(F) = Za) & Svm(F) & (range(F) •incin Ra) & Ra_eqseq(F,F))
(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)})))
(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)))