Structure iterateTheory
signature iterateTheory =
sig
type thm = Thm.thm
(* Definitions *)
val FINREC_def : thm
val ITSET' : 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 ABS_LE_0 : thm
val ADD_SUB2 : thm
val ADD_SUBR : thm
val ADD_SUBR2 : thm
val BIGINTER_BIGUNION : thm
val BIGINTER_GSPEC : thm
val BIGINTER_IMAGE : thm
val BIGUNION_BIGINTER : thm
val BIGUNION_GSPEC : thm
val BIGUNION_IMAGE : thm
val BOUNDS_LINEAR : thm
val BOUNDS_LINEAR_0 : thm
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 DIFF_BIGINTER : thm
val DISJOINT_NUMSEG : thm
val EMPTY_BIGUNION : thm
val EXISTS_FINITE_SUBSET_IMAGE : thm
val EXISTS_IN_GSPEC : thm
val FINITE_INDEX_NUMBERS : thm
val FINITE_INDEX_NUMSEG : thm
val FINITE_NUMSEG : thm
val FINITE_POWERSET : thm
val FINITE_REAL_INTERVAL : thm
val FINITE_RECURSION : thm
val FINITE_RESTRICT : thm
val FINITE_SUBSET_IMAGE : 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_FINITE_SUBSET_IMAGE : thm
val FORALL_IN_GSPEC : thm
val FUN_IN_IMAGE : 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 LAMBDA_PAIR : thm
val LE_ADD : thm
val LE_ADDR : thm
val LE_EXISTS : thm
val LOWER_BOUND_FINITE_SET_REAL : thm
val LT_EXISTS : 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 NOT_EQ : 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_CONG : 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 POWERSET_CLAUSES : thm
val REAL_ABS_INF_LE : thm
val REAL_ABS_SUP_LE : thm
val REAL_BOUNDS_LT : thm
val REAL_COMPLETE : thm
val REAL_EQ_SQUARE_ABS : thm
val REAL_HALF : 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_INV_1_LE : thm
val REAL_LE_BETWEEN : thm
val REAL_LE_INF : thm
val REAL_LE_INF_FINITE : thm
val REAL_LE_INF_SUBSET : thm
val REAL_LE_INV2 : thm
val REAL_LE_LMUL1 : thm
val REAL_LE_SQUARE_ABS : 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_INV2 : thm
val REAL_LT_LCANCEL_IMP : thm
val REAL_LT_POW2 : thm
val REAL_LT_SUP_FINITE : thm
val REAL_OF_NUM_GE : 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_POW_1_LE : thm
val REAL_POW_LE_1 : 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' : thm
val REAL_SUP_LE_EQ : thm
val REAL_SUP_LE_FINITE : thm
val REAL_SUP_LE_SUBSET : thm
val REAL_SUP_LT_FINITE : thm
val REAL_SUP_UNIQUE : thm
val REAL_WLOG_LE : thm
val REAL_WLOG_LT : thm
val SET_PROVE_CASES : thm
val SET_RECURSION_LEMMA : thm
val SIMPLE_IMAGE_GEN : thm
val SUBSET_NUMSEG : thm
val SUBSET_RESTRICT : thm
val SUMS_SYM : 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_ABS_TRIANGLE : 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_CONG : 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_GP : thm
val SUM_GP_BASIC : thm
val SUM_GP_MULTIPLIED : 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 TOPOLOGICAL_SORT : thm
val TRANSITIVE_STEPWISE_LE : thm
val TRANSITIVE_STEPWISE_LE_EQ : thm
val UPPER_BOUND_FINITE_SET : thm
val UPPER_BOUND_FINITE_SET_REAL : thm
val WLOG_LE : thm
val inf_alt : thm
val real_INFINITE : thm
val sum_real : thm
val sup_alt : thm
val iterate_grammars : type_grammar.grammar * term_grammar.grammar
(*
[cardinal] Parent theory of "iterate"
[logroot] Parent theory of "iterate"
[real_sigma] Parent theory of "iterate"
[sorting] 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'] 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
[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}
[ABS_LE_0] Theorem
⊢ ∀x. abs x ≤ 0 ⇔ x = 0
[ADD_SUB2] Theorem
⊢ ∀m n. m + n − m = n
[ADD_SUBR] Theorem
⊢ ∀m n. n − (m + n) = 0
[ADD_SUBR2] Theorem
⊢ ∀m n. m − (m + n) = 0
[BIGINTER_BIGUNION] Theorem
⊢ ∀s. BIGINTER s = 𝕌(:α) DIFF BIGUNION {𝕌(:α) DIFF t | t ∈ s}
[BIGINTER_GSPEC] Theorem
⊢ (∀P f. BIGINTER {f x | P x} = {a | ∀x. P x ⇒ a ∈ f x}) ∧
(∀P f. BIGINTER {f x y | P x y} = {a | ∀x y. P x y ⇒ a ∈ f x y}) ∧
∀P f.
BIGINTER {f x y z | P x y z} =
{a | ∀x y z. P x y z ⇒ a ∈ f x y z}
[BIGINTER_IMAGE] Theorem
⊢ ∀f s. BIGINTER (IMAGE f s) = {y | ∀x. x ∈ s ⇒ y ∈ f x}
[BIGUNION_BIGINTER] Theorem
⊢ ∀s. BIGUNION s = 𝕌(:α) DIFF BIGINTER {𝕌(:α) DIFF t | t ∈ s}
[BIGUNION_GSPEC] Theorem
⊢ (∀P f. BIGUNION {f x | P x} = {a | ∃x. P x ∧ a ∈ f x}) ∧
(∀P f. BIGUNION {f x y | P x y} = {a | ∃x y. P x y ∧ a ∈ f x y}) ∧
∀P f.
BIGUNION {f x y z | P x y z} =
{a | ∃x y z. P x y z ∧ a ∈ f x y z}
[BIGUNION_IMAGE] Theorem
⊢ ∀f s. BIGUNION (IMAGE f s) = {y | ∃x. x ∈ s ∧ y ∈ f x}
[BOUNDS_LINEAR] Theorem
⊢ ∀A B C. (∀n. A * n ≤ B * n + C) ⇔ A ≤ B
[BOUNDS_LINEAR_0] Theorem
⊢ ∀A B. (∀n. A * n ≤ B) ⇔ A = 0
[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
[DIFF_BIGINTER] Theorem
⊢ ∀u s. u DIFF BIGINTER s = BIGUNION {u DIFF t | t ∈ s}
[DISJOINT_NUMSEG] Theorem
⊢ ∀m n p q.
DISJOINT (m .. n) (p .. q) ⇔ n < p ∨ q < m ∨ n < m ∨ q < p
[EMPTY_BIGUNION] Theorem
⊢ ∀s. BIGUNION s = ∅ ⇔ ∀t. t ∈ s ⇒ t = ∅
[EXISTS_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∃t. FINITE t ∧ t ⊆ IMAGE f s ∧ P t) ⇔
∃t. FINITE t ∧ t ⊆ s ∧ P (IMAGE f t)
[EXISTS_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)
[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_POWERSET] Theorem
⊢ ∀s. FINITE s ⇒ FINITE {t | t ⊆ s}
[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_SUBSET_IMAGE] Theorem
⊢ ∀f s t.
FINITE t ∧ t ⊆ IMAGE f s ⇔
∃s'. FINITE s' ∧ s' ⊆ s ∧ t = IMAGE f s'
[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_FINITE_SUBSET_IMAGE] Theorem
⊢ ∀P f s.
(∀t. FINITE t ∧ t ⊆ IMAGE f s ⇒ P t) ⇔
∀t. FINITE t ∧ t ⊆ s ⇒ P (IMAGE f t)
[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)
[FUN_IN_IMAGE] Theorem
⊢ ∀f s x. x ∈ s ⇒ f x ∈ IMAGE f s
[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.
s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ∧ t ≠ ∅ ∧
(∃b. ∀x. x ∈ t ⇒ b ≤ x) ∧
(∀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 a. 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)
[LAMBDA_PAIR] Theorem
⊢ (λ(x,y). P x y) = (λp. P (FST p) (SND p))
[LE_ADD] Theorem
⊢ ∀m n. m ≤ m + n
[LE_ADDR] Theorem
⊢ ∀m n. n ≤ m + n
[LE_EXISTS] Theorem
⊢ ∀m n. m ≤ n ⇔ ∃d. n = m + d
[LOWER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ a ≤ f x
[LT_EXISTS] Theorem
⊢ ∀m n. m < n ⇔ ∃d. n = m + SUC d
[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
[NOT_EQ] Theorem
⊢ ∀a b. a ≠ b ⇔ a ≠ b
[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_CONG] Theorem
⊢ (∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nsum s (λi. f i) = nsum s g) ∧
(∀f g a b.
(∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
nsum (a .. b) (λi. f i) = nsum (a .. b) g) ∧
∀f g p.
(∀x. p x ⇒ f x = g x) ⇒
nsum {y | p y} (λi. f i) = nsum {y | p y} g
[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)
[POWERSET_CLAUSES] Theorem
⊢ {s | s ⊆ ∅} = {∅} ∧
∀a t.
{s | s ⊆ a INSERT t} =
{s | s ⊆ t} ∪ IMAGE (λs. a INSERT s) {s | s ⊆ t}
[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_BOUNDS_LT] Theorem
⊢ ∀x k. -k < x ∧ x < k ⇔ abs x < k
[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_EQ_SQUARE_ABS] Theorem
⊢ ∀x y. abs x = abs y ⇔ x² = y²
[REAL_HALF] Theorem
⊢ (∀e. 0 < e / 2 ⇔ 0 < e) ∧ (∀e. e / 2 + e / 2 = e) ∧
∀e. 2 * (e / 2) = e
[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_INV_1_LE] Theorem
⊢ ∀x. 0 < x ∧ x ≤ 1 ⇒ 1 ≤ x⁻¹
[REAL_LE_BETWEEN] Theorem
⊢ ∀a b. a ≤ b ⇔ ∃x. a ≤ x ∧ x ≤ b
[REAL_LE_INF] Theorem
⊢ ∀s 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_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x ≤ y ⇒ y⁻¹ ≤ x⁻¹
[REAL_LE_LMUL1] Theorem
⊢ ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z
[REAL_LE_SQUARE_ABS] Theorem
⊢ ∀x y. abs x ≤ abs y ⇔ x² ≤ y²
[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_INV2] Theorem
⊢ ∀x y. 0 < x ∧ x < y ⇒ y⁻¹ < x⁻¹
[REAL_LT_LCANCEL_IMP] Theorem
⊢ ∀x y z. 0 < x ∧ x * y < x * z ⇒ y < z
[REAL_LT_POW2] Theorem
⊢ ∀n. 0 < 2 pow n
[REAL_LT_SUP_FINITE] Theorem
⊢ ∀s a. FINITE s ∧ s ≠ ∅ ⇒ (a < sup s ⇔ ∃x. x ∈ s ∧ a < x)
[REAL_OF_NUM_GE] Theorem
⊢ ∀m n. &m ≥ &n ⇔ m ≥ n
[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_POW_1_LE] Theorem
⊢ ∀n x. 0 ≤ x ∧ x ≤ 1 ⇒ x pow n ≤ 1
[REAL_POW_LE_1] Theorem
⊢ ∀n x. 1 ≤ x ⇒ 1 ≤ x pow 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'] Theorem
⊢ ∀s b. s ≠ ∅ ∧ (∀x. x ∈ s ⇒ x ≤ b) ⇒ sup s ≤ b
[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_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_LE] Theorem
⊢ (∀x y. P x y ⇔ P y x) ∧ (∀x y. x ≤ y ⇒ P x y) ⇒ ∀x y. P x y
[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)
[SIMPLE_IMAGE_GEN] Theorem
⊢ ∀f P. {f x | P x} = IMAGE f {x | P x}
[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
[SUMS_SYM] Theorem
⊢ ∀s t. {x + y | x ∈ s ∧ y ∈ t} = {y + x | y ∈ t ∧ 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_ABS_TRIANGLE] Theorem
⊢ ∀s f b. FINITE s ∧ sum s (λa. abs (f a)) ≤ b ⇒ abs (sum s f) ≤ b
[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_CONG] 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
[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_GP] Theorem
⊢ ∀x m n.
sum (m .. n) (λi. x pow i) =
if n < m then 0
else if x = 1 then &(n + 1 − m)
else (x pow m − x pow SUC n) / (1 − x)
[SUM_GP_BASIC] Theorem
⊢ ∀x n. (1 − x) * sum (0 .. n) (λi. x pow i) = 1 − x pow SUC n
[SUM_GP_MULTIPLIED] Theorem
⊢ ∀x m n.
m ≤ n ⇒
(1 − x) * sum (m .. n) (λi. x pow i) = x pow m − x pow SUC n
[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 a. FINITE s ∧ s ≠ ∅ ⇒ (sup s = a ⇔ a ∈ s ∧ ∀y. y ∈ s ⇒ y ≤ a)
[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)
[TRANSITIVE_STEPWISE_LE] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ∧
(∀n. R n (SUC n)) ⇒
∀m n. m ≤ n ⇒ R m n
[TRANSITIVE_STEPWISE_LE_EQ] Theorem
⊢ ∀R. (∀x. R x x) ∧ (∀x y z. R x y ∧ R y z ⇒ R x z) ⇒
((∀m n. m ≤ n ⇒ R m n) ⇔ ∀n. R n (SUC n))
[UPPER_BOUND_FINITE_SET] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[UPPER_BOUND_FINITE_SET_REAL] Theorem
⊢ ∀f s. FINITE s ⇒ ∃a. ∀x. x ∈ s ⇒ f x ≤ a
[WLOG_LE] Theorem
⊢ (∀m n. P m n ⇔ P n m) ∧ (∀m n. m ≤ n ⇒ P m n) ⇒ ∀m n. P m n
[inf_alt] Theorem
⊢ ∀s. s ≠ ∅ ∧ (∃b. ∀x. x ∈ s ⇒ b ≤ x) ⇒
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
[real_INFINITE] Theorem
⊢ INFINITE 𝕌(:real)
[sum_real] Theorem
⊢ ∀f n. sum (0 .. n) f = sum (0,SUC n) f
[sup_alt] Theorem
⊢ sup s = @a. (∀x. x ∈ s ⇒ x ≤ a) ∧ ∀b. (∀x. x ∈ s ⇒ x ≤ b) ⇒ a ≤ b
*)
end
HOL 4, Kananaskis-14