List of theorems referencing the symbol AT_
(76) Theorem 55: [Map compositions are maps] Is_map(F @ G)
(87) Theorem 66: [Associativity of map multiplication] F @ (G @ H) = (F @ G) @ H
(126) Theorem 94: [Range and domain of map product] (range(F @ G) = range(F •ON range(G))) & ((range(G) •incin domain(F)) •imp (domain(F @ G) = domain(G)))
(127) Theorem 95: [Range and domain of map product, 2] (range(G) = domain(F)) •imp ((range(F @ G) = range(F)) & (domain(F @ G) = domain(G)))
(128) Theorem 96: [Range and domain of map product, 3] (range(G) •incin domain(F)) •imp ((range(F @ G) •incin range(F)) & (domain(F @ G) = domain(G)))
(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)
(151) Theorem 112: [Composition with the inverse map] Svm(F) •imp (F @ inv(F) = ident(range(F)))
(152) Theorem 113: [Inverses of one-one maps] one_1_map(F) •imp (((F @ inv(F)) = ident(range(F))) & ((inv(F) @ F) = ident(domain(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)
(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)))
(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)}))
(167) Theorem 128: [Composition of one-one maps] (one_1_map(F) & one_1_map(G)) •imp one_1_map(F @ G)
(170) Theorem 131: [Union of map composition] (F + FF) @ G = (F @ G) + (FF @ G)
(171) Theorem 132: [Union of map composition, 2] G @ (F + FF) = (G @ F) + (G @ FF)
(374) Theorem 323: [Composition of shift-maps yields a shift-map] ((M in Za) & (N in Za)) •imp (Shift(M) @ Shift(N) = Shift(M •PLUS N))
(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))
(385) Theorem subseq.1: (g = (f @ h_thryvar)) & one_1_map(h_thryvar) & (domain(h_thryvar) in next(Za)) & (range(h_thryvar) •incin domain(f)) & (FORALL i in domain(h_thryvar), j in domain(h_thryvar) | (i in j) •imp ((h_thryvar~[i]) in (h_thryvar~[j])))
(904) Theorem 749: [Continuous functions map limits into limits] (Cf_RR(F,S) & (G in ReCauchy) & (range(G) •incin S)) •imp ((F @ G in ReCauchy) & (limit(F @ G) = F~[limit(G)]))
(907) Theorem 752: [The composition of two real continuous functions is continuous.] (Cf_RR(F,S) & Cf_RR(G,T) & (range(G •ON T) •incin S)) •imp Cf_RR(F @ G,T)