Structure util_probTheory
signature util_probTheory =
sig
type thm = Thm.thm
(* Definitions *)
val binary_def : thm
val disjoint_def : thm
val disjoint_family : thm
val disjoint_family_on : thm
val disjointed : thm
val fcp_cross_def : thm
val fcp_prod_def : thm
val general_cross_def : thm
val general_prod_def : thm
val lg_def : thm
val logr_def : thm
val minimal_def : thm
val pair_operation_def : thm
val prod_sets_def : thm
(* Theorems *)
val ADD_POW_2 : thm
val BIGINTER_IMAGE_OVER_INTER_L : thm
val BIGINTER_IMAGE_OVER_INTER_R : thm
val BIGINTER_PAIR : thm
val BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV : thm
val BIGUNION_IMAGE_COUNT_IMP_UNIV : thm
val BIGUNION_IMAGE_OVER_INTER_L : thm
val BIGUNION_IMAGE_OVER_INTER_R : thm
val BIGUNION_IMAGE_UNIV_CROSS_UNIV : thm
val BIGUNION_OVER_DIFF : thm
val BIGUNION_OVER_INTER_L : thm
val BIGUNION_OVER_INTER_R : thm
val BIGUNION_disjointed : thm
val BINARY_RANGE : thm
val COMPL_BIGINTER : thm
val COMPL_BIGINTER_IMAGE : thm
val COMPL_BIGUNION : thm
val COMPL_BIGUNION_IMAGE : thm
val CROSS_ALT : thm
val DIFF_INTER_PAIR : thm
val DINTER_IMP_FINITE_INTER : thm
val DISJOINT_CROSS_L : thm
val DISJOINT_CROSS_R : thm
val DISJOINT_RESTRICT_L : thm
val DISJOINT_RESTRICT_R : thm
val DUNION_IMP_FINITE_UNION : thm
val FCP_BIGUNION_CROSS : thm
val FCP_CROSS_BIGUNION : thm
val FCP_CROSS_DIFF : thm
val FCP_CROSS_DIFF' : thm
val FCP_INTER_CROSS : thm
val FCP_SUBSET_CROSS : thm
val GBIGUNION_IMAGE : thm
val GEN_COMPL_BIGINTER : thm
val GEN_COMPL_BIGINTER_IMAGE : thm
val GEN_COMPL_BIGUNION : thm
val GEN_COMPL_BIGUNION_IMAGE : thm
val GEN_COMPL_FINITE_INTER : thm
val GEN_COMPL_FINITE_UNION : thm
val GEN_COMPL_INTER : thm
val GEN_COMPL_UNION : thm
val GEN_DIFF_INTER : thm
val HARMONIC_SERIES_POW_2 : thm
val INCREASING_TO_DISJOINT_SETS : thm
val INCREASING_TO_DISJOINT_SETS' : thm
val INF_CLOSE : thm
val INF_DEF_ALT : thm
val INF_GREATER : thm
val INF_LE : thm
val INTER_BINARY : thm
val IN_FCP_CROSS : thm
val IN_FCP_PROD : thm
val IN_PROD_SETS : thm
val IN_general_cross : thm
val IN_general_prod : thm
val IN_o : thm
val LE_INF : thm
val LOGR_MONO_LE : thm
val LOGR_MONO_LE_IMP : thm
val MINIMAL_EQ : thm
val MINIMAL_EQ_IMP : thm
val MINIMAL_EXISTS : thm
val MINIMAL_EXISTS0 : thm
val MINIMAL_EXISTS_IMP : thm
val MINIMAL_SUC : thm
val MINIMAL_SUC_IMP : thm
val NUM_2D_BIJ : thm
val NUM_2D_BIJ_INV : thm
val NUM_2D_BIJ_NZ : thm
val NUM_2D_BIJ_NZ_ALT : thm
val NUM_2D_BIJ_NZ_ALT2 : thm
val NUM_2D_BIJ_NZ_ALT2_INV : thm
val NUM_2D_BIJ_NZ_ALT_INV : thm
val NUM_2D_BIJ_NZ_INV : thm
val NUM_2D_BIJ_nfst_nsnd : thm
val NUM_2D_BIJ_npair : thm
val PAIRED_BETA_THM : thm
val POW_HALF_MONO : thm
val POW_HALF_POS : thm
val POW_HALF_SMALL : thm
val POW_NEG_ODD : thm
val POW_POS_EVEN : thm
val PREIMAGE_REAL_COMPL1 : thm
val PREIMAGE_REAL_COMPL2 : thm
val PREIMAGE_REAL_COMPL3 : thm
val PREIMAGE_REAL_COMPL4 : thm
val REAL_ARCH_INV' : thm
val REAL_ARCH_INV_SUC : thm
val REAL_LE_LT_MUL : thm
val REAL_LE_RDIV_EQ_NEG : thm
val REAL_LT_LE_MUL : thm
val REAL_LT_LMUL_0_NEG : thm
val REAL_LT_LMUL_NEG_0 : thm
val REAL_LT_LMUL_NEG_0_NEG : thm
val REAL_LT_MAX_BETWEEN : thm
val REAL_LT_RDIV_EQ_NEG : thm
val REAL_LT_RMUL_0_NEG : thm
val REAL_LT_RMUL_NEG_0 : thm
val REAL_LT_RMUL_NEG_0_NEG : thm
val REAL_MAX_REDUCE : thm
val REAL_MIN_LE_BETWEEN : thm
val REAL_MIN_REDUCE : thm
val REAL_MUL_IDEMPOT : thm
val REAL_NEG_NZ : thm
val REAL_SUP_LE_X : thm
val REAL_X_LE_SUP : thm
val SETS_TO_DISJOINT_SETS : thm
val SETS_TO_DISJOINT_SETS' : thm
val SETS_TO_INCREASING_SETS : thm
val SETS_TO_INCREASING_SETS' : thm
val SUBSET_DIFF_DISJOINT : thm
val SUBSET_DIFF_SUBSET : thm
val SUBSET_INTER_SUBSET_L : thm
val SUBSET_INTER_SUBSET_R : thm
val SUBSET_MONO_DIFF : thm
val SUBSET_RESTRICT_DIFF : thm
val SUBSET_RESTRICT_L : thm
val SUBSET_RESTRICT_R : thm
val UNION_BINARY : thm
val UNION_TO_3_DISJOINT_UNIONS : thm
val countable_disjoint_decomposition : thm
val disjoint : thm
val disjointD : thm
val disjointI : thm
val disjoint_empty : thm
val disjoint_family_disjoint : thm
val disjoint_image : thm
val disjoint_insert : thm
val disjoint_insert_imp : thm
val disjoint_insert_notin : thm
val disjoint_restrict : thm
val disjoint_same : thm
val disjoint_sing : thm
val disjoint_two : thm
val disjoint_union : thm
val disjointed_subset : thm
val fcp_cross_UNIV : thm
val fcp_cross_alt : thm
val fcp_prod_alt : thm
val finite_decomposition : thm
val finite_decomposition_simple : thm
val finite_disjoint_decomposition : thm
val finite_enumeration_of_sets_has_max_non_empty : thm
val general_BIGUNION_CROSS : thm
val general_CROSS_BIGUNION : thm
val general_CROSS_DIFF : thm
val general_CROSS_DIFF' : thm
val general_INTER_CROSS : thm
val general_SUBSET_CROSS : thm
val infinitely_often_lemma : thm
val infinity_bound_lemma : thm
val lg_1 : thm
val lg_2 : thm
val lg_inv : thm
val lg_mul : thm
val lg_nonzero : thm
val lg_pow : thm
val logr_1 : thm
val logr_div : thm
val logr_inv : thm
val logr_mul : thm
val neg_lg : thm
val neg_logr : thm
val pair_operation_FCP_CONCAT : thm
val pair_operation_pair : thm
val prod_sets_alt : thm
val tail_countable : thm
val tail_not_empty : thm
val util_prob_grammars : type_grammar.grammar * term_grammar.grammar
(*
[fcp] Parent theory of "util_prob"
[numeral_bit] Parent theory of "util_prob"
[real_sigma] Parent theory of "util_prob"
[sorting] Parent theory of "util_prob"
[binary_def] Definition
⊢ ∀a b. binary a b = (λx. if x = 0 then a else b)
[disjoint_def] Definition
⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ DISJOINT a b
[disjoint_family] Definition
⊢ ∀A. disjoint_family A ⇔ disjoint_family_on A 𝕌(:α)
[disjoint_family_on] Definition
⊢ ∀a s.
disjoint_family_on a s ⇔
∀m n. m ∈ s ∧ n ∈ s ∧ m ≠ n ⇒ a m ∩ a n = ∅
[disjointed] Definition
⊢ ∀A n.
disjointed A n =
A n DIFF BIGUNION {A i | i ∈ {x | 0 ≤ x ∧ x < n}}
[fcp_cross_def] Definition
⊢ ∀A B. fcp_cross A B = {FCP_CONCAT a b | a ∈ A ∧ b ∈ B}
[fcp_prod_def] Definition
⊢ ∀a b. fcp_prod a b = {fcp_cross s t | s ∈ a ∧ t ∈ b}
[general_cross_def] Definition
⊢ ∀cons A B. general_cross cons A B = {cons a b | a ∈ A ∧ b ∈ B}
[general_prod_def] Definition
⊢ ∀cons A B.
general_prod cons A B = {general_cross cons a b | a ∈ A ∧ b ∈ B}
[lg_def] Definition
⊢ ∀x. lg x = logr 2 x
[logr_def] Definition
⊢ ∀a x. logr a x = ln x / ln a
[minimal_def] Definition
⊢ ∀p. minimal p = @n. p n ∧ ∀m. m < n ⇒ ¬p m
[pair_operation_def] Definition
⊢ ∀cons car cdr.
pair_operation cons car cdr ⇔
(∀a b. car (cons a b) = a ∧ cdr (cons a b) = b) ∧
∀a b c d. cons a b = cons c d ⇔ a = c ∧ b = d
[prod_sets_def] Definition
⊢ ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}
[ADD_POW_2] Theorem
⊢ ∀x y. (x + y)² = x² + y² + 2 * x * y
[BIGINTER_IMAGE_OVER_INTER_L] Theorem
⊢ ∀f n d.
0 < n ⇒
BIGINTER (IMAGE f (count n)) ∩ d =
BIGINTER (IMAGE (λi. f i ∩ d) (count n))
[BIGINTER_IMAGE_OVER_INTER_R] Theorem
⊢ ∀f n d.
0 < n ⇒
d ∩ BIGINTER (IMAGE f (count n)) =
BIGINTER (IMAGE (λi. d ∩ f i) (count n))
[BIGINTER_PAIR] Theorem
⊢ ∀s t. BIGINTER {s; t} = s ∩ t
[BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV] Theorem
⊢ ∀f. BIGUNION (IMAGE (λn. BIGUNION (IMAGE (f n) 𝕌(:num))) 𝕌(:num)) =
BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num))
[BIGUNION_IMAGE_COUNT_IMP_UNIV] Theorem
⊢ ∀f g.
(∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[BIGUNION_IMAGE_OVER_INTER_L] Theorem
⊢ ∀f n d.
BIGUNION (IMAGE f (count n)) ∩ d =
BIGUNION (IMAGE (λi. f i ∩ d) (count n))
[BIGUNION_IMAGE_OVER_INTER_R] Theorem
⊢ ∀f n d.
d ∩ BIGUNION (IMAGE f (count n)) =
BIGUNION (IMAGE (λi. d ∩ f i) (count n))
[BIGUNION_IMAGE_UNIV_CROSS_UNIV] Theorem
⊢ ∀f h.
BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
BIGUNION (IMAGE (UNCURRY f) 𝕌(:num # num)) =
BIGUNION (IMAGE (UNCURRY f ∘ h) 𝕌(:num))
[BIGUNION_OVER_DIFF] Theorem
⊢ ∀f d.
BIGUNION (IMAGE f 𝕌(:num)) DIFF d =
BIGUNION (IMAGE (λi. f i DIFF d) 𝕌(:num))
[BIGUNION_OVER_INTER_L] Theorem
⊢ ∀f d.
BIGUNION (IMAGE f 𝕌(:num)) ∩ d =
BIGUNION (IMAGE (λi. f i ∩ d) 𝕌(:num))
[BIGUNION_OVER_INTER_R] Theorem
⊢ ∀f d.
d ∩ BIGUNION (IMAGE f 𝕌(:num)) =
BIGUNION (IMAGE (λi. d ∩ f i) 𝕌(:num))
[BIGUNION_disjointed] Theorem
⊢ ∀A. BIGUNION {disjointed A i | i ∈ 𝕌(:num)} =
BIGUNION {A i | i ∈ 𝕌(:num)}
[BINARY_RANGE] Theorem
⊢ ∀a b. IMAGE (binary a b) 𝕌(:num) = {a; b}
[COMPL_BIGINTER] Theorem
⊢ ∀c. COMPL (BIGINTER c) = BIGUNION (IMAGE COMPL c)
[COMPL_BIGINTER_IMAGE] Theorem
⊢ ∀f. COMPL (BIGINTER (IMAGE f 𝕌(:num))) =
BIGUNION (IMAGE (COMPL ∘ f) 𝕌(:num))
[COMPL_BIGUNION] Theorem
⊢ ∀c. c ≠ ∅ ⇒ COMPL (BIGUNION c) = BIGINTER (IMAGE COMPL c)
[COMPL_BIGUNION_IMAGE] Theorem
⊢ ∀f. COMPL (BIGUNION (IMAGE f 𝕌(:num))) =
BIGINTER (IMAGE (COMPL ∘ f) 𝕌(:num))
[CROSS_ALT] Theorem
⊢ ∀A B. A × B = general_cross $, A B
[DIFF_INTER_PAIR] Theorem
⊢ ∀sp x y. sp DIFF x ∩ y = sp DIFF x ∪ (sp DIFF y)
[DINTER_IMP_FINITE_INTER] Theorem
⊢ ∀sts f.
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (𝕌(:num) → sts) ⇒
∀n. 0 < n ⇒ BIGINTER (IMAGE f (count n)) ∈ sts
[DISJOINT_CROSS_L] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s × c) (t × c)
[DISJOINT_CROSS_R] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c × s) (c × t)
[DISJOINT_RESTRICT_L] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s ∩ c) (t ∩ c)
[DISJOINT_RESTRICT_R] Theorem
⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c ∩ s) (c ∩ t)
[DUNION_IMP_FINITE_UNION] Theorem
⊢ ∀sts f.
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ⇒
∀n. 0 < n ∧ (∀i. i < n ⇒ f i ∈ sts) ⇒
BIGUNION (IMAGE f (count n)) ∈ sts
[FCP_BIGUNION_CROSS] Theorem
⊢ ∀f s t.
fcp_cross (BIGUNION (IMAGE f s)) t =
BIGUNION (IMAGE (λn. fcp_cross (f n) t) s)
[FCP_CROSS_BIGUNION] Theorem
⊢ ∀f s t.
fcp_cross t (BIGUNION (IMAGE f s)) =
BIGUNION (IMAGE (λn. fcp_cross t (f n)) s)
[FCP_CROSS_DIFF] Theorem
⊢ ∀X s t.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross (X DIFF s) t = fcp_cross X t DIFF fcp_cross s t
[FCP_CROSS_DIFF'] Theorem
⊢ ∀s X t.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross s (X DIFF t) = fcp_cross s X DIFF fcp_cross s t
[FCP_INTER_CROSS] Theorem
⊢ ∀a b c d.
FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross a b ∩ fcp_cross c d = fcp_cross (a ∩ c) (b ∩ d)
[FCP_SUBSET_CROSS] Theorem
⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ fcp_cross a c ⊆ fcp_cross b d
[GBIGUNION_IMAGE] Theorem
⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))
[GEN_COMPL_BIGINTER] Theorem
⊢ ∀sp c.
(∀x. x ∈ c ⇒ x ⊆ sp) ⇒
sp DIFF BIGINTER c = BIGUNION (IMAGE (λx. sp DIFF x) c)
[GEN_COMPL_BIGINTER_IMAGE] Theorem
⊢ ∀sp f.
(∀n. f n ⊆ sp) ⇒
sp DIFF BIGINTER (IMAGE f 𝕌(:num)) =
BIGUNION (IMAGE (λn. sp DIFF f n) 𝕌(:num))
[GEN_COMPL_BIGUNION] Theorem
⊢ ∀sp c.
c ≠ ∅ ∧ (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
sp DIFF BIGUNION c = BIGINTER (IMAGE (λx. sp DIFF x) c)
[GEN_COMPL_BIGUNION_IMAGE] Theorem
⊢ ∀sp f.
(∀n. f n ⊆ sp) ⇒
sp DIFF BIGUNION (IMAGE f 𝕌(:num)) =
BIGINTER (IMAGE (λn. sp DIFF f n) 𝕌(:num))
[GEN_COMPL_FINITE_INTER] Theorem
⊢ ∀sp f n.
0 < n ⇒
sp DIFF BIGINTER (IMAGE f (count n)) =
BIGUNION (IMAGE (λi. sp DIFF f i) (count n))
[GEN_COMPL_FINITE_UNION] Theorem
⊢ ∀sp f n.
0 < n ⇒
sp DIFF BIGUNION (IMAGE f (count n)) =
BIGINTER (IMAGE (λi. sp DIFF f i) (count n))
[GEN_COMPL_INTER] Theorem
⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF s ∩ t = sp DIFF s ∪ (sp DIFF t)
[GEN_COMPL_UNION] Theorem
⊢ ∀sp s t.
s ⊆ sp ∧ t ⊆ sp ⇒ sp DIFF (s ∪ t) = (sp DIFF s) ∩ (sp DIFF t)
[GEN_DIFF_INTER] Theorem
⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ s DIFF t = s ∩ (sp DIFF t)
[HARMONIC_SERIES_POW_2] Theorem
⊢ summable (λn. (&SUC n)² ⁻¹)
[INCREASING_TO_DISJOINT_SETS] Theorem
⊢ ∀f. (∀n. f n ⊆ f (SUC n)) ⇒
∃g. g 0 = f 0 ∧ (∀n. 0 < n ⇒ g n = f n DIFF f (PRE n)) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[INCREASING_TO_DISJOINT_SETS'] Theorem
⊢ ∀f. f 0 = ∅ ∧ (∀n. f n ⊆ f (SUC n)) ⇒
∃g. (∀n. g n = f (SUC n) DIFF f n) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[INF_CLOSE] Theorem
⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e
[INF_DEF_ALT] Theorem
⊢ ∀p. inf p = -sup (λr. -r ∈ p)
[INF_GREATER] Theorem
⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z
[INF_LE] Theorem
⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r
[INTER_BINARY] Theorem
⊢ ∀a b. a ∩ b = BIGINTER {binary a b i | i ∈ 𝕌(:num)}
[IN_FCP_CROSS] Theorem
⊢ ∀s a b.
s ∈ fcp_cross a b ⇔ ∃t u. s = FCP_CONCAT t u ∧ t ∈ a ∧ u ∈ b
[IN_FCP_PROD] Theorem
⊢ ∀s A B. s ∈ fcp_prod A B ⇔ ∃a b. s = fcp_cross a b ∧ a ∈ A ∧ b ∈ B
[IN_PROD_SETS] Theorem
⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. s = t × u ∧ t ∈ a ∧ u ∈ b
[IN_general_cross] Theorem
⊢ ∀cons s A B.
s ∈ general_cross cons A B ⇔ ∃a b. s = cons a b ∧ a ∈ A ∧ b ∈ B
[IN_general_prod] Theorem
⊢ ∀cons s A B.
s ∈ general_prod cons A B ⇔
∃a b. s = general_cross cons a b ∧ a ∈ A ∧ b ∈ B
[IN_o] Theorem
⊢ ∀x f s. x ∈ s ∘ f ⇔ f x ∈ s
[LE_INF] Theorem
⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p
[LOGR_MONO_LE] Theorem
⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)
[LOGR_MONO_LE_IMP] Theorem
⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y
[MINIMAL_EQ] Theorem
⊢ ∀p m. p m ∧ m = minimal p ⇔ p m ∧ ∀n. n < m ⇒ ¬p n
[MINIMAL_EQ_IMP] Theorem
⊢ ∀m p. p m ∧ (∀n. n < m ⇒ ¬p n) ⇒ m = minimal p
[MINIMAL_EXISTS] Theorem
⊢ ∀P. (∃n. P n) ⇔ P (minimal P) ∧ ∀n. n < minimal P ⇒ ¬P n
[MINIMAL_EXISTS0] Theorem
⊢ (∃n. P n) ⇔ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m
[MINIMAL_EXISTS_IMP] Theorem
⊢ ∀P. (∃n. P n) ⇒ ∃m. P m ∧ ∀n. n < m ⇒ ¬P n
[MINIMAL_SUC] Theorem
⊢ ∀n p.
SUC n = minimal p ∧ p (SUC n) ⇔
¬p 0 ∧ n = minimal (p ∘ SUC) ∧ p (SUC n)
[MINIMAL_SUC_IMP] Theorem
⊢ ∀n p. p (SUC n) ∧ ¬p 0 ∧ n = minimal (p ∘ SUC) ⇒ SUC n = minimal p
[NUM_2D_BIJ] Theorem
⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) 𝕌(:num)
[NUM_2D_BIJ_INV] Theorem
⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num))
[NUM_2D_BIJ_NZ] Theorem
⊢ ∃f. BIJ f (𝕌(:num) × (𝕌(:num) DIFF {0})) 𝕌(:num)
[NUM_2D_BIJ_NZ_ALT] Theorem
⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) (𝕌(:num) DIFF {0})
[NUM_2D_BIJ_NZ_ALT2] Theorem
⊢ ∃f. BIJ f ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0})) 𝕌(:num)
[NUM_2D_BIJ_NZ_ALT2_INV] Theorem
⊢ ∃f. BIJ f 𝕌(:num) ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0}))
[NUM_2D_BIJ_NZ_ALT_INV] Theorem
⊢ ∃f. BIJ f (𝕌(:num) DIFF {0}) (𝕌(:num) × 𝕌(:num))
[NUM_2D_BIJ_NZ_INV] Theorem
⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × (𝕌(:num) DIFF {0}))
[NUM_2D_BIJ_nfst_nsnd] Theorem
⊢ BIJ (λn. (nfst n,nsnd n)) 𝕌(:num) (𝕌(:num) × 𝕌(:num))
[NUM_2D_BIJ_npair] Theorem
⊢ BIJ (UNCURRY $*,) (𝕌(:num) × 𝕌(:num)) 𝕌(:num)
[PAIRED_BETA_THM] Theorem
⊢ ∀f z. UNCURRY f z = f (FST z) (SND z)
[POW_HALF_MONO] Theorem
⊢ ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m
[POW_HALF_POS] Theorem
⊢ ∀n. 0 < (1 / 2) pow n
[POW_HALF_SMALL] Theorem
⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e
[POW_NEG_ODD] Theorem
⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)
[POW_POS_EVEN] Theorem
⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)
[PREIMAGE_REAL_COMPL1] Theorem
⊢ ∀c. COMPL {x | c < x} = {x | x ≤ c}
[PREIMAGE_REAL_COMPL2] Theorem
⊢ ∀c. COMPL {x | c ≤ x} = {x | x < c}
[PREIMAGE_REAL_COMPL3] Theorem
⊢ ∀c. COMPL {x | x ≤ c} = {x | c < x}
[PREIMAGE_REAL_COMPL4] Theorem
⊢ ∀c. COMPL {x | x < c} = {x | c ≤ x}
[REAL_ARCH_INV'] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&n)⁻¹ < x
[REAL_ARCH_INV_SUC] Theorem
⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x
[REAL_LE_LT_MUL] Theorem
⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y
[REAL_LE_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)
[REAL_LT_LE_MUL] Theorem
⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y
[REAL_LT_LMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0
[REAL_LT_LMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0
[REAL_LT_LMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y
[REAL_LT_MAX_BETWEEN] Theorem
⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d
[REAL_LT_RDIV_EQ_NEG] Theorem
⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)
[REAL_LT_RMUL_0_NEG] Theorem
⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0
[REAL_LT_RMUL_NEG_0] Theorem
⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0
[REAL_LT_RMUL_NEG_0_NEG] Theorem
⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x
[REAL_MAX_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ max x y = y ∧ max y x = y
[REAL_MIN_LE_BETWEEN] Theorem
⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x
[REAL_MIN_REDUCE] Theorem
⊢ ∀x y. x ≤ y ∨ x < y ⇒ min x y = x ∧ min y x = x
[REAL_MUL_IDEMPOT] Theorem
⊢ ∀r. r * r = r ⇔ r = 0 ∨ r = 1
[REAL_NEG_NZ] Theorem
⊢ ∀x. x < 0 ⇒ x ≠ 0
[REAL_SUP_LE_X] Theorem
⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x
[REAL_X_LE_SUP] Theorem
⊢ ∀P x.
(∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P
[SETS_TO_DISJOINT_SETS] Theorem
⊢ ∀sp sts f.
(∀s. s ∈ sts ⇒ s ⊆ sp) ∧ (∀n. f n ∈ sts) ⇒
∃g. g 0 = f 0 ∧
(∀n. 0 < n ⇒
g n = f n ∩ BIGINTER (IMAGE (λi. sp DIFF f i) (count n))) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_DISJOINT_SETS'] Theorem
⊢ ∀f. ∃g.
g 0 = f 0 ∧
(∀n. 0 < n ⇒ g n = f n ∩ BIGINTER (IMAGE (COMPL ∘ f) (count n))) ∧
(∀i j. i ≠ j ⇒ DISJOINT (g i) (g j)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_INCREASING_SETS] Theorem
⊢ ∀f. ∃g.
g 0 = f 0 ∧ (∀n. g n = BIGUNION (IMAGE f (count (SUC n)))) ∧
(∀n. g n ⊆ g (SUC n)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SETS_TO_INCREASING_SETS'] Theorem
⊢ ∀f. ∃g.
g 0 = ∅ ∧ (∀n. g n = BIGUNION (IMAGE f (count n))) ∧
(∀n. g n ⊆ g (SUC n)) ∧
BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))
[SUBSET_DIFF_DISJOINT] Theorem
⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇒ DISJOINT s1 s3
[SUBSET_DIFF_SUBSET] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t
[SUBSET_INTER_SUBSET_L] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t
[SUBSET_INTER_SUBSET_R] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ t
[SUBSET_MONO_DIFF] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t DIFF r
[SUBSET_RESTRICT_DIFF] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r DIFF t ⊆ r DIFF s
[SUBSET_RESTRICT_L] Theorem
⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t ∩ r
[SUBSET_RESTRICT_R] Theorem
⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ r ∩ t
[UNION_BINARY] Theorem
⊢ ∀a b. a ∪ b = BIGUNION {binary a b i | i ∈ 𝕌(:num)}
[UNION_TO_3_DISJOINT_UNIONS] Theorem
⊢ ∀s t.
s ∪ t = s DIFF t ∪ s ∩ t ∪ (t DIFF s) ∧
disjoint {s DIFF t; s ∩ t; t DIFF s}
[countable_disjoint_decomposition] Theorem
⊢ ∀c. FINITE c ∧ disjoint c ⇒
∃f n.
(∀i. i < n ⇒ f i ∈ c) ∧ (∀i. n ≤ i ⇒ f i = ∅) ∧
c = IMAGE f (count n) ∧
BIGUNION c = BIGUNION (IMAGE f 𝕌(:num)) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
[disjoint] Theorem
⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ a ∩ b = ∅
[disjointD] Theorem
⊢ ∀A a b. disjoint A ⇒ a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b
[disjointI] Theorem
⊢ ∀A. (∀a b. a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b) ⇒ disjoint A
[disjoint_empty] Theorem
⊢ disjoint ∅
[disjoint_family_disjoint] Theorem
⊢ ∀A. disjoint_family (disjointed A)
[disjoint_image] Theorem
⊢ ∀f. (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒ disjoint (IMAGE f 𝕌(:α))
[disjoint_insert] Theorem
⊢ ∀e c.
disjoint c ∧ (∀x. x ∈ c ⇒ DISJOINT x e) ⇒ disjoint (e INSERT c)
[disjoint_insert_imp] Theorem
⊢ ∀e c. disjoint (e INSERT c) ⇒ disjoint c
[disjoint_insert_notin] Theorem
⊢ ∀e c. disjoint (e INSERT c) ∧ e ∉ c ⇒ ∀s. s ∈ c ⇒ DISJOINT e s
[disjoint_restrict] Theorem
⊢ ∀e c. disjoint c ⇒ disjoint (IMAGE ($INTER e) c)
[disjoint_same] Theorem
⊢ ∀s t. s = t ⇒ disjoint {s; t}
[disjoint_sing] Theorem
⊢ ∀a. disjoint {a}
[disjoint_two] Theorem
⊢ ∀s t. s ≠ t ∧ DISJOINT s t ⇒ disjoint {s; t}
[disjoint_union] Theorem
⊢ ∀A B.
disjoint A ∧ disjoint B ∧ BIGUNION A ∩ BIGUNION B = ∅ ⇒
disjoint (A ∪ B)
[disjointed_subset] Theorem
⊢ ∀A n. disjointed A n ⊆ A n
[fcp_cross_UNIV] Theorem
⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
fcp_cross 𝕌(:α[β]) 𝕌(:α[γ]) = 𝕌(:α[β + γ])
[fcp_cross_alt] Theorem
⊢ ∀A B. fcp_cross A B = general_cross FCP_CONCAT A B
[fcp_prod_alt] Theorem
⊢ ∀A B. fcp_prod A B = general_prod FCP_CONCAT A B
[finite_decomposition] Theorem
⊢ ∀c. FINITE c ⇒
∃f n.
(∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j
[finite_decomposition_simple] Theorem
⊢ ∀c. FINITE c ⇒ ∃f n. (∀x. x < n ⇒ f x ∈ c) ∧ c = IMAGE f (count n)
[finite_disjoint_decomposition] Theorem
⊢ ∀c. FINITE c ∧ disjoint c ⇒
∃f n.
(∀i. i < n ⇒ f i ∈ c) ∧ c = IMAGE f (count n) ∧
(∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ f i ≠ f j) ∧
∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)
[finite_enumeration_of_sets_has_max_non_empty] Theorem
⊢ ∀f s.
FINITE s ∧ (∀x. f x ∈ s) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
∃N. ∀n. n ≥ N ⇒ f n = ∅
[general_BIGUNION_CROSS] Theorem
⊢ ∀cons f s t.
general_cross cons (BIGUNION (IMAGE f s)) t =
BIGUNION (IMAGE (λn. general_cross cons (f n) t) s)
[general_CROSS_BIGUNION] Theorem
⊢ ∀cons f s t.
general_cross cons t (BIGUNION (IMAGE f s)) =
BIGUNION (IMAGE (λn. general_cross cons t (f n)) s)
[general_CROSS_DIFF] Theorem
⊢ ∀cons car cdr X s t.
pair_operation cons car cdr ⇒
general_cross cons (X DIFF s) t =
general_cross cons X t DIFF general_cross cons s t
[general_CROSS_DIFF'] Theorem
⊢ ∀cons car cdr s X t.
pair_operation cons car cdr ⇒
general_cross cons s (X DIFF t) =
general_cross cons s X DIFF general_cross cons s t
[general_INTER_CROSS] Theorem
⊢ ∀cons car cdr a b c d.
pair_operation cons car cdr ⇒
general_cross cons a b ∩ general_cross cons c d =
general_cross cons (a ∩ c) (b ∩ d)
[general_SUBSET_CROSS] Theorem
⊢ ∀cons a b c d.
a ⊆ b ∧ c ⊆ d ⇒ general_cross cons a c ⊆ general_cross cons b d
[infinitely_often_lemma] Theorem
⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n
[infinity_bound_lemma] Theorem
⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N
[lg_1] Theorem
⊢ lg 1 = 0
[lg_2] Theorem
⊢ lg 2 = 1
[lg_inv] Theorem
⊢ ∀x. 0 < x ⇒ lg x⁻¹ = -lg x
[lg_mul] Theorem
⊢ ∀x y. 0 < x ∧ 0 < y ⇒ lg (x * y) = lg x + lg y
[lg_nonzero] Theorem
⊢ ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)
[lg_pow] Theorem
⊢ ∀n. lg (2 pow n) = &n
[logr_1] Theorem
⊢ ∀b. logr b 1 = 0
[logr_div] Theorem
⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ logr b (x / y) = logr b x − logr b y
[logr_inv] Theorem
⊢ ∀b x. 0 < x ⇒ logr b x⁻¹ = -logr b x
[logr_mul] Theorem
⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ logr b (x * y) = logr b x + logr b y
[neg_lg] Theorem
⊢ ∀x. 0 < x ⇒ -lg x = lg x⁻¹
[neg_logr] Theorem
⊢ ∀b x. 0 < x ⇒ -logr b x = logr b x⁻¹
[pair_operation_FCP_CONCAT] Theorem
⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
pair_operation FCP_CONCAT FCP_FST FCP_SND
[pair_operation_pair] Theorem
⊢ pair_operation $, FST SND
[prod_sets_alt] Theorem
⊢ ∀A B. prod_sets A B = general_prod $, A B
[tail_countable] Theorem
⊢ ∀A m. countable {A n | m ≤ n}
[tail_not_empty] Theorem
⊢ ∀A m. {A n | m ≤ n} ≠ ∅
*)
end
HOL 4, Kananaskis-14