Theory "util_prob"

Signature

Definitions

binary_def

⊢ ∀a b. binary a b = (λx. if x = 0 then a else b)

disjoint_def

⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ DISJOINT a b

disjoint_family

⊢ ∀A. disjoint_family A ⇔ disjoint_family_on A 𝕌(:α)

disjoint_family_on

⊢ ∀a s. disjoint_family_on a s ⇔ ∀m n. m ∈ s ∧ n ∈ s ∧ m ≠ n ⇒ (a m ∩ a n = ∅)

disjointed

⊢ ∀A n. disjointed A n = A n DIFF BIGUNION {A i | i ∈ {x | 0 ≤ x ∧ x < n}}

fcp_cross_def

⊢ ∀A B. fcp_cross A B = {FCP_CONCAT a b | a ∈ A ∧ b ∈ B}

fcp_prod_def

⊢ ∀a b. fcp_prod a b = {fcp_cross s t | s ∈ a ∧ t ∈ b}

general_cross_def

⊢ ∀cons A B. general_cross cons A B = {cons a b | a ∈ A ∧ b ∈ B}

general_prod_def

⊢ ∀cons A B. general_prod cons A B = {general_cross cons a b | a ∈ A ∧ b ∈ B}

lg_def

⊢ ∀x. lg x = logr 2 x

logr_def

⊢ ∀a x. logr a x = ln x / ln a

minimal_def

⊢ ∀p. minimal p = @n. p n ∧ ∀m. m < n ⇒ ¬p m

pair_operation_def

⊢ ∀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

⊢ ∀a b. prod_sets a b = {s × t | s ∈ a ∧ t ∈ b}

Theorems

ADD_POW_2

⊢ ∀x y. (x + y)² = x² + y² + 2 * x * y

BIGINTER_IMAGE_OVER_INTER_L

⊢ ∀f n d.
    0 < n ⇒
    (BIGINTER (IMAGE f (count n)) ∩ d =
     BIGINTER (IMAGE (λi. f i ∩ d) (count n)))

BIGINTER_IMAGE_OVER_INTER_R

⊢ ∀f n d.
    0 < n ⇒
    (d ∩ BIGINTER (IMAGE f (count n)) =
     BIGINTER (IMAGE (λi. d ∩ f i) (count n)))

BIGINTER_PAIR

⊢ ∀s t. BIGINTER {s; t} = s ∩ t

BIGUNION_IMAGE_BIGUNION_IMAGE_UNIV

