Structure iterateTheory
signature iterateTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FINREC_def : thm
val ITSET_def : thm
val inf : thm
val iterate : thm
val monoidal : thm
val neutral : thm
val nsum_def : thm
val numseg : thm
val polynomial_function : thm
val sum_def : thm
val support : thm
(* Theorems *)
val CARD_BIGUNION : thm
val CARD_EQ_NSUM : thm
val CARD_EQ_SUM : thm
val CARD_NUMSEG : thm
val CARD_NUMSEG_1 : thm
val CARD_NUMSEG_LEMMA : thm
val CARD_UNION_EQ : thm
val CHOOSE_SUBSET : thm
val CHOOSE_SUBSET_STRONG : thm
val DISJOINT_NUMSEG : thm
val FINITE_INDEX_NUMBERS : thm
val FINITE_INDEX_NUMSEG : thm
val FINITE_NUMSEG : thm
val FINITE_REAL_INTERVAL : thm
val FINITE_RECURSION : thm
val FINITE_RESTRICT : thm
val FINITE_SUPPORT : thm
val FINITE_SUPPORT_DELTA : thm
val FINREC_1_LEMMA : thm
val FINREC_EXISTS_LEMMA : thm
val FINREC_FUN : thm
val FINREC_FUN_LEMMA : thm
val FINREC_SUC_LEMMA : thm
val FINREC_UNIQUE_LEMMA : thm
val FINREC_compute : thm
val FORALL_IN_GSPEC : thm
val HAS_SIZE_NUMSEG : thm
val HAS_SIZE_NUMSEG_1 : thm
val INF : thm
val INF_EQ : thm
val INF_FINITE : thm
val INF_FINITE_LEMMA : thm
val INF_INSERT_FINITE : thm
val INF_SING : thm
val INF_UNIQUE_FINITE : thm
val IN_NUMSEG : thm
val IN_NUMSEG_0 : thm
val IN_SUPPORT : thm
val ITERATE_BIJECTION : thm
val ITERATE_CASES : thm
val ITERATE_CLAUSES : thm
val ITERATE_CLAUSES_GEN : thm
val ITERATE_CLAUSES_NUMSEG : thm
val ITERATE_CLOSED : thm
val ITERATE_DELETE : thm
val ITERATE_DELTA : thm
val ITERATE_DIFF : thm
val ITERATE_DIFF_GEN : thm
val ITERATE_EQ : thm
val ITERATE_EQ_GENERAL : thm
val ITERATE_EQ_GENERAL_INVERSES : thm
val ITERATE_EQ_NEUTRAL : thm
val ITERATE_EXPAND_CASES : thm
val ITERATE_IMAGE : thm
val ITERATE_IMAGE_NONZERO : thm
val ITERATE_INCL_EXCL : thm
val ITERATE_INJECTION : thm
val ITERATE_ITERATE_PRODUCT : thm
val ITERATE_OP : thm
val ITERATE_OP_GEN : thm
val ITERATE_PAIR : thm
val ITERATE_RELATED : thm
val ITERATE_SING : thm
val ITERATE_SUPERSET : thm
val ITERATE_SUPPORT : thm
val ITERATE_UNION : thm
val ITERATE_UNION_GEN : thm
val ITERATE_UNION_NONZERO : thm
val LOWER_BOUND_FINITE_SET_REAL : thm
val MOD_NSUM_MOD : thm
val MOD_NSUM_MOD_NUMSEG : thm
val MONOIDAL_AC : thm
val MONOIDAL_ADD : thm
val MONOIDAL_MUL : thm
val MONOIDAL_REAL_ADD : thm
val MONOIDAL_REAL_MUL : thm
val NEUTRAL_ADD : thm
val NEUTRAL_MUL : thm
val NEUTRAL_REAL_ADD : thm
val NEUTRAL_REAL_MUL : thm
val NSUM_0 : thm
val NSUM_ADD : thm
val NSUM_ADD_GEN : thm
val NSUM_ADD_NUMSEG : thm
val NSUM_ADD_SPLIT : thm
val NSUM_BIGUNION_NONZERO : thm
val NSUM_BIJECTION : thm
val NSUM_BOUND : thm
val NSUM_BOUND_GEN : thm
val NSUM_BOUND_LT : thm
val NSUM_BOUND_LT_ALL : thm
val NSUM_BOUND_LT_GEN : thm
val NSUM_CASES : thm
val NSUM_CLAUSES : thm
val NSUM_CLAUSES_LEFT : thm
val NSUM_CLAUSES_NUMSEG : thm
val NSUM_CLAUSES_RIGHT : thm
val NSUM_CLOSED : thm
val NSUM_CONST : thm
val NSUM_CONST_NUMSEG : thm
val NSUM_DEGENERATE : thm
val NSUM_DELETE : thm
val NSUM_DELTA : thm
val NSUM_DIFF : thm
val NSUM_EQ : thm
val NSUM_EQ_0 : thm
val NSUM_EQ_0_IFF : thm
val NSUM_EQ_0_IFF_NUMSEG : thm
val NSUM_EQ_0_NUMSEG : thm
val NSUM_EQ_GENERAL : thm
val NSUM_EQ_GENERAL_INVERSES : thm
val NSUM_EQ_NUMSEG : thm
val NSUM_EQ_SUPERSET : thm
val NSUM_GROUP : thm
val NSUM_IMAGE : thm
val NSUM_IMAGE_GEN : thm
val NSUM_IMAGE_NONZERO : thm
val NSUM_INCL_EXCL : thm
val NSUM_INJECTION : thm
val NSUM_LE : thm
val NSUM_LE_GEN : thm
val NSUM_LE_NUMSEG : thm
val NSUM_LMUL : thm
val NSUM_LT : thm
val NSUM_LT_ALL : thm
val NSUM_MULTICOUNT : thm
val NSUM_MULTICOUNT_GEN : thm
val NSUM_NSUM_PRODUCT : thm
val NSUM_NSUM_RESTRICT : thm
val NSUM_OFFSET : thm
val NSUM_OFFSET_0 : thm
val NSUM_PAIR : thm
val NSUM_POS_BOUND : thm
val NSUM_POS_LT : thm
val NSUM_POS_LT_ALL : thm
val NSUM_RESTRICT : thm
val NSUM_RESTRICT_SET : thm
val NSUM_RMUL : thm
val NSUM_SING : thm
val NSUM_SING_NUMSEG : thm
val NSUM_SUBSET : thm
val NSUM_SUBSET_SIMPLE : thm
val NSUM_SUPERSET : thm
val NSUM_SUPPORT : thm
val NSUM_SWAP : thm
val NSUM_SWAP_NUMSEG : thm
val NSUM_TRIV_NUMSEG : thm
val NSUM_UNION : thm
val NSUM_UNION_EQ : thm
val NSUM_UNION_LZERO : thm
val NSUM_UNION_NONZERO : thm
val NSUM_UNION_RZERO : thm
val NUMSEG_ADD_SPLIT : thm
val NUMSEG_CLAUSES : thm
val NUMSEG_COMBINE_L : thm
val NUMSEG_COMBINE_R : thm
val NUMSEG_EMPTY : thm
val NUMSEG_LE : thm
val NUMSEG_LREC : thm
val NUMSEG_LT : thm
val NUMSEG_OFFSET_IMAGE : thm
val NUMSEG_REC : thm
val NUMSEG_RREC : thm
val NUMSEG_SING : thm
val POLYNOMIAL_FUNCTION_ADD : thm
val POLYNOMIAL_FUNCTION_CONST : thm
val POLYNOMIAL_FUNCTION_FINITE_ROOTS : thm
val POLYNOMIAL_FUNCTION_ID : thm
val POLYNOMIAL_FUNCTION_INDUCT : thm
val POLYNOMIAL_FUNCTION_LMUL : thm
val POLYNOMIAL_FUNCTION_MUL : thm
val POLYNOMIAL_FUNCTION_NEG : thm
val POLYNOMIAL_FUNCTION_POW : thm
val POLYNOMIAL_FUNCTION_RMUL : thm
val POLYNOMIAL_FUNCTION_SUB : thm
val POLYNOMIAL_FUNCTION_SUM : thm
val POLYNOMIAL_FUNCTION_o : thm
val REAL_ABS_INF_LE : thm
val REAL_ABS_SUP_LE : thm
val REAL_COMPLETE : thm
val REAL_INF_ASCLOSE : thm
val REAL_INF_BOUNDS : thm
val REAL_INF_LE_FINITE : thm
val REAL_INF_LT_FINITE : thm
val REAL_INF_UNIQUE : thm
val REAL_LE_INF : thm
val REAL_LE_INF_FINITE : thm
val REAL_LE_INF_SUBSET : thm
val REAL_LE_SUP : thm
val REAL_LE_SUP_FINITE : thm
val REAL_LT_BETWEEN : thm
val REAL_LT_INF_FINITE : thm
val REAL_LT_SUP_FINITE : thm
val REAL_OF_NUM_SUM : thm
val REAL_OF_NUM_SUM_NUMSEG : thm
val REAL_POLYFUN_EQ_0 : thm
val REAL_POLYFUN_EQ_CONST : thm
val REAL_POLYFUN_FINITE_ROOTS : thm
val REAL_POLYFUN_ROOTBOUND : thm
val REAL_SUB_POLYFUN : thm
val REAL_SUB_POLYFUN_ALT : thm
val REAL_SUB_POW : thm
val REAL_SUB_POW_L1 : thm
val REAL_SUB_POW_R1 : thm
val REAL_SUP_ASCLOSE : thm
val REAL_SUP_BOUNDS : thm
val REAL_SUP_EQ_INF : thm
val REAL_SUP_LE_EQ : thm
val REAL_SUP_LE_FINITE : thm
val REAL_SUP_LE_S : thm
val REAL_SUP_LE_SUBSET : thm
val REAL_SUP_LT_FINITE : thm
val REAL_SUP_UNIQUE : thm
val REAL_WLOG_LT : thm
val SET_PROVE_CASES : thm
val SET_RECURSION_LEMMA : thm
val SIMP_REAL_ARCH : thm
val SUBSET_NUMSEG : thm
val SUBSET_RESTRICT : thm
val SUM_0 : thm
val SUM_ABS : thm
val SUM_ABS_BOUND : thm
val SUM_ABS_LE : thm
val SUM_ABS_NUMSEG : thm
val SUM_ADD : thm
val SUM_ADD_GEN : thm
val SUM_ADD_NUMSEG : thm
val SUM_ADD_SPLIT : thm
val SUM_BIGUNION_NONZERO : thm
val SUM_BIJECTION : thm
val SUM_BOUND : thm
val SUM_BOUND_GEN : thm
val SUM_BOUND_LT : thm
val SUM_BOUND_LT_ALL : thm
val SUM_BOUND_LT_GEN : thm
val SUM_CASES : thm
val SUM_CASES_1 : thm
val SUM_CLAUSES : thm
val SUM_CLAUSES_LEFT : thm
val SUM_CLAUSES_NUMSEG : thm
val SUM_CLAUSES_RIGHT : thm
val SUM_CLOSED : thm
val SUM_COMBINE_L : thm
val SUM_COMBINE_R : thm
val SUM_CONST : thm
val SUM_CONST_NUMSEG : thm
val SUM_DEGENERATE : thm
val SUM_DELETE : thm
val SUM_DELETE_CASES : thm
val SUM_DELTA : thm
val SUM_DIFF : thm
val SUM_DIFFS : thm
val SUM_DIFFS_ALT : thm
val SUM_EQ : thm
val SUM_EQ_0 : thm
val SUM_EQ_0_NUMSEG : thm
val SUM_EQ_GENERAL : thm
val SUM_EQ_GENERAL_INVERSES : thm
val SUM_EQ_NUMSEG : thm
val SUM_EQ_SUPERSET : thm
val SUM_GROUP : thm
val SUM_IMAGE : thm
val SUM_IMAGE_GEN : thm
val SUM_IMAGE_LE : thm
val SUM_IMAGE_NONZERO : thm
val SUM_INCL_EXCL : thm
val SUM_INJECTION : thm
val SUM_LE : thm
val SUM_LE_INCLUDED : thm
val SUM_LE_NUMSEG : thm
val SUM_LMUL : thm
val SUM_LT : thm
val SUM_LT_ALL : thm
val SUM_MULTICOUNT : thm
val SUM_MULTICOUNT_GEN : thm
val SUM_NEG : thm
val SUM_OFFSET : thm
val SUM_OFFSET_0 : thm
val SUM_PAIR : thm
val SUM_PARTIAL_PRE : thm
val SUM_PARTIAL_SUC : thm
val SUM_POS_BOUND : thm
val SUM_POS_EQ_0 : thm
val SUM_POS_EQ_0_NUMSEG : thm
val SUM_POS_LE : thm
val SUM_POS_LE_NUMSEG : thm
val SUM_POS_LT : thm
val SUM_POS_LT_ALL : thm
val SUM_RESTRICT : thm
val SUM_RESTRICT_SET : thm
val SUM_RMUL : thm
val SUM_SING : thm
val SUM_SING_NUMSEG : thm
val SUM_SUB : thm
val SUM_SUBSET : thm
val SUM_SUBSET_SIMPLE : thm
val SUM_SUB_NUMSEG : thm
val SUM_SUM_PRODUCT : thm
val SUM_SUM_RESTRICT : thm
val SUM_SUPERSET : thm
val SUM_SUPPORT : thm
val SUM_SWAP : thm
val SUM_SWAP_NUMSEG : thm
val SUM_TRIV_NUMSEG : thm
val SUM_UNION : thm
val SUM_UNION_EQ : thm
val SUM_UNION_LZERO : thm
val SUM_UNION_NONZERO : thm
val SUM_UNION_RZERO : thm
val SUM_ZERO_EXISTS : thm
val SUP : thm
val SUPPORT_CLAUSES : thm
val SUPPORT_DELTA : thm
val SUPPORT_EMPTY : thm
val SUPPORT_SUBSET : thm
val SUPPORT_SUPPORT : thm
val SUP_EQ : thm
val SUP_FINITE : thm
val SUP_FINITE_LEMMA : thm
val SUP_INSERT_FINITE : thm
val SUP_SING : thm
val SUP_UNION : thm
val SUP_UNIQUE : thm
val SUP_UNIQUE_FINITE : thm
val TH : thm
val TOPOLOGICAL_SORT : thm
val UPPER_BOUND_FINITE_SET_REAL : thm
val real_INFINITE : thm
val sup_alt : thm
val iterate_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cardinal] Parent theory of "iterate"
[util_prob] Parent theory of "iterate"
[FINREC_def] Definition
⊢ (∀f b s a. FINREC f b s a 0 ⇔ (s = ∅) ∧ (a = b)) ∧
∀f b s a n.
FINREC f b s a (SUC n) ⇔
∃x c. x ∈ s ∧ FINREC f b (s DELETE x) c n ∧ (a = f x c)
[ITSET_def] Definition
⊢ ∀f s b.
ITSET f s b =
(@g.
(g ∅ = b) ∧
∀x s.
FINITE s ⇒
(g (x INSERT s) = if x ∈ s then g s else f x (g s))) s
[inf] Definition
⊢ ∀s.
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
[iterate] Definition
⊢ ∀op s f.
iterate op s f =
if FINITE (support op f s) then
ITSET (λx a. op (f x) a) (support op f s) (neutral op)
else neutral op
[monoidal] Definition
⊢ ∀op.
monoidal op ⇔
(∀x y. op x y = op y x) ∧
(∀x y z. op x (op y z) = op (op x y) z) ∧
∀x. op (neutral op) x = x
[neutral] Definition
⊢ ∀op. neutral op = @x. ∀y. (op x y = y) ∧ (op y x = y)
[nsum_def] Definition
⊢ nsum = iterate $+
[numseg] Definition
⊢ ∀m n. m .. n = {x | m ≤ x ∧ x ≤ n}
[polynomial_function] Definition
⊢ ∀p.
polynomial_function p ⇔
∃m c. ∀x. p x = sum (0 .. m) (λi. c i * x pow i)
[sum_def] Definition
⊢ sum = iterate $+
[support] Definition
⊢ ∀op f s. support op f s = {x | x ∈ s ∧ f x ≠ neutral op}
[CARD_BIGUNION] Theorem
⊢ ∀s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t u. t ∈ s ∧ u ∈ s ∧ t ≠ u ⇒ (t ∩ u = ∅)) ⇒
(CARD (BIGUNION s) = nsum s CARD)
[CARD_EQ_NSUM] Theorem
⊢ ∀s. FINITE s ⇒ (CARD s = nsum s (λx. 1))
[CARD_EQ_SUM] Theorem
⊢ ∀s. FINITE s ⇒ (&CARD s = sum s (λx. 1))
[CARD_NUMSEG] Theorem
⊢ ∀m n. CARD (m .. n) = n + 1 − m
[CARD_NUMSEG_1] Theorem
⊢ ∀n. CARD (1 .. n) = n
[CARD_NUMSEG_LEMMA] Theorem
⊢ ∀m d. CARD (m .. m + d) = d + 1
[CARD_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒
(CARD s + CARD t = CARD u)
[CHOOSE_SUBSET] Theorem
⊢ ∀s. FINITE s ⇒ ∀n. n ≤ CARD s ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[CHOOSE_SUBSET_STRONG] Theorem
⊢ ∀n s. (FINITE s ⇒ n ≤ CARD s) ⇒ ∃t. t ⊆ s ∧ t HAS_SIZE n
[DISJOINT_NUMSEG] Theorem
⊢ ∀m n p q.
DISJOINT (m .. n) (p .. q) ⇔ n < p ∨ q < m ∨ n < m ∨ q < p
[FINITE_INDEX_NUMBERS] Theorem
⊢ ∀s.
FINITE s ⇔
∃k f.
(∀i j. i ∈ k ∧ j ∈ k ∧ (f i = f j) ⇒ (i = j)) ∧ FINITE k ∧
(s = IMAGE f k)
[FINITE_INDEX_NUMSEG] Theorem
⊢ ∀s.
FINITE s ⇔
∃f.
(∀i j.
i ∈ 1 .. CARD s ∧ j ∈ 1 .. CARD s ∧ (f i = f j) ⇒
(i = j)) ∧ (s = IMAGE f (1 .. CARD s))
[FINITE_NUMSEG] Theorem
⊢ ∀m n. FINITE (m .. n)
[FINITE_REAL_INTERVAL] Theorem
⊢ (∀a. INFINITE {x | a < x}) ∧ (∀a. INFINITE {x | a ≤ x}) ∧
(∀b. INFINITE {x | x < b}) ∧ (∀b. INFINITE {x | x ≤ b}) ∧
(∀a b. FINITE {x | a < x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a ≤ x ∧ x < b} ⇔ b ≤ a) ∧
(∀a b. FINITE {x | a < x ∧ x ≤ b} ⇔ b ≤ a) ∧
∀a b. FINITE {x | a ≤ x ∧ x ≤ b} ⇔ b ≤ a
[FINITE_RECURSION] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ (f x (f y s) = f y (f x s))) ⇒
(ITSET f ∅ b = b) ∧
∀x s.
FINITE s ⇒
(ITSET f (x INSERT s) b =
if x ∈ s then ITSET f s b else f x (ITSET f s b))
[FINITE_RESTRICT] Theorem
⊢ ∀s P. FINITE s ⇒ FINITE {x | x ∈ s ∧ P x}
[FINITE_SUPPORT] Theorem
⊢ ∀op f s. FINITE s ⇒ FINITE (support op f s)
[FINITE_SUPPORT_DELTA] Theorem
⊢ ∀op f a.
FINITE (support op (λx. if x = a then f x else neutral op) s)
[FINREC_1_LEMMA] Theorem
⊢ ∀f b s a. FINREC f b s a (SUC 0) ⇔ ∃x. (s = {x}) ∧ (a = f x b)
[FINREC_EXISTS_LEMMA] Theorem
⊢ ∀f b s. FINITE s ⇒ ∃a n. FINREC f b s a n
[FINREC_FUN] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ (f x (f y s) = f y (f x s))) ⇒
∃g.
(g ∅ = b) ∧
∀s x. FINITE s ∧ x ∈ s ⇒ (g s = f x (g (s DELETE x)))
[FINREC_FUN_LEMMA] Theorem
⊢ ∀P R.
(∀s. P s ⇒ ∃a n. R s a n) ∧
(∀n1 n2 s a1 a2. R s a1 n1 ∧ R s a2 n2 ⇒ (a1 = a2) ∧ (n1 = n2)) ⇒
∃f. ∀s a. P s ⇒ ((∃n. R s a n) ⇔ (f s = a))
[FINREC_SUC_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ (f x (f y s) = f y (f x s))) ⇒
∀n s z.
FINREC f b s z (SUC n) ⇒
∀x. x ∈ s ⇒ ∃w. FINREC f b (s DELETE x) w n ∧ (z = f x w)
[FINREC_UNIQUE_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ (f x (f y s) = f y (f x s))) ⇒
∀n1 n2 s a1 a2.
FINREC f b s a1 n1 ∧ FINREC f b s a2 n2 ⇒
(a1 = a2) ∧ (n1 = n2)
[FINREC_compute] Theorem
⊢ (∀f b s a. FINREC f b s a 0 ⇔ (s = ∅) ∧ (a = b)) ∧
(∀f b s a n.
FINREC f b s a (NUMERAL (BIT1 n)) ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c (NUMERAL (BIT1 n) − 1) ∧
(a = f x c)) ∧
∀f b s a n.
FINREC f b s a (NUMERAL (BIT2 n)) ⇔
∃x c.
x ∈ s ∧ FINREC f b (s DELETE x) c (NUMERAL (BIT1 n)) ∧
(a = f x c)
[FORALL_IN_GSPEC] Theorem
⊢ (∀P f. (∀z. z ∈ {f x | P x} ⇒ Q z) ⇔ ∀x. P x ⇒ Q (f x)) ∧
(∀P f. (∀z. z ∈ {f x y | P x y} ⇒ Q z) ⇔ ∀x y. P x y ⇒ Q (f x y)) ∧
∀P f.
(∀z. z ∈ {f w x y | P w x y} ⇒ Q z) ⇔
∀w x y. P w x y ⇒ Q (f w x y)
[HAS_SIZE_NUMSEG] Theorem
⊢ ∀m n. (m .. n) HAS_SIZE n + 1 − m
[HAS_SIZE_NUMSEG_1] Theorem
⊢ ∀n. (1 .. n) HAS_SIZE n
[INF] Theorem
⊢ ∀s.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
(∀x. x ∈ s ⇒ inf s ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[INF_EQ] Theorem
⊢ ∀s t.
(∀a. (∀x. x ∈ s ⇒ a ≤ x) ⇔ ∀x. x ∈ t ⇒ a ≤ x) ⇒ (inf s = inf t)
[INF_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ inf s ∈ s ∧ ∀x. x ∈ s ⇒ inf s ≤ x
[INF_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ b ≤ x
[INF_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒
(inf (x INSERT s) = if s = ∅ then x else min x (inf s))
[INF_SING] Theorem
⊢ ∀a. inf {a} = a
[INF_UNIQUE_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ((inf s = a) ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ a ≤ y)
[IN_NUMSEG] Theorem
⊢ ∀m n p. p ∈ m .. n ⇔ m ≤ p ∧ p ≤ n
[IN_NUMSEG_0] Theorem
⊢ ∀m n. m ∈ 0 .. n ⇔ m ≤ n
[IN_SUPPORT] Theorem
⊢ ∀op f x s. x ∈ support op f s ⇔ x ∈ s ∧ f x ≠ neutral op
[ITERATE_BIJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ (p x = y)) ⇒
(iterate op s f = iterate op s (f ∘ p))
[ITERATE_CASES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s P f g.
FINITE s ⇒
(iterate op s (λx. if P x then f x else g x) =
op (iterate op {x | x ∈ s ∧ P x} f)
(iterate op {x | x ∈ s ∧ ¬P x} g))
[ITERATE_CLAUSES] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
FINITE s ⇒
(iterate op (x INSERT s) f =
if x ∈ s then iterate op s f
else op (f x) (iterate op s f))
[ITERATE_CLAUSES_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
(∀f. iterate op ∅ f = neutral op) ∧
∀f x s.
monoidal op ∧ FINITE (support op f s) ⇒
(iterate op (x INSERT s) f =
if x ∈ s then iterate op s f
else op (f x) (iterate op s f))
[ITERATE_CLAUSES_NUMSEG] Theorem
⊢ ∀op.
monoidal op ⇒
(∀m. iterate op (m .. 0) f = if m = 0 then f 0 else neutral op) ∧
∀m n.
iterate op (m .. SUC n) f =
if m ≤ SUC n then op (iterate op (m .. n) f) (f (SUC n))
else iterate op (m .. n) f
[ITERATE_CLOSED] Theorem
⊢ ∀op.
monoidal op ⇒
∀P.
P (neutral op) ∧ (∀x y. P x ∧ P y ⇒ P (op x y)) ⇒
∀f s.
(∀x. x ∈ s ∧ f x ≠ neutral op ⇒ P (f x)) ⇒
P (iterate op s f)
[ITERATE_DELETE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s a.
FINITE s ∧ a ∈ s ⇒
(op (f a) (iterate op (s DELETE a) f) = iterate op s f)
[ITERATE_DELTA] Theorem
⊢ ∀op.
monoidal op ⇒
∀f a s.
iterate op s (λx. if x = a then f x else neutral op) =
if a ∈ s then f a else neutral op
[ITERATE_DIFF] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ t ⊆ s ⇒
(op (iterate op (s DIFF t) f) (iterate op t f) =
iterate op s f)
[ITERATE_DIFF_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ support op f t ⊆ support op f s ⇒
(op (iterate op (s DIFF t) f) (iterate op t f) =
iterate op s f)
[ITERATE_EQ] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
(∀x. x ∈ s ⇒ (f x = g x)) ⇒
(iterate op s f = iterate op s g)
[ITERATE_EQ_GENERAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ (h x = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (g (h x) = f x)) ⇒
(iterate op s f = iterate op t g)
[ITERATE_EQ_GENERAL_INVERSES] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ (h (k y) = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (k (h x) = x) ∧ (g (h x) = f x)) ⇒
(iterate op s f = iterate op t g)
[ITERATE_EQ_NEUTRAL] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s.
(∀x. x ∈ s ⇒ (f x = neutral op)) ⇒
(iterate op s f = neutral op)
[ITERATE_EXPAND_CASES] Theorem
⊢ ∀op f s.
iterate op s f =
if FINITE (support op f s) then iterate op (support op f s) f
else neutral op
[ITERATE_IMAGE] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇒
(iterate op (IMAGE f s) g = iterate op s (g ∘ f))
[ITERATE_IMAGE_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀g f s.
FINITE s ∧
(∀x y.
x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ (f x = f y) ⇒
(g (f x) = neutral op)) ⇒
(iterate op (IMAGE f s) g = iterate op s (g ∘ f))
[ITERATE_INCL_EXCL] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t f.
FINITE s ∧ FINITE t ⇒
(op (iterate op s f) (iterate op t f) =
op (iterate op (s ∪ t) f) (iterate op (s ∩ t) f))
[ITERATE_INJECTION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ (p x = p y) ⇒ (x = y)) ⇒
(iterate op s (f ∘ p) = iterate op s f)
[ITERATE_ITERATE_PRODUCT] Theorem
⊢ ∀op.
monoidal op ⇒
∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
(iterate op s (λi. iterate op (t i) (x i)) =
iterate op {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j))
[ITERATE_OP] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE s ⇒
(iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g))
[ITERATE_OP_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f g s.
FINITE (support op f s) ∧ FINITE (support op g s) ⇒
(iterate op s (λx. op (f x) (g x)) =
op (iterate op s f) (iterate op s g))
[ITERATE_PAIR] Theorem
⊢ ∀op.
monoidal op ⇒
∀f m n.
iterate op (2 * m .. 2 * n + 1) f =
iterate op (m .. n) (λi. op (f (2 * i)) (f (2 * i + 1)))
[ITERATE_RELATED] Theorem
⊢ ∀op.
monoidal op ⇒
∀R.
R (neutral op) (neutral op) ∧
(∀x1 y1 x2 y2. R x1 x2 ∧ R y1 y2 ⇒ R (op x1 y1) (op x2 y2)) ⇒
∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ R (f x) (g x)) ⇒
R (iterate op s f) (iterate op s g)
[ITERATE_SING] Theorem
⊢ ∀op. monoidal op ⇒ ∀f x. iterate op {x} f = f x
[ITERATE_SUPERSET] Theorem
⊢ ∀op.
monoidal op ⇒
∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = neutral op)) ⇒
(iterate op v f = iterate op u f)
[ITERATE_SUPPORT] Theorem
⊢ ∀op f s. iterate op (support op f s) f = iterate op s f
[ITERATE_UNION] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
(iterate op (s ∪ t) f =
op (iterate op s f) (iterate op t f))
[ITERATE_UNION_GEN] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE (support op f s) ∧ FINITE (support op f t) ∧
DISJOINT (support op f s) (support op f t) ⇒
(iterate op (s ∪ t) f =
op (iterate op s f) (iterate op t f))
[ITERATE_UNION_NONZERO] Theorem
⊢ ∀op.
monoidal op ⇒
∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ (f x = neutral op)) ⇒
(iterate op (s ∪ t) f =
op (iterate op s f) (iterate op t f))
[LOWER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x
[MOD_NSUM_MOD] Theorem
⊢ ∀f n s.
FINITE s ∧ n ≠ 0 ⇒
(nsum s f MOD n = nsum s (λi. f i MOD n) MOD n)
[MOD_NSUM_MOD_NUMSEG] Theorem
⊢ ∀f a b n.
n ≠ 0 ⇒
(nsum (a .. b) f MOD n = nsum (a .. b) (λi. f i MOD n) MOD n)
[MONOIDAL_AC] Theorem
⊢ ∀op.
monoidal op ⇒
(∀a. op (neutral op) a = a) ∧ (∀a. op a (neutral op) = a) ∧
(∀a b. op a b = op b a) ∧
(∀a b c. op (op a b) c = op a (op b c)) ∧
∀a b c. op a (op b c) = op b (op a c)
[MONOIDAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_MUL] Theorem
⊢ monoidal $*
[MONOIDAL_REAL_ADD] Theorem
⊢ monoidal $+
[MONOIDAL_REAL_MUL] Theorem
⊢ monoidal $*
[NEUTRAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_MUL] Theorem
⊢ neutral $* = 1
[NEUTRAL_REAL_ADD] Theorem
⊢ neutral $+ = 0
[NEUTRAL_REAL_MUL] Theorem
⊢ neutral $* = 1
[NSUM_0] Theorem
⊢ ∀s. nsum s (λn. 0) = 0
[NSUM_ADD] Theorem
⊢ ∀f g s. FINITE s ⇒ (nsum s (λx. f x + g x) = nsum s f + nsum s g)
[NSUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
(nsum s (λx. f x + g x) = nsum s f + nsum s g)
[NSUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
nsum (m .. n) (λi. f i + g i) =
nsum (m .. n) f + nsum (m .. n) g
[NSUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
(nsum (m .. n + p) f =
nsum (m .. n) f + nsum (n + 1 .. n + p) f)
[NSUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x.
t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ (f x = 0)) ⇒
(nsum (BIGUNION s) f = nsum s (λt. nsum t f))
[NSUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ (p x = y)) ⇒
(nsum s f = nsum s (f ∘ p))
[NSUM_BOUND] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ nsum s f ≤ CARD s * b
[NSUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b DIV CARD s) ⇒
nsum s f ≤ b
[NSUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
nsum s f < CARD s * b
[NSUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒
nsum s f < CARD s * b
[NSUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b DIV CARD s) ⇒
nsum s f < b
[NSUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
(nsum s (λx. if P x then f x else g x) =
nsum {x | x ∈ s ∧ P x} f + nsum {x | x ∈ s ∧ ¬P x} g)
[NSUM_CLAUSES] Theorem
⊢ (∀f. nsum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
(nsum (x INSERT s) f =
if x ∈ s then nsum s f else f x + nsum s f)
[NSUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ (nsum (m .. n) f = f m + nsum (m + 1 .. n) f)
[NSUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. nsum (m .. 0) f = if m = 0 then f 0 else 0) ∧
∀m n.
nsum (m .. SUC n) f =
if m ≤ SUC n then nsum (m .. n) f + f (SUC n)
else nsum (m .. n) f
[NSUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n.
0 < n ∧ m ≤ n ⇒ (nsum (m .. n) f = nsum (m .. n − 1) f + f n)
[NSUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (nsum s f)
[NSUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ (nsum s (λn. c) = CARD s * c)
[NSUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. nsum (m .. n) (λn. c) = (n + 1 − m) * c
[NSUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ (nsum s f = 0)
[NSUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (f a + nsum (s DELETE a) f = nsum s f)
[NSUM_DELTA] Theorem
⊢ ∀s a. nsum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[NSUM_DIFF] Theorem
⊢ ∀f s t.
FINITE s ∧ t ⊆ s ⇒ (nsum (s DIFF t) f = nsum s f − nsum t f)
[NSUM_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (nsum s f = nsum s g)
[NSUM_EQ_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (nsum s f = 0)
[NSUM_EQ_0_IFF] Theorem
⊢ ∀s. FINITE s ⇒ ((nsum s f = 0) ⇔ ∀x. x ∈ s ⇒ (f x = 0))
[NSUM_EQ_0_IFF_NUMSEG] Theorem
⊢ ∀f m n. (nsum (m .. n) f = 0) ⇔ ∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)
[NSUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)) ⇒ (nsum (m .. n) f = 0)
[NSUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ (h x = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (g (h x) = f x)) ⇒
(nsum s f = nsum t g)
[NSUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ (h (k y) = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (k (h x) = x) ∧ (g (h x) = f x)) ⇒
(nsum s f = nsum t g)
[NSUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒
(nsum (m .. n) f = nsum (m .. n) g)
[NSUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ (f x = g x)) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ (f x = 0)) ⇒
(nsum s f = nsum t g)
[NSUM_GROUP] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
(nsum t (λy. nsum {x | x ∈ s ∧ (f x = y)} g) = nsum s g)
[NSUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇒
(nsum (IMAGE f s) g = nsum s (g ∘ f))
[NSUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
(nsum s g =
nsum (IMAGE f s) (λy. nsum {x | x ∈ s ∧ (f x = y)} g))
[NSUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ (i x = i y) ⇒ (d (i x) = 0)) ⇒
(nsum (IMAGE i s) d = nsum s (d ∘ i))
[NSUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
(nsum s f + nsum t f = nsum (s ∪ t) f + nsum (s ∩ t) f)
[NSUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ (p x = p y) ⇒ (x = y)) ⇒
(nsum s (f ∘ p) = nsum s f)
[NSUM_LE] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ nsum s f ≤ nsum s g
[NSUM_LE_GEN] Theorem
⊢ ∀f g s.
(∀x. x ∈ s ⇒ f x ≤ g x) ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
nsum s f ≤ nsum s g
[NSUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒
nsum (m .. n) f ≤ nsum (m .. n) g
[NSUM_LMUL] Theorem
⊢ ∀f c s. nsum s (λx. c * f x) = c * nsum s f
[NSUM_LT] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
nsum s f < nsum s g
[NSUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒
nsum s f < nsum s g
[NSUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k)) ⇒
(nsum s (λi. CARD {j | j ∈ t ∧ R i j}) = k * CARD t)
[NSUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k j)) ⇒
(nsum s (λi. CARD {j | j ∈ t ∧ R i j}) = nsum t (λi. k i))
[NSUM_NSUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
(nsum s (λi. nsum (t i) (x i)) =
nsum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j))
[NSUM_NSUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
(nsum s (λx. nsum {y | y ∈ t ∧ R x y} (λy. f x y)) =
nsum t (λy. nsum {x | x ∈ s ∧ R x y} (λx. f x y)))
[NSUM_OFFSET] Theorem
⊢ ∀p f m n. nsum (m + p .. n + p) f = nsum (m .. n) (λi. f (i + p))
[NSUM_OFFSET_0] Theorem
⊢ ∀f m n.
m ≤ n ⇒ (nsum (m .. n) f = nsum (0 .. n − m) (λi. f (i + m)))
[NSUM_PAIR] Theorem
⊢ ∀f m n.
nsum (2 * m .. 2 * n + 1) f =
nsum (m .. n) (λi. f (2 * i) + f (2 * i + 1))
[NSUM_POS_BOUND] Theorem
⊢ ∀f b s. FINITE s ∧ nsum s f ≤ b ⇒ ∀x. x ∈ s ⇒ f x ≤ b
[NSUM_POS_LT] Theorem
⊢ ∀f s. FINITE s ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒ 0 < nsum s f
[NSUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < nsum s f
[NSUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ (nsum s (λx. if x ∈ s then f x else 0) = nsum s f)
[NSUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
nsum {x | x ∈ s ∧ P x} f = nsum s (λx. if P x then f x else 0)
[NSUM_RMUL] Theorem
⊢ ∀f c s. nsum s (λx. f x * c) = nsum s f * c
[NSUM_SING] Theorem
⊢ ∀f x. nsum {x} f = f x
[NSUM_SING_NUMSEG] Theorem
⊢ ∀f n. nsum (n .. n) f = f n
[NSUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ (f x = 0)) ⇒
nsum u f ≤ nsum v f
[NSUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f. FINITE v ∧ u ⊆ v ⇒ nsum u f ≤ nsum v f
[NSUM_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (nsum v f = nsum u f)
[NSUM_SUPPORT] Theorem
⊢ ∀f s. nsum (support $+ f s) f = nsum s f
[NSUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
(nsum s (λi. nsum t (f i)) = nsum t (λj. nsum s (λi. f i j)))
[NSUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
nsum (a .. b) (λi. nsum (c .. d) (f i)) =
nsum (c .. d) (λj. nsum (a .. b) (λi. f i j))
[NSUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ (nsum (m .. n) f = 0)
[NSUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
(nsum (s ∪ t) f = nsum s f + nsum t f)
[NSUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒
(nsum s f + nsum t f = nsum u f)
[NSUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ (f x = 0)) ⇒
(nsum (u ∪ v) f = nsum v f)
[NSUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ (f x = 0)) ⇒
(nsum (s ∪ t) f = nsum s f + nsum t f)
[NSUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒
(nsum (u ∪ v) f = nsum u f)
[NUMSEG_ADD_SPLIT] Theorem
⊢ ∀m n p. m ≤ n + 1 ⇒ (m .. n + p = (m .. n) ∪ (n + 1 .. n + p))
[NUMSEG_CLAUSES] Theorem
⊢ (∀m. m .. 0 = if m = 0 then {0} else ∅) ∧
∀m n.
m .. SUC n =
if m ≤ SUC n then SUC n INSERT (m .. n) else m .. n
[NUMSEG_COMBINE_L] Theorem
⊢ ∀m p n. m ≤ p ∧ p ≤ n + 1 ⇒ ((m .. p − 1) ∪ (p .. n) = m .. n)
[NUMSEG_COMBINE_R] Theorem
⊢ ∀m p n. m ≤ p + 1 ∧ p ≤ n ⇒ ((m .. p) ∪ (p + 1 .. n) = m .. n)
[NUMSEG_EMPTY] Theorem
⊢ ∀m n. (m .. n = ∅) ⇔ n < m
[NUMSEG_LE] Theorem
⊢ ∀n. {x | x ≤ n} = 0 .. n
[NUMSEG_LREC] Theorem
⊢ ∀m n. m ≤ n ⇒ (m INSERT (m + 1 .. n) = m .. n)
[NUMSEG_LT] Theorem
⊢ ∀n. {x | x < n} = if n = 0 then ∅ else 0 .. n − 1
[NUMSEG_OFFSET_IMAGE] Theorem
⊢ ∀m n p. m + p .. n + p = IMAGE (λi. i + p) (m .. n)
[NUMSEG_REC] Theorem
⊢ ∀m n. m ≤ SUC n ⇒ (m .. SUC n = SUC n INSERT (m .. n))
[NUMSEG_RREC] Theorem
⊢ ∀m n. m ≤ n ⇒ (n INSERT (m .. n − 1) = m .. n)
[NUMSEG_SING] Theorem
⊢ ∀n. n .. n = {n}
[POLYNOMIAL_FUNCTION_ADD] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x + q x)
[POLYNOMIAL_FUNCTION_CONST] Theorem
⊢ ∀c. polynomial_function (λx. c)
[POLYNOMIAL_FUNCTION_FINITE_ROOTS] Theorem
⊢ ∀p a. polynomial_function p ⇒ (FINITE {x | p x = a} ⇔ ¬∀x. p x = a)
[POLYNOMIAL_FUNCTION_ID] Theorem
⊢ polynomial_function (λx. x)
[POLYNOMIAL_FUNCTION_INDUCT] Theorem
⊢ ∀P.
P (λx. x) ∧ (∀c. P (λx. c)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x + q x)) ∧
(∀p q. P p ∧ P q ⇒ P (λx. p x * q x)) ⇒
∀p. polynomial_function p ⇒ P p
[POLYNOMIAL_FUNCTION_LMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. c * p x)
[POLYNOMIAL_FUNCTION_MUL] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x * q x)
[POLYNOMIAL_FUNCTION_NEG] Theorem
⊢ ∀p. polynomial_function (λx. -p x) ⇔ polynomial_function p
[POLYNOMIAL_FUNCTION_POW] Theorem
⊢ ∀p n. polynomial_function p ⇒ polynomial_function (λx. p x pow n)
[POLYNOMIAL_FUNCTION_RMUL] Theorem
⊢ ∀p c. polynomial_function p ⇒ polynomial_function (λx. p x * c)
[POLYNOMIAL_FUNCTION_SUB] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (λx. p x − q x)
[POLYNOMIAL_FUNCTION_SUM] Theorem
⊢ ∀s p.
FINITE s ∧ (∀i. i ∈ s ⇒ polynomial_function (λx. p x i)) ⇒
polynomial_function (λx. sum s (p x))
[POLYNOMIAL_FUNCTION_o] Theorem
⊢ ∀p q.
polynomial_function p ∧ polynomial_function q ⇒
polynomial_function (p ∘ q)
[REAL_ABS_INF_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (inf s) ≤ a
[REAL_ABS_SUP_LE] Theorem
⊢ ∀s a. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs x ≤ a) ⇒ abs (sup s) ≤ a
[REAL_COMPLETE] Theorem
⊢ ∀P.
(∃x. P x) ∧ (∃M. ∀x. P x ⇒ x ≤ M) ⇒
∃M. (∀x. P x ⇒ x ≤ M) ∧ ∀M'. (∀x. P x ⇒ x ≤ M') ⇒ M ≤ M'
[REAL_INF_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (inf s − l) ≤ e
[REAL_INF_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ inf s ∧ inf s ≤ b
[REAL_INF_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s ≤ a ⇔ ∃x. x ∈ s ∧ x ≤ a)
[REAL_INF_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (inf s < a ⇔ ∃x. x ∈ s ∧ x < a)
[REAL_INF_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ b ≤ x) ∧ (∀b'. b < b' ⇒ ∃x. x ∈ s ∧ x < b') ⇒
(inf s = b)
[REAL_LE_INF] Theorem
⊢ ∀b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ inf s
[REAL_LE_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ inf s ⇔ ∀x. x ∈ s ⇒ a ≤ x)
[REAL_LE_INF_SUBSET] Theorem
⊢ ∀s t. t ≠ ∅ ∧ t ⊆ s ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒ inf s ≤ inf t
[REAL_LE_SUP] Theorem
⊢ ∀s a b y. y ∈ s ∧ a ≤ y ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ sup s
[REAL_LE_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a ≤ sup s ⇔ ∃x. x ∈ s ∧ a ≤ x)
[REAL_LT_BETWEEN] Theorem
⊢ ∀a b. a < b ⇔ ∃x. a < x ∧ x < b
[REAL_LT_INF_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < inf s ⇔ ∀x. x ∈ s ⇒ a < x)
[REAL_LT_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)
[REAL_OF_NUM_SUM] Theorem
⊢ ∀f s. FINITE s ⇒ (&nsum s f = sum s (λx. &f x))
[REAL_OF_NUM_SUM_NUMSEG] Theorem
⊢ ∀f m n. &nsum (m .. n) f = sum (m .. n) (λi. &f i)
[REAL_POLYFUN_EQ_0] Theorem
⊢ ∀n c.
(∀x. sum (0 .. n) (λi. c i * x pow i) = 0) ⇔
∀i. i ∈ 0 .. n ⇒ (c i = 0)
[REAL_POLYFUN_EQ_CONST] Theorem
⊢ ∀n c k.
(∀x. sum (0 .. n) (λi. c i * x pow i) = k) ⇔
(c 0 = k) ∧ ∀i. i ∈ 1 .. n ⇒ (c i = 0)
[REAL_POLYFUN_FINITE_ROOTS] Theorem
⊢ ∀n c.
FINITE {x | sum (0 .. n) (λi. c i * x pow i) = 0} ⇔
∃i. i ∈ 0 .. n ∧ c i ≠ 0
[REAL_POLYFUN_ROOTBOUND] Theorem
⊢ ∀n c.
¬(∀i. i ∈ 0 .. n ⇒ (c i = 0)) ⇒
FINITE {x | sum (0 .. n) (λi. c i * x pow i) = 0} ∧
CARD {x | sum (0 .. n) (λi. c i * x pow i) = 0} ≤ n
[REAL_SUB_POLYFUN] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
(sum (0 .. n) (λi. a i * x pow i) −
sum (0 .. n) (λi. a i * y pow i) =
(x − y) *
sum (0 .. n − 1)
(λj.
sum (j + 1 .. n) (λi. a i * y pow (i − j − 1)) *
x pow j))
[REAL_SUB_POLYFUN_ALT] Theorem
⊢ ∀a x y n.
1 ≤ n ⇒
(sum (0 .. n) (λi. a i * x pow i) −
sum (0 .. n) (λi. a i * y pow i) =
(x − y) *
sum (0 .. n − 1)
(λj.
sum (0 .. n − j − 1) (λk. a (j + k + 1) * y pow k) *
x pow j))
[REAL_SUB_POW] Theorem
⊢ ∀x y n.
1 ≤ n ⇒
(x pow n − y pow n =
(x − y) * sum (0 .. n − 1) (λi. x pow i * y pow (n − 1 − i)))
[REAL_SUB_POW_L1] Theorem
⊢ ∀x n.
1 ≤ n ⇒
(1 − x pow n = (1 − x) * sum (0 .. n − 1) (λi. x pow i))
[REAL_SUB_POW_R1] Theorem
⊢ ∀x n.
1 ≤ n ⇒
(x pow n − 1 = (x − 1) * sum (0 .. n − 1) (λi. x pow i))
[REAL_SUP_ASCLOSE] Theorem
⊢ ∀s l e. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ abs (x − l) ≤ e) ⇒ abs (sup s − l) ≤ e
[REAL_SUP_BOUNDS] Theorem
⊢ ∀s a b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ a ≤ x ∧ x ≤ b) ⇒ a ≤ sup s ∧ sup s ≤ b
[REAL_SUP_EQ_INF] Theorem
⊢ ∀s.
s ≠ ∅ ∧ (∃B. ∀x. x ∈ s ⇒ abs x ≤ B) ⇒
((sup s = inf s) ⇔ ∃a. s = {a})
[REAL_SUP_LE_EQ] Theorem
⊢ ∀s y.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
(sup s ≤ y ⇔ ∀x. x ∈ s ⇒ x ≤ y)
[REAL_SUP_LE_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s ≤ a ⇔ ∀x. x ∈ s ⇒ x ≤ a)
[REAL_SUP_LE_S] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[REAL_SUP_LE_SUBSET] Theorem
⊢ ∀s t. s ≠ ∅ ∧ s ⊆ t ∧ (∃b. ∀x. x ∈ t ⇒ x ≤ b) ⇒ sup s ≤ sup t
[REAL_SUP_LT_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (sup s < a ⇔ ∀x. x ∈ s ⇒ x < a)
[REAL_SUP_UNIQUE] Theorem
⊢ ∀s b.
(∀x. x ∈ s ⇒ x ≤ b) ∧ (∀b'. b' < b ⇒ ∃x. x ∈ s ∧ b' < x) ⇒
(sup s = b)
[REAL_WLOG_LT] Theorem
⊢ (∀x. P x x) ∧ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x < y ⇒ P x y) ⇒
∀x y. P x y
[SET_PROVE_CASES] Theorem
⊢ ∀P. P ∅ ∧ (∀a s. a ∉ s ⇒ P (a INSERT s)) ⇒ ∀s. P s
[SET_RECURSION_LEMMA] Theorem
⊢ ∀f b.
(∀x y s. x ≠ y ⇒ (f x (f y s) = f y (f x s))) ⇒
∃g.
(g ∅ = b) ∧
∀x s.
FINITE s ⇒
(g (x INSERT s) = if x ∈ s then g s else f x (g s))
[SIMP_REAL_ARCH] Theorem
⊢ ∀x. ∃n. x ≤ &n
[SUBSET_NUMSEG] Theorem
⊢ ∀m n p q. (m .. n) ⊆ (p .. q) ⇔ n < m ∨ p ≤ m ∧ n ≤ q
[SUBSET_RESTRICT] Theorem
⊢ ∀s P. {x | x ∈ s ∧ P x} ⊆ s
[SUM_0] Theorem
⊢ ∀s. sum s (λn. 0) = 0
[SUM_ABS] Theorem
⊢ ∀f s. FINITE s ⇒ abs (sum s f) ≤ sum s (λx. abs (f x))
[SUM_ABS_BOUND] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ b) ⇒
abs (sum s f) ≤ &CARD s * b
[SUM_ABS_LE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ abs (f x) ≤ g x) ⇒
abs (sum s f) ≤ sum s g
[SUM_ABS_NUMSEG] Theorem
⊢ ∀f m n. abs (sum (m .. n) f) ≤ sum (m .. n) (λi. abs (f i))
[SUM_ADD] Theorem
⊢ ∀f g s. FINITE s ⇒ (sum s (λx. f x + g x) = sum s f + sum s g)
[SUM_ADD_GEN] Theorem
⊢ ∀f g s.
FINITE {x | x ∈ s ∧ f x ≠ 0} ∧ FINITE {x | x ∈ s ∧ g x ≠ 0} ⇒
(sum s (λx. f x + g x) = sum s f + sum s g)
[SUM_ADD_NUMSEG] Theorem
⊢ ∀f g m n.
sum (m .. n) (λi. f i + g i) = sum (m .. n) f + sum (m .. n) g
[SUM_ADD_SPLIT] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ⇒
(sum (m .. n + p) f = sum (m .. n) f + sum (n + 1 .. n + p) f)
[SUM_BIGUNION_NONZERO] Theorem
⊢ ∀f s.
FINITE s ∧ (∀t. t ∈ s ⇒ FINITE t) ∧
(∀t1 t2 x.
t1 ∈ s ∧ t2 ∈ s ∧ t1 ≠ t2 ∧ x ∈ t1 ∧ x ∈ t2 ⇒ (f x = 0)) ⇒
(sum (BIGUNION s) f = sum s (λt. sum t f))
[SUM_BIJECTION] Theorem
⊢ ∀f p s.
(∀x. x ∈ s ⇒ p x ∈ s) ∧ (∀y. y ∈ s ⇒ ∃!x. x ∈ s ∧ (p x = y)) ⇒
(sum s f = sum s (f ∘ p))
[SUM_BOUND] Theorem
⊢ ∀s f b. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ⇒ sum s f ≤ &CARD s * b
[SUM_BOUND_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x ≤ b / &CARD s) ⇒
sum s f ≤ b
[SUM_BOUND_LT] Theorem
⊢ ∀s f b.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ b) ∧ (∃x. x ∈ s ∧ f x < b) ⇒
sum s f < &CARD s * b
[SUM_BOUND_LT_ALL] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b) ⇒
sum s f < &CARD s * b
[SUM_BOUND_LT_GEN] Theorem
⊢ ∀s f b.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < b / &CARD s) ⇒
sum s f < b
[SUM_CASES] Theorem
⊢ ∀s P f g.
FINITE s ⇒
(sum s (λx. if P x then f x else g x) =
sum {x | x ∈ s ∧ P x} f + sum {x | x ∈ s ∧ ¬P x} g)
[SUM_CASES_1] Theorem
⊢ ∀s a.
FINITE s ∧ a ∈ s ⇒
(sum s (λx. if x = a then y else f x) = sum s f + (y − f a))
[SUM_CLAUSES] Theorem
⊢ (∀f. sum ∅ f = 0) ∧
∀x f s.
FINITE s ⇒
(sum (x INSERT s) f = if x ∈ s then sum s f else f x + sum s f)
[SUM_CLAUSES_LEFT] Theorem
⊢ ∀f m n. m ≤ n ⇒ (sum (m .. n) f = f m + sum (m + 1 .. n) f)
[SUM_CLAUSES_NUMSEG] Theorem
⊢ (∀m. sum (m .. 0) f = if m = 0 then f 0 else 0) ∧
∀m n.
sum (m .. SUC n) f =
if m ≤ SUC n then sum (m .. n) f + f (SUC n)
else sum (m .. n) f
[SUM_CLAUSES_RIGHT] Theorem
⊢ ∀f m n. 0 < n ∧ m ≤ n ⇒ (sum (m .. n) f = sum (m .. n − 1) f + f n)
[SUM_CLOSED] Theorem
⊢ ∀P f s.
P 0 ∧ (∀x y. P x ∧ P y ⇒ P (x + y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
P (sum s f)
[SUM_COMBINE_L] Theorem
⊢ ∀f m n p.
0 < n ∧ m ≤ n ∧ n ≤ p + 1 ⇒
(sum (m .. n − 1) f + sum (n .. p) f = sum (m .. p) f)
[SUM_COMBINE_R] Theorem
⊢ ∀f m n p.
m ≤ n + 1 ∧ n ≤ p ⇒
(sum (m .. n) f + sum (n + 1 .. p) f = sum (m .. p) f)
[SUM_CONST] Theorem
⊢ ∀c s. FINITE s ⇒ (sum s (λn. c) = &CARD s * c)
[SUM_CONST_NUMSEG] Theorem
⊢ ∀c m n. sum (m .. n) (λn. c) = &(n + 1 − m) * c
[SUM_DEGENERATE] Theorem
⊢ ∀f s. INFINITE {x | x ∈ s ∧ f x ≠ 0} ⇒ (sum s f = 0)
[SUM_DELETE] Theorem
⊢ ∀f s a. FINITE s ∧ a ∈ s ⇒ (sum (s DELETE a) f = sum s f − f a)
[SUM_DELETE_CASES] Theorem
⊢ ∀f s a.
FINITE s ⇒
(sum (s DELETE a) f = if a ∈ s then sum s f − f a else sum s f)
[SUM_DELTA] Theorem
⊢ ∀s a. sum s (λx. if x = a then b else 0) = if a ∈ s then b else 0
[SUM_DIFF] Theorem
⊢ ∀f s t. FINITE s ∧ t ⊆ s ⇒ (sum (s DIFF t) f = sum s f − sum t f)
[SUM_DIFFS] Theorem
⊢ ∀m n.
sum (m .. n) (λk. f k − f (k + 1)) =
if m ≤ n then f m − f (n + 1) else 0
[SUM_DIFFS_ALT] Theorem
⊢ ∀m n.
sum (m .. n) (λk. f (k + 1) − f k) =
if m ≤ n then f (n + 1) − f m else 0
[SUM_EQ] Theorem
⊢ ∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (sum s f = sum s g)
[SUM_EQ_0] Theorem
⊢ ∀f s. (∀x. x ∈ s ⇒ (f x = 0)) ⇒ (sum s f = 0)
[SUM_EQ_0_NUMSEG] Theorem
⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ (f i = 0)) ⇒ (sum (m .. n) f = 0)
[SUM_EQ_GENERAL] Theorem
⊢ ∀s t f g h.
(∀y. y ∈ t ⇒ ∃!x. x ∈ s ∧ (h x = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (g (h x) = f x)) ⇒
(sum s f = sum t g)
[SUM_EQ_GENERAL_INVERSES] Theorem
⊢ ∀s t f g h k.
(∀y. y ∈ t ⇒ k y ∈ s ∧ (h (k y) = y)) ∧
(∀x. x ∈ s ⇒ h x ∈ t ∧ (k (h x) = x) ∧ (g (h x) = f x)) ⇒
(sum s f = sum t g)
[SUM_EQ_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ (f i = g i)) ⇒
(sum (m .. n) f = sum (m .. n) g)
[SUM_EQ_SUPERSET] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ s ∧ (∀x. x ∈ t ⇒ (f x = g x)) ∧
(∀x. x ∈ s ∧ x ∉ t ⇒ (f x = 0)) ⇒
(sum s f = sum t g)
[SUM_GROUP] Theorem
⊢ ∀f g s t.
FINITE s ∧ IMAGE f s ⊆ t ⇒
(sum t (λy. sum {x | x ∈ s ∧ (f x = y)} g) = sum s g)
[SUM_IMAGE] Theorem
⊢ ∀f g s.
(∀x y. x ∈ s ∧ y ∈ s ∧ (f x = f y) ⇒ (x = y)) ⇒
(sum (IMAGE f s) g = sum s (g ∘ f))
[SUM_IMAGE_GEN] Theorem
⊢ ∀f g s.
FINITE s ⇒
(sum s g = sum (IMAGE f s) (λy. sum {x | x ∈ s ∧ (f x = y)} g))
[SUM_IMAGE_LE] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ g (f x)) ⇒
sum (IMAGE f s) g ≤ sum s (g ∘ f)
[SUM_IMAGE_NONZERO] Theorem
⊢ ∀d i s.
FINITE s ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ x ≠ y ∧ (i x = i y) ⇒ (d (i x) = 0)) ⇒
(sum (IMAGE i s) d = sum s (d ∘ i))
[SUM_INCL_EXCL] Theorem
⊢ ∀s t f.
FINITE s ∧ FINITE t ⇒
(sum s f + sum t f = sum (s ∪ t) f + sum (s ∩ t) f)
[SUM_INJECTION] Theorem
⊢ ∀f p s.
FINITE s ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
(∀x y. x ∈ s ∧ y ∈ s ∧ (p x = p y) ⇒ (x = y)) ⇒
(sum s (f ∘ p) = sum s f)
[SUM_LE] Theorem
⊢ ∀f g s. FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ⇒ sum s f ≤ sum s g
[SUM_LE_INCLUDED] Theorem
⊢ ∀f g s t i.
FINITE s ∧ FINITE t ∧ (∀y. y ∈ t ⇒ 0 ≤ g y) ∧
(∀x. x ∈ s ⇒ ∃y. y ∈ t ∧ (i y = x) ∧ f x ≤ g y) ⇒
sum s f ≤ sum t g
[SUM_LE_NUMSEG] Theorem
⊢ ∀f g m n.
(∀i. m ≤ i ∧ i ≤ n ⇒ f i ≤ g i) ⇒
sum (m .. n) f ≤ sum (m .. n) g
[SUM_LMUL] Theorem
⊢ ∀f c s. sum s (λx. c * f x) = c * sum s f
[SUM_LT] Theorem
⊢ ∀f g s.
FINITE s ∧ (∀x. x ∈ s ⇒ f x ≤ g x) ∧ (∃x. x ∈ s ∧ f x < g x) ⇒
sum s f < sum s g
[SUM_LT_ALL] Theorem
⊢ ∀f g s.
FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ f x < g x) ⇒ sum s f < sum s g
[SUM_MULTICOUNT] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k)) ⇒
(sum s (λi. &CARD {j | j ∈ t ∧ R i j}) = &(k * CARD t))
[SUM_MULTICOUNT_GEN] Theorem
⊢ ∀R s t k.
FINITE s ∧ FINITE t ∧
(∀j. j ∈ t ⇒ (CARD {i | i ∈ s ∧ R i j} = k j)) ⇒
(sum s (λi. &CARD {j | j ∈ t ∧ R i j}) = sum t (λi. &k i))
[SUM_NEG] Theorem
⊢ ∀f s. sum s (λx. -f x) = -sum s f
[SUM_OFFSET] Theorem
⊢ ∀p f m n. sum (m + p .. n + p) f = sum (m .. n) (λi. f (i + p))
[SUM_OFFSET_0] Theorem
⊢ ∀f m n. m ≤ n ⇒ (sum (m .. n) f = sum (0 .. n − m) (λi. f (i + m)))
[SUM_PAIR] Theorem
⊢ ∀f m n.
sum (2 * m .. 2 * n + 1) f =
sum (m .. n) (λi. f (2 * i) + f (2 * i + 1))
[SUM_PARTIAL_PRE] Theorem
⊢ ∀f g m n.
sum (m .. n) (λk. f k * (g k − g (k − 1))) =
if m ≤ n then
f (n + 1) * g n − f m * g (m − 1) −
sum (m .. n) (λk. g k * (f (k + 1) − f k))
else 0
[SUM_PARTIAL_SUC] Theorem
⊢ ∀f g m n.
sum (m .. n) (λk. f k * (g (k + 1) − g k)) =
if m ≤ n then
f (n + 1) * g (n + 1) − f m * g m −
sum (m .. n) (λk. g (k + 1) * (f (k + 1) − f k))
else 0
[SUM_POS_BOUND] Theorem
⊢ ∀f b s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ sum s f ≤ b ⇒
∀x. x ∈ s ⇒ f x ≤ b
[SUM_POS_EQ_0] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (sum s f = 0) ⇒
∀x. x ∈ s ⇒ (f x = 0)
[SUM_POS_EQ_0_NUMSEG] Theorem
⊢ ∀f m n.
(∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ∧ (sum (m .. n) f = 0) ⇒
∀p. m ≤ p ∧ p ≤ n ⇒ (f p = 0)
[SUM_POS_LE] Theorem
⊢ ∀s. (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ sum s f
[SUM_POS_LE_NUMSEG] Theorem
⊢ ∀m n f. (∀p. m ≤ p ∧ p ≤ n ⇒ 0 ≤ f p) ⇒ 0 ≤ sum (m .. n) f
[SUM_POS_LT] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ∧ (∃x. x ∈ s ∧ 0 < f x) ⇒
0 < sum s f
[SUM_POS_LT_ALL] Theorem
⊢ ∀s f. FINITE s ∧ s ≠ ∅ ∧ (∀i. i ∈ s ⇒ 0 < f i) ⇒ 0 < sum s f
[SUM_RESTRICT] Theorem
⊢ ∀f s. FINITE s ⇒ (sum s (λx. if x ∈ s then f x else 0) = sum s f)
[SUM_RESTRICT_SET] Theorem
⊢ ∀P s f.
sum {x | x ∈ s ∧ P x} f = sum s (λx. if P x then f x else 0)
[SUM_RMUL] Theorem
⊢ ∀f c s. sum s (λx. f x * c) = sum s f * c
[SUM_SING] Theorem
⊢ ∀f x. sum {x} f = f x
[SUM_SING_NUMSEG] Theorem
⊢ ∀f n. sum (n .. n) f = f n
[SUM_SUB] Theorem
⊢ ∀f g s. FINITE s ⇒ (sum s (λx. f x − g x) = sum s f − sum s g)
[SUM_SUBSET] Theorem
⊢ ∀u v f.
FINITE u ∧ FINITE v ∧ (∀x. x ∈ u DIFF v ⇒ f x ≤ 0) ∧
(∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUBSET_SIMPLE] Theorem
⊢ ∀u v f.
FINITE v ∧ u ⊆ v ∧ (∀x. x ∈ v DIFF u ⇒ 0 ≤ f x) ⇒
sum u f ≤ sum v f
[SUM_SUB_NUMSEG] Theorem
⊢ ∀f g m n.
sum (m .. n) (λi. f i − g i) = sum (m .. n) f − sum (m .. n) g
[SUM_SUM_PRODUCT] Theorem
⊢ ∀s t x.
FINITE s ∧ (∀i. i ∈ s ⇒ FINITE (t i)) ⇒
(sum s (λi. sum (t i) (x i)) =
sum {(i,j) | i ∈ s ∧ j ∈ t i} (λ(i,j). x i j))
[SUM_SUM_RESTRICT] Theorem
⊢ ∀R f s t.
FINITE s ∧ FINITE t ⇒
(sum s (λx. sum {y | y ∈ t ∧ R x y} (λy. f x y)) =
sum t (λy. sum {x | x ∈ s ∧ R x y} (λx. f x y)))
[SUM_SUPERSET] Theorem
⊢ ∀f u v.
u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒ (sum v f = sum u f)
[SUM_SUPPORT] Theorem
⊢ ∀f s. sum (support $+ f s) f = sum s f
[SUM_SWAP] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ⇒
(sum s (λi. sum t (f i)) = sum t (λj. sum s (λi. f i j)))
[SUM_SWAP_NUMSEG] Theorem
⊢ ∀a b c d f.
sum (a .. b) (λi. sum (c .. d) (f i)) =
sum (c .. d) (λj. sum (a .. b) (λi. f i j))
[SUM_TRIV_NUMSEG] Theorem
⊢ ∀f m n. n < m ⇒ (sum (m .. n) f = 0)
[SUM_UNION] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
(sum (s ∪ t) f = sum s f + sum t f)
[SUM_UNION_EQ] Theorem
⊢ ∀s t u.
FINITE u ∧ (s ∩ t = ∅) ∧ (s ∪ t = u) ⇒
(sum s f + sum t f = sum u f)
[SUM_UNION_LZERO] Theorem
⊢ ∀f u v.
FINITE v ∧ (∀x. x ∈ u ∧ x ∉ v ⇒ (f x = 0)) ⇒
(sum (u ∪ v) f = sum v f)
[SUM_UNION_NONZERO] Theorem
⊢ ∀f s t.
FINITE s ∧ FINITE t ∧ (∀x. x ∈ s ∩ t ⇒ (f x = 0)) ⇒
(sum (s ∪ t) f = sum s f + sum t f)
[SUM_UNION_RZERO] Theorem
⊢ ∀f u v.
FINITE u ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ (f x = 0)) ⇒
(sum (u ∪ v) f = sum u f)
[SUM_ZERO_EXISTS] Theorem
⊢ ∀u s.
FINITE s ∧ (sum s u = 0) ⇒
(∀i. i ∈ s ⇒ (u i = 0)) ∨
∃j k. j ∈ s ∧ u j < 0 ∧ k ∈ s ∧ u k > 0
[SUP] Theorem
⊢ ∀s.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ⇒
(∀x. x ∈ s ⇒ x ≤ sup s) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[SUPPORT_CLAUSES] Theorem
⊢ (∀f. support op f ∅ = ∅) ∧
(∀f x s.
support op f (x INSERT s) =
if f x = neutral op then support op f s
else x INSERT support op f s) ∧
(∀f x s. support op f (s DELETE x) = support op f s DELETE x) ∧
(∀f s t. support op f (s ∪ t) = support op f s ∪ support op f t) ∧
(∀f s t. support op f (s ∩ t) = support op f s ∩ support op f t) ∧
(∀f s t.
support op f (s DIFF t) = support op f s DIFF support op f t) ∧
∀f g s. support op g (IMAGE f s) = IMAGE f (support op (g ∘ f) s)
[SUPPORT_DELTA] Theorem
⊢ ∀op s f a.
support op (λx. if x = a then f x else neutral op) s =
if a ∈ s then support op f {a} else ∅
[SUPPORT_EMPTY] Theorem
⊢ ∀op f s. (∀x. x ∈ s ⇒ (f x = neutral op)) ⇔ (support op f s = ∅)
[SUPPORT_SUBSET] Theorem
⊢ ∀op f s. support op f s ⊆ s
[SUPPORT_SUPPORT] Theorem
⊢ ∀op f s. support op f (support op f s) = support op f s
[SUP_EQ] Theorem
⊢ ∀s t.
(∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇔ ∀x. x ∈ t ⇒ x ≤ b) ⇒ (sup s = sup t)
[SUP_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ sup s ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ sup s
[SUP_FINITE_LEMMA] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∃b. b ∈ s ∧ ∀x. x ∈ s ⇒ x ≤ b
[SUP_INSERT_FINITE] Theorem
⊢ ∀x s.
FINITE s ⇒
(sup (x INSERT s) = if s = ∅ then x else max x (sup s))
[SUP_SING] Theorem
⊢ ∀a. sup {a} = a
[SUP_UNION] Theorem
⊢ ∀s t.
s ≠ ∅ ∧ t ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ x ≤ b) ∧
(∃c. ∀x. x ∈ t ⇒ x ≤ c) ⇒
(sup (s ∪ t) = max (sup s) (sup t))
[SUP_UNIQUE] Theorem
⊢ ∀s b. (∀c. (∀x. x ∈ s ⇒ x ≤ c) ⇔ b ≤ c) ⇒ (sup s = b)
[SUP_UNIQUE_FINITE] Theorem
⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ((sup s = a) ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)
[TH] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ (f x = g x)) ⇒ (sum s (λi. f i) = sum s g)) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ (f i = g i)) ⇒
(sum (a .. b) (λi. f i) = sum (a .. b) g)) ∧
∀f g p.
(∀x. p x ⇒ (f x = g x)) ⇒
(sum {y | p y} (λi. f i) = sum {y | p y} g)
[TOPOLOGICAL_SORT] Theorem
⊢ ∀ $<<.
(∀x y. x << y ∧ y << x ⇒ (x = y)) ∧
(∀x y z. x << y ∧ y << z ⇒ x << z) ⇒
∀n s.
s HAS_SIZE n ⇒
∃f.
(s = IMAGE f (1 .. n)) ∧
∀j k. j ∈ 1 .. n ∧ k ∈ 1 .. n ∧ j < k ⇒ ¬(f k << f j)
[UPPER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[real_INFINITE] Theorem
⊢ INFINITE 𝕌(:real)
[sup_alt] Theorem
⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b
*)
end
HOL 4, Kananaskis-13