List of theorems referencing the symbol IS_MAP

(39) Theorem 26: [Maps are mapformers] Is_map(F) •eq (F •incin {[car(x),cdr(x)]: x in F})
(40) Theorem iz_map.1: [Mapformers are maps] Is_map({[a(x),b(x)]: x in s}) & (domain({[a(x),b(x)]: x in s}) = {a(x): x in s}) & (range({[a(x),b(x)]: x in s}) = {b(x): x in s})
(41) Theorem iz_map_2.1: [Two-variable mapformers] Is_map({[a2(x,y),b2(x,y)]: x in s, y in t | P2(x,y)})
(42) Theorem iz_map_3.1: [Three-variable mapformers] Is_map({[a3(x,y,yy),b3(x,y,yy)]: x in s, y in t, yy in u | P3(x,y,yy)})
(72) Theorem 51: [Map members are pairs] (Is_map(F) •imp ((X in F) •imp (X = [car(X),cdr(X)]))) & ((FORALL x in F | x = [car(x),cdr(x)]) •imp Is_map(F))
(73) Theorem 52: [Map subsets are maps] (G •incin F & Is_map(F)) •imp Is_map(G)
(76) Theorem 55: [Map compositions are maps] Is_map(F @ G)
(77) Theorem 56: [Map restrictions are maps] Is_map(F) •imp Is_map(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)
(83) Theorem 62: [Map unions are maps] (Is_map(F) & Is_map(G)) •imp Is_map(F + G)
(106) Theorem 76: [Map members are pairs, 2] (Is_map(F) & (U in F)) •imp (U = [car(U),cdr(U)])
(107) Theorem 77: [Map domain member lemma] Is_map(F) •imp ((X in domain(F)) •eq ([X,F~[X]] in F))
(122) Theorem 90: [Members of the inverse map] Is_map(F) •imp (([X,Y] in F) •eq ([Y,X] in inv(F)))
(130) Theorem 98: [Inverse map basic properties] Is_map(inv(F)) & range(inv(F)) = domain(F) & domain(inv(F)) = range(F)
(131) Theorem 99: [Double inverse map] Is_map(F) •imp (F = inv(inv(F)))
(149) Theorem 110: [Elementary properties of identity maps] one_1_map(ident(S)) & (domain(ident(S)) = S) & (range(ident(S)) = S) & (inv(ident(S)) = ident(S)) & ((X in S) •imp (ident(S)~[X] = X)) & (Is_map(F) •imp (((domain(F) •incin S) •imp (F @ ident(S) = F)) & ((range(F) •incin S) •imp (ident(S) @ F = F))))
(150) Theorem 111: [Composition with an identity map is restriction] (Is_map(F)) •imp (F @ ident(S) = F •ON S)
(153) Theorem 114: [Product of inverses lemma] (Is_map(F) & Is_map(G) & (domain(F) •incin range(G)) & Svm(F @ G)) •imp Svm(F)
(154) Theorem 115: [Product of Inverses] (Is_map(F) & Is_map(G)) •imp (inv(F @ G) = inv(G) @ inv(F))
(156) Theorem 117: [An inverse pair of maps must be 1-1 and must be each other's inverses] (Is_map(F) & Is_map(G) & (domain(F) = range(G)) & (range(F) = domain(G)) & (F @ G = ident(range(F))) & (G @ F = ident(domain(F)))) •imp (one_1_map(F) & (G = inv(F)))
(166) Theorem 127: [Single-valued and one-one maps] Is_map(F) •imp (one_1_map(F) •eq one_1_map(inv(F)))
(175) Theorem 136: [Subsets of Cartesian products] (Y •incin (S •PROD T)) •eq (Is_map(Y) & (domain(Y) •incin S) & (range(Y) •incin T))
(376) Theorem 325: [Shift(0) is the identity map on Za] (Shift(0) = {[n,n]: n in Za}) & ((Is_map(F) & (domain(F) •incin Za)) •imp (F @ Shift(0) = F))
(377) Theorem 326: [Shift-by-0 is the identity map on sequences] (Is_map(F) & (domain(F) •incin Za)) •imp (shifted_seq(F,0) = F)
(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))))
(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))))
(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)})))
(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)))))