⊢ ∀f. BIGUNION (IMAGE (λn. BIGUNION (IMAGE (f n) 𝕌(:num))) 𝕌(:num)) =
      BIGUNION (IMAGE fᴾ 𝕌(:num # num))

BIGUNION_IMAGE_COUNT_IMP_UNIV

⊢ ∀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

⊢ ∀f n d.
    BIGUNION (IMAGE f (count n)) ∩ d =
    BIGUNION (IMAGE (λi. f i ∩ d) (count n))

BIGUNION_IMAGE_OVER_INTER_R

⊢ ∀f n d.
    d ∩ BIGUNION (IMAGE f (count n)) =
    BIGUNION (IMAGE (λi. d ∩ f i) (count n))

BIGUNION_IMAGE_UNIV_CROSS_UNIV

⊢ ∀f h.
    BIJ h 𝕌(:num) (𝕌(:num) × 𝕌(:num)) ⇒
    (BIGUNION (IMAGE fᴾ 𝕌(:num # num)) = BIGUNION (IMAGE (fᴾ ∘ h) 𝕌(:num)))

BIGUNION_OVER_DIFF

⊢ ∀f d.
    BIGUNION (IMAGE f 𝕌(:num)) DIFF d =
    BIGUNION (IMAGE (λi. f i DIFF d) 𝕌(:num))

BIGUNION_OVER_INTER_L

⊢ ∀f d.
    BIGUNION (IMAGE f 𝕌(:num)) ∩ d = BIGUNION (IMAGE (λi. f i ∩ d) 𝕌(:num))

BIGUNION_OVER_INTER_R

⊢ ∀f d.
    d ∩ BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE (λi. d ∩ f i) 𝕌(:num))

BIGUNION_disjointed

⊢ ∀A. BIGUNION {disjointed A i | i ∈ 𝕌(:num)} = BIGUNION {A i | i ∈ 𝕌(:num)}

BINARY_RANGE

⊢ ∀a b. IMAGE (binary a b) 𝕌(:num) = {a; b}

COMPL_BIGINTER

⊢ ∀c. COMPL (BIGINTER c) = BIGUNION (IMAGE COMPL c)

COMPL_BIGINTER_IMAGE

⊢ ∀f. COMPL (BIGINTER (IMAGE f 𝕌(:num))) =
      BIGUNION (IMAGE (COMPL ∘ f) 𝕌(:num))

COMPL_BIGUNION

⊢ ∀c. c ≠ ∅ ⇒ (COMPL (BIGUNION c) = BIGINTER (IMAGE COMPL c))

COMPL_BIGUNION_IMAGE

⊢ ∀f. COMPL (BIGUNION (IMAGE f 𝕌(:num))) =
      BIGINTER (IMAGE (COMPL ∘ f) 𝕌(:num))

CROSS_ALT

⊢ ∀A B. A × B = general_cross $, A B

DIFF_INTER_PAIR

⊢ ∀sp x y. sp DIFF x ∩ y = sp DIFF x ∪ (sp DIFF y)

DINTER_IMP_FINITE_INTER

⊢ ∀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

⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s × c) (t × c)

DISJOINT_CROSS_R

⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c × s) (c × t)

DISJOINT_RESTRICT_L

⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (s ∩ c) (t ∩ c)

DISJOINT_RESTRICT_R

⊢ ∀s t c. DISJOINT s t ⇒ DISJOINT (c ∩ s) (c ∩ t)

DUNION_IMP_FINITE_UNION

⊢ ∀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

⊢ ∀f s t.
    fcp_cross (BIGUNION (IMAGE f s)) t =
    BIGUNION (IMAGE (λn. fcp_cross (f n) t) s)

FCP_CROSS_BIGUNION

⊢ ∀f s t.
    fcp_cross t (BIGUNION (IMAGE f s)) =
    BIGUNION (IMAGE (λn. fcp_cross t (f n)) s)

FCP_CROSS_DIFF

⊢ ∀X s t.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    (fcp_cross (X DIFF s) t = fcp_cross X t DIFF fcp_cross s t)

FCP_CROSS_DIFF'

⊢ ∀s X t.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    (fcp_cross s (X DIFF t) = fcp_cross s X DIFF fcp_cross s t)

FCP_INTER_CROSS

⊢ ∀a b c d.
    FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒
    (fcp_cross a b ∩ fcp_cross c d = fcp_cross (a ∩ c) (b ∩ d))

FCP_SUBSET_CROSS

⊢ ∀a b c d. a ⊆ b ∧ c ⊆ d ⇒ fcp_cross a c ⊆ fcp_cross b d

GBIGUNION_IMAGE

⊢ ∀s p n. {s | ∃n. p s n} = BIGUNION (IMAGE (λn. {s | p s n}) 𝕌(:γ))

GEN_COMPL_BIGINTER

⊢ ∀sp c.
    (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
    (sp DIFF BIGINTER c = BIGUNION (IMAGE (λx. sp DIFF x) c))

GEN_COMPL_BIGINTER_IMAGE

⊢ ∀sp f.
    (∀n. f n ⊆ sp) ⇒
    (sp DIFF BIGINTER (IMAGE f 𝕌(:num)) =
     BIGUNION (IMAGE (λn. sp DIFF f n) 𝕌(:num)))

GEN_COMPL_BIGUNION

⊢ ∀sp c.
    c ≠ ∅ ∧ (∀x. x ∈ c ⇒ x ⊆ sp) ⇒
    (sp DIFF BIGUNION c = BIGINTER (IMAGE (λx. sp DIFF x) c))

GEN_COMPL_BIGUNION_IMAGE

⊢ ∀sp f.
    (∀n. f n ⊆ sp) ⇒
    (sp DIFF BIGUNION (IMAGE f 𝕌(:num)) =
     BIGINTER (IMAGE (λn. sp DIFF f n) 𝕌(:num)))

GEN_COMPL_FINITE_INTER

⊢ ∀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

⊢ ∀sp f n.
    0 < n ⇒
    (sp DIFF BIGUNION (IMAGE f (count n)) =
     BIGINTER (IMAGE (λi. sp DIFF f i) (count n)))

GEN_COMPL_INTER

⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ (sp DIFF s ∩ t = sp DIFF s ∪ (sp DIFF t))

GEN_COMPL_UNION

⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ (sp DIFF (s ∪ t) = (sp DIFF s) ∩ (sp DIFF t))

GEN_DIFF_INTER

⊢ ∀sp s t. s ⊆ sp ∧ t ⊆ sp ⇒ (s DIFF t = s ∩ (sp DIFF t))

HARMONIC_SERIES_POW_2

⊢ summable (λn. (&SUC n)² ⁻¹)

INCREASING_TO_DISJOINT_SETS

⊢ ∀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'

⊢ ∀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

⊢ ∀p e. (∃x. x ∈ p) ∧ 0 < e ⇒ ∃x. x ∈ p ∧ x < inf p + e

INF_DEF_ALT

⊢ ∀p. inf p = -sup (λr. -r ∈ p)

INF_GREATER

⊢ ∀p z. (∃x. x ∈ p) ∧ inf p < z ⇒ ∃x. x ∈ p ∧ x < z

INF_LE

⊢ ∀p r. (∃z. ∀x. x ∈ p ⇒ z ≤ x) ∧ (∃x. x ∈ p ∧ x ≤ r) ⇒ inf p ≤ r

INTER_BINARY

⊢ ∀a b. a ∩ b = BIGINTER {binary a b i | i ∈ 𝕌(:num)}

IN_FCP_CROSS

⊢ ∀s a b. s ∈ fcp_cross a b ⇔ ∃t u. (s = FCP_CONCAT t u) ∧ t ∈ a ∧ u ∈ b

IN_FCP_PROD

⊢ ∀s A B. s ∈ fcp_prod A B ⇔ ∃a b. (s = fcp_cross a b) ∧ a ∈ A ∧ b ∈ B

IN_PROD_SETS

⊢ ∀s a b. s ∈ prod_sets a b ⇔ ∃t u. (s = t × u) ∧ t ∈ a ∧ u ∈ b

IN_general_cross

⊢ ∀cons s A B.
    s ∈ general_cross cons A B ⇔ ∃a b. (s = cons a b) ∧ a ∈ A ∧ b ∈ B

IN_general_prod

⊢ ∀cons s A B.
    s ∈ general_prod cons A B ⇔
    ∃a b. (s = general_cross cons a b) ∧ a ∈ A ∧ b ∈ B

IN_o

⊢ ∀x f s. x ∈ s ∘ f ⇔ f x ∈ s

LE_INF

⊢ ∀p r. (∃x. x ∈ p) ∧ (∀x. x ∈ p ⇒ r ≤ x) ⇒ r ≤ inf p

LOGR_MONO_LE

⊢ ∀x y b. 0 < x ∧ 0 < y ∧ 1 < b ⇒ (logr b x ≤ logr b y ⇔ x ≤ y)

LOGR_MONO_LE_IMP

⊢ ∀x y b. 0 < x ∧ x ≤ y ∧ 1 ≤ b ⇒ logr b x ≤ logr b y

MINIMAL_EQ

⊢ ∀p m. p m ∧ (m = minimal p) ⇔ p m ∧ ∀n. n < m ⇒ ¬p n

MINIMAL_EQ_IMP

⊢ ∀m p. p m ∧ (∀n. n < m ⇒ ¬p n) ⇒ (m = minimal p)

MINIMAL_EXISTS

⊢ ∀P. (∃n. P n) ⇔ P (minimal P) ∧ ∀n. n < minimal P ⇒ ¬P n

MINIMAL_EXISTS0

⊢ (∃n. P n) ⇔ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m

MINIMAL_EXISTS_IMP

⊢ ∀P. (∃n. P n) ⇒ ∃m. P m ∧ ∀n. n < m ⇒ ¬P n

MINIMAL_SUC

⊢ ∀n p.
    (SUC n = minimal p) ∧ p (SUC n) ⇔
    ¬p 0 ∧ (n = minimal (p ∘ SUC)) ∧ p (SUC n)

MINIMAL_SUC_IMP

⊢ ∀n p. p (SUC n) ∧ ¬p 0 ∧ (n = minimal (p ∘ SUC)) ⇒ (SUC n = minimal p)

NUM_2D_BIJ

⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) 𝕌(:num)

NUM_2D_BIJ_INV

⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × 𝕌(:num))

NUM_2D_BIJ_NZ

⊢ ∃f. BIJ f (𝕌(:num) × (𝕌(:num) DIFF {0})) 𝕌(:num)

NUM_2D_BIJ_NZ_ALT

⊢ ∃f. BIJ f (𝕌(:num) × 𝕌(:num)) (𝕌(:num) DIFF {0})

NUM_2D_BIJ_NZ_ALT2

⊢ ∃f. BIJ f ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0})) 𝕌(:num)

NUM_2D_BIJ_NZ_ALT2_INV

⊢ ∃f. BIJ f 𝕌(:num) ((𝕌(:num) DIFF {0}) × (𝕌(:num) DIFF {0}))

NUM_2D_BIJ_NZ_ALT_INV

⊢ ∃f. BIJ f (𝕌(:num) DIFF {0}) (𝕌(:num) × 𝕌(:num))

NUM_2D_BIJ_NZ_INV

⊢ ∃f. BIJ f 𝕌(:num) (𝕌(:num) × (𝕌(:num) DIFF {0}))

NUM_2D_BIJ_nfst_nsnd

⊢ BIJ (λn. (nfst n,nsnd n)) 𝕌(:num) (𝕌(:num) × 𝕌(:num))

NUM_2D_BIJ_npair

⊢ BIJ $*,ᴾ (𝕌(:num) × 𝕌(:num)) 𝕌(:num)

PAIRED_BETA_THM

⊢ ∀f z. fᴾ z = f (FST z) (SND z)

POW_HALF_MONO

⊢ ∀m n. m ≤ n ⇒ (1 / 2) pow n ≤ (1 / 2) pow m

POW_HALF_POS

⊢ ∀n. 0 < (1 / 2) pow n

POW_HALF_SMALL

⊢ ∀e. 0 < e ⇒ ∃n. (1 / 2) pow n < e

POW_NEG_ODD

⊢ ∀x. x < 0 ⇒ (x pow n < 0 ⇔ ODD n)

POW_POS_EVEN

⊢ ∀x. x < 0 ⇒ (0 < x pow n ⇔ EVEN n)

PREIMAGE_REAL_COMPL1

⊢ ∀c. COMPL {x | c < x} = {x | x ≤ c}

PREIMAGE_REAL_COMPL2

⊢ ∀c. COMPL {x | c ≤ x} = {x | x < c}

PREIMAGE_REAL_COMPL3

⊢ ∀c. COMPL {x | x ≤ c} = {x | c < x}

PREIMAGE_REAL_COMPL4

⊢ ∀c. COMPL {x | x < c} = {x | c ≤ x}

REAL_ARCH_INV'

⊢ ∀x. 0 < x ⇒ ∃n. (&n)⁻¹ < x

REAL_ARCH_INV_SUC

⊢ ∀x. 0 < x ⇒ ∃n. (&SUC n)⁻¹ < x

REAL_LE_LT_MUL

⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 ≤ x * y

REAL_LE_RDIV_EQ_NEG

⊢ ∀x y z. z < 0 ⇒ (y / z ≤ x ⇔ x * z ≤ y)

REAL_LT_LE_MUL

⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 ≤ x * y

REAL_LT_LMUL_0_NEG

⊢ ∀x y. 0 < x * y ∧ x < 0 ⇒ y < 0

REAL_LT_LMUL_NEG_0

⊢ ∀x y. x * y < 0 ∧ 0 < x ⇒ y < 0

REAL_LT_LMUL_NEG_0_NEG

⊢ ∀x y. x * y < 0 ∧ x < 0 ⇒ 0 < y

REAL_LT_MAX_BETWEEN

⊢ ∀x b d. x < max b d ∧ b ≤ x ⇒ x < d

REAL_LT_RDIV_EQ_NEG

⊢ ∀x y z. z < 0 ⇒ (y / z < x ⇔ x * z < y)

REAL_LT_RMUL_0_NEG

⊢ ∀x y. 0 < x * y ∧ y < 0 ⇒ x < 0

REAL_LT_RMUL_NEG_0

⊢ ∀x y. x * y < 0 ∧ 0 < y ⇒ x < 0

REAL_LT_RMUL_NEG_0_NEG

⊢ ∀x y. x * y < 0 ∧ y < 0 ⇒ 0 < x

REAL_MAX_REDUCE

⊢ ∀x y. x ≤ y ∨ x < y ⇒ (max x y = y) ∧ (max y x = y)

REAL_MIN_LE_BETWEEN

⊢ ∀x a c. min a c ≤ x ∧ x < a ⇒ c ≤ x

REAL_MIN_REDUCE

⊢ ∀x y. x ≤ y ∨ x < y ⇒ (min x y = x) ∧ (min y x = x)

REAL_MUL_IDEMPOT

⊢ ∀r. (r * r = r) ⇔ (r = 0) ∨ (r = 1)

REAL_NEG_NZ

⊢ ∀x. x < 0 ⇒ x ≠ 0

REAL_SUP_LE_X

⊢ ∀P x. (∃r. P r) ∧ (∀r. P r ⇒ r ≤ x) ⇒ sup P ≤ x

REAL_X_LE_SUP

⊢ ∀P x. (∃r. P r) ∧ (∃z. ∀r. P r ⇒ r ≤ z) ∧ (∃r. P r ∧ x ≤ r) ⇒ x ≤ sup P

SETS_TO_DISJOINT_SETS

⊢ ∀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'

⊢ ∀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

⊢ ∀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'

⊢ ∀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

⊢ ∀s1 s2 s3. s1 ⊆ s2 DIFF s3 ⇒ DISJOINT s1 s3

SUBSET_DIFF_SUBSET

⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t

SUBSET_INTER_SUBSET_L

⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t

SUBSET_INTER_SUBSET_R

⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ t

SUBSET_MONO_DIFF

⊢ ∀r s t. s ⊆ t ⇒ s DIFF r ⊆ t DIFF r

SUBSET_RESTRICT_DIFF

⊢ ∀r s t. s ⊆ t ⇒ r DIFF t ⊆ r DIFF s

SUBSET_RESTRICT_L

⊢ ∀r s t. s ⊆ t ⇒ s ∩ r ⊆ t ∩ r

SUBSET_RESTRICT_R

⊢ ∀r s t. s ⊆ t ⇒ r ∩ s ⊆ r ∩ t

UNION_BINARY

⊢ ∀a b. a ∪ b = BIGUNION {binary a b i | i ∈ 𝕌(:num)}

UNION_TO_3_DISJOINT_UNIONS

⊢ ∀s t.
    (s ∪ t = s DIFF t ∪ s ∩ t ∪ (t DIFF s)) ∧
    disjoint {s DIFF t; s ∩ t; t DIFF s}

countable_disjoint_decomposition

⊢ ∀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

⊢ ∀A. disjoint A ⇔ ∀a b. a ∈ A ∧ b ∈ A ∧ a ≠ b ⇒ (a ∩ b = ∅)

disjointD

⊢ ∀A a b. disjoint A ⇒ a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b

disjointI

⊢ ∀A. (∀a b. a ∈ A ⇒ b ∈ A ⇒ a ≠ b ⇒ DISJOINT a b) ⇒ disjoint A

disjoint_empty

⊢ disjoint ∅

disjoint_family_disjoint

⊢ ∀A. disjoint_family (disjointed A)

disjoint_image

⊢ ∀f. (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒ disjoint (IMAGE f 𝕌(:α))

disjoint_insert

⊢ ∀e c. disjoint c ∧ (∀x. x ∈ c ⇒ DISJOINT x e) ⇒ disjoint (e INSERT c)

disjoint_insert_imp

⊢ ∀e c. disjoint (e INSERT c) ⇒ disjoint c

disjoint_insert_notin

⊢ ∀e c. disjoint (e INSERT c) ∧ e ∉ c ⇒ ∀s. s ∈ c ⇒ DISJOINT e s

disjoint_restrict

⊢ ∀e c. disjoint c ⇒ disjoint (IMAGE ($INTER e) c)

disjoint_same

⊢ ∀s t. (s = t) ⇒ disjoint {s; t}

disjoint_sing

⊢ ∀a. disjoint {a}

disjoint_two

⊢ ∀s t. s ≠ t ∧ DISJOINT s t ⇒ disjoint {s; t}

disjoint_union

⊢ ∀A B.
    disjoint A ∧ disjoint B ∧ (BIGUNION A ∩ BIGUNION B = ∅) ⇒ disjoint (A ∪ B)

disjointed_subset

⊢ ∀A n. disjointed A n ⊆ A n

fcp_cross_UNIV

⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒ (fcp_cross 𝕌(:α[β]) 𝕌(:α[γ]) = 𝕌(:α[β + γ]))

fcp_cross_alt

⊢ ∀A B. fcp_cross A B = general_cross FCP_CONCAT A B

fcp_prod_alt

⊢ ∀A B. fcp_prod A B = general_prod FCP_CONCAT A B

finite_decomposition

⊢ ∀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

⊢ ∀c. FINITE c ⇒ ∃f n. (∀x. x < n ⇒ f x ∈ c) ∧ (c = IMAGE f (count n))

finite_disjoint_decomposition

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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

⊢ ∀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'

⊢ ∀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

⊢ ∀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

⊢ ∀cons a b c d.
    a ⊆ b ∧ c ⊆ d ⇒ general_cross cons a c ⊆ general_cross cons b d

infinitely_often_lemma

⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n

infinity_bound_lemma

⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N

lg_1

⊢ lg 1 = 0

lg_2

⊢ lg 2 = 1

lg_inv

⊢ ∀x. 0 < x ⇒ (lg x⁻¹ = -lg x)

lg_mul

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ (lg (x * y) = lg x + lg y)

lg_nonzero

⊢ ∀x. x ≠ 0 ∧ 0 ≤ x ⇒ (lg x ≠ 0 ⇔ x ≠ 1)

lg_pow

⊢ ∀n. lg (2 pow n) = &n

logr_1

⊢ ∀b. logr b 1 = 0

logr_div

⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x / y) = logr b x − logr b y)

logr_inv

⊢ ∀b x. 0 < x ⇒ (logr b x⁻¹ = -logr b x)

logr_mul

⊢ ∀b x y. 0 < x ∧ 0 < y ⇒ (logr b (x * y) = logr b x + logr b y)

neg_lg

⊢ ∀x. 0 < x ⇒ (-lg x = lg x⁻¹)

neg_logr

⊢ ∀b x. 0 < x ⇒ (-logr b x = logr b x⁻¹)

pair_operation_FCP_CONCAT

⊢ FINITE 𝕌(:β) ∧ FINITE 𝕌(:γ) ⇒ pair_operation FCP_CONCAT FCP_FST FCP_SND

pair_operation_pair

⊢ pair_operation $, FST SND

prod_sets_alt

⊢ ∀A B. prod_sets A B = general_prod $, A B

tail_countable

⊢ ∀A m. COUNTABLE {A n | m ≤ n}

tail_not_empty

⊢ ∀A m. {A n | m ≤ n} ≠ ∅