Theory "sigma_algebra"

Signature

Definitions

algebra_def

⊢ ∀a. algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a

dynkin_def

⊢ ∀sp sts. dynkin sp sts = (sp,BIGINTER {d | sts ⊆ d ∧ dynkin_system (sp,d)})

dynkin_system_def

⊢ ∀d. dynkin_system d ⇔
      subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
      (∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
      ∀f. f ∈ (𝕌(:num) → subsets d) ∧ (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d

measurable_def

⊢ ∀a b.
    measurable a b =
    {f |
     sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
     ∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a}

prod_sigma_def

⊢ ∀a b. a × b = sigma (space a × space b) (prod_sets (subsets a) (subsets b))

ring_def

⊢ ∀r. ring r ⇔
      subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
      (∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r) ∧
      ∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r

semiring_def

⊢ ∀r. semiring r ⇔
      subset_class (space r) (subsets r) ∧ ∅ ∈ subsets r ∧
      (∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r) ∧
      ∀s t.
        s ∈ subsets r ∧ t ∈ subsets r ⇒
        ∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧ (s DIFF t = BIGUNION c)

sigma_algebra_def

⊢ ∀a. sigma_algebra a ⇔
      algebra a ∧ ∀c. COUNTABLE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

sigma_def

⊢ ∀sp sts. sigma sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ sigma_algebra (sp,s)})

sigma_function_def

⊢ ∀sp A f. sigma sp A f = (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))

sigma_functions_def

⊢ ∀sp A f J.
    sigma sp A f J =
    sigma sp
      (BIGUNION
         (IMAGE (λi. IMAGE (λs. PREIMAGE (f i) s ∩ sp) (subsets (A i))) J))

sigma_sets_def

⊢ sigma_sets =
  (λsp st a0.
       ∀sigma_sets'.
         (∀a0.
            (a0 = ∅) ∨ st a0 ∨ (∃a. (a0 = sp DIFF a) ∧ sigma_sets' a) ∨
            (∃A. (a0 = BIGUNION {A i | i ∈ 𝕌(:num)}) ∧ ∀i. sigma_sets' (A i)) ⇒
            sigma_sets' a0) ⇒
         sigma_sets' a0)

smallest_ring_def

⊢ ∀sp sts. smallest_ring sp sts = (sp,BIGINTER {s | sts ⊆ s ∧ ring (sp,s)})

space_def

⊢ ∀x y. space (x,y) = x

subset_class_def

⊢ ∀sp sts. subset_class sp sts ⇔ ∀x. x ∈ sts ⇒ x ⊆ sp

subsets_def

⊢ ∀x y. subsets (x,y) = y

Theorems

ALGEBRA_ALT_INTER

⊢ ∀a. algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a

ALGEBRA_COMPL

⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a

ALGEBRA_COMPL_SETS

⊢ ∀sp sts a. algebra (sp,sts) ∧ a ∈ sts ⇒ sp DIFF a ∈ sts

ALGEBRA_DIFF

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s DIFF t ∈ subsets a

ALGEBRA_EMPTY

⊢ ∀a. algebra a ⇒ ∅ ∈ subsets a

ALGEBRA_FINITE_UNION

⊢ ∀a c. algebra a ∧ FINITE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

ALGEBRA_IMP_RING

⊢ ∀a. algebra a ⇒ ring a

ALGEBRA_IMP_SEMIRING

⊢ ∀a. algebra a ⇒ semiring a

ALGEBRA_INTER

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a

ALGEBRA_INTER_SPACE

⊢ ∀a s. algebra a ∧ s ∈ subsets a ⇒ (space a ∩ s = s) ∧ (s ∩ space a = s)

ALGEBRA_RESTRICT

⊢ ∀sp sts a. algebra (sp,sts) ∧ a ∈ sts ⇒ algebra (a,IMAGE (λs. s ∩ a) sts)

ALGEBRA_SETS_COLLECT_CONST

⊢ ∀sp sts P. algebra (sp,sts) ⇒ {x | x ∈ sp ∧ P} ∈ sts

ALGEBRA_SETS_COLLECT_IMP

⊢ ∀sp sts P Q.
    algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒
    {x | x ∈ sp ∧ Q x} ∈ sts ⇒
    {x | x ∈ sp ∧ (Q x ⇒ P x)} ∈ sts

ALGEBRA_SETS_COLLECT_NEG

⊢ ∀sp sts P.
    algebra (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ⇒ {x | x ∈ sp ∧ ¬P x} ∈ sts

ALGEBRA_SINGLE_SET

⊢ ∀X S. X ⊆ S ⇒ algebra (S,{∅; X; S DIFF X; S})

ALGEBRA_SPACE

⊢ ∀a. algebra a ⇒ space a ∈ subsets a

ALGEBRA_UNION

⊢ ∀a s t. algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a

DYNKIN

⊢ ∀sp sts.
    subset_class sp sts ⇒
    sts ⊆ subsets (dynkin sp sts) ∧ dynkin_system (dynkin sp sts) ∧
    subset_class sp (subsets (dynkin sp sts))

DYNKIN_LEMMA

⊢ ∀d. dynkin_system d ∧
      (∀s t. s ∈ subsets d ∧ t ∈ subsets d ⇒ s ∩ t ∈ subsets d) ⇔
      sigma_algebra d

DYNKIN_MONOTONE

⊢ ∀sp a b. a ⊆ b ⇒ subsets (dynkin sp a) ⊆ subsets (dynkin sp b)

DYNKIN_SMALLEST

⊢ ∀sp sts D.
    sts ⊆ D ∧ D ⊆ subsets (dynkin sp sts) ∧ dynkin_system (sp,D) ⇒
    (D = subsets (dynkin sp sts))

DYNKIN_STABLE

⊢ ∀d. dynkin_system d ⇒ (dynkin (space d) (subsets d) = d)

DYNKIN_STABLE_LEMMA

⊢ ∀sp sts. dynkin_system (sp,sts) ⇒ (dynkin sp sts = (sp,sts))

DYNKIN_SUBSET

⊢ ∀a b.
    dynkin_system b ∧ a ⊆ subsets b ⇒ subsets (dynkin (space b) a) ⊆ subsets b

DYNKIN_SUBSET_SIGMA

⊢ ∀sp sts.
    subset_class sp sts ⇒ subsets (dynkin sp sts) ⊆ subsets (sigma sp sts)

DYNKIN_SUBSET_SUBSETS

⊢ ∀sp a. a ⊆ subsets (dynkin sp a)

DYNKIN_SYSTEM_ALT

⊢ ∀d. dynkin_system d ⇔
      subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
      (∀s. s ∈ subsets d ⇒ space d DIFF s ∈ subsets d) ∧
      (∀f. f ∈ (𝕌(:num) → subsets d) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
           BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d) ∧
      ∀f. f ∈ (𝕌(:num) → subsets d) ∧ (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d

DYNKIN_SYSTEM_ALT_MONO

⊢ ∀d. dynkin_system d ⇔
      subset_class (space d) (subsets d) ∧ space d ∈ subsets d ∧
      (∀s t. s ∈ subsets d ∧ t ∈ subsets d ∧ s ⊆ t ⇒ t DIFF s ∈ subsets d) ∧
      ∀f. f ∈ (𝕌(:num) → subsets d) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d

DYNKIN_SYSTEM_COMPL

⊢ ∀d s. dynkin_system d ∧ s ∈ subsets d ⇒ space d DIFF s ∈ subsets d

DYNKIN_SYSTEM_COUNTABLY_DUNION

⊢ ∀d f.
    dynkin_system d ∧ f ∈ (𝕌(:num) → subsets d) ∧
    (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets d

DYNKIN_SYSTEM_DUNION

⊢ ∀d s t.
    dynkin_system d ∧ s ∈ subsets d ∧ t ∈ subsets d ∧ DISJOINT s t ⇒
    s ∪ t ∈ subsets d

DYNKIN_SYSTEM_EMPTY

⊢ ∀d. dynkin_system d ⇒ ∅ ∈ subsets d

DYNKIN_SYSTEM_INCREASING

⊢ ∀p f.
    dynkin_system p ∧ f ∈ (𝕌(:num) → subsets p) ∧ (f 0 = ∅) ∧
    (∀n. f n ⊆ f (SUC n)) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets p

DYNKIN_SYSTEM_SPACE

⊢ ∀d. dynkin_system d ⇒ space d ∈ subsets d

DYNKIN_THM

⊢ ∀sp sts.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ⇒
    (dynkin sp sts = sigma sp sts)

INTER_SPACE_EQ1

⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ (sp ∩ x = x)

INTER_SPACE_REDUCE

⊢ ∀sp sts. subset_class sp sts ⇒ ∀x. x ∈ sts ⇒ (x ∩ sp = x)

IN_DYNKIN

⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (dynkin sp a)

IN_MEASURABLE

⊢ ∀a b f.
    f ∈ measurable a b ⇔
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
    ∀s. s ∈ subsets b ⇒ PREIMAGE f s ∩ space a ∈ subsets a

IN_SIGMA

⊢ ∀sp a x. x ∈ a ⇒ x ∈ subsets (sigma sp a)

MEASUBABLE_BIGUNION_LEMMA

⊢ ∀a b f.
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
    (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
    ∀c. COUNTABLE c ∧ c ⊆ IMAGE (PREIMAGE f) (subsets b) ⇒
        BIGUNION c ∈ IMAGE (PREIMAGE f) (subsets b)

MEASURABLE_BIGUNION_PROPERTY

⊢ ∀a b f.
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
    (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
    ∀c. c ⊆ subsets b ⇒
        (PREIMAGE f (BIGUNION c) = BIGUNION (IMAGE (PREIMAGE f) c))

MEASURABLE_COMP

⊢ ∀f g a b c. f ∈ measurable a b ∧ g ∈ measurable b c ⇒ g ∘ f ∈ measurable a c

MEASURABLE_COMP_STRONG

⊢ ∀f g a b c.
    f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b → space c) ∧
    (∀x. x ∈ subsets c ⇒ PREIMAGE g x ∩ IMAGE f (space a) ∈ subsets b) ⇒
    g ∘ f ∈ measurable a c

MEASURABLE_COMP_STRONGER

⊢ ∀f g a b c t.
    f ∈ measurable a b ∧ sigma_algebra c ∧ g ∈ (space b → space c) ∧
    IMAGE f (space a) ⊆ t ∧ (∀s. s ∈ subsets c ⇒ PREIMAGE g s ∩ t ∈ subsets b) ⇒
    g ∘ f ∈ measurable a c

MEASURABLE_DIFF_PROPERTY

⊢ ∀a b f.
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
    (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
    ∀s. s ∈ subsets b ⇒
        (PREIMAGE f (space b DIFF s) = space a DIFF PREIMAGE f s)

MEASURABLE_I

⊢ ∀a. sigma_algebra a ⇒ I ∈ measurable a a

MEASURABLE_LIFT

⊢ ∀f a b. f ∈ measurable a b ⇒ f ∈ measurable a (sigma (space b) (subsets b))

MEASURABLE_PROD_SIGMA

⊢ ∀a a1 a2 f.
    sigma_algebra a ∧ FST ∘ f ∈ measurable a a1 ∧ SND ∘ f ∈ measurable a a2 ⇒
    f ∈
    measurable a
      (sigma (space a1 × space a2) (prod_sets (subsets a1) (subsets a2)))

MEASURABLE_PROD_SIGMA'

⊢ ∀a a1 a2 f.
    sigma_algebra a ∧ FST ∘ f ∈ measurable a a1 ∧ SND ∘ f ∈ measurable a a2 ⇒
    f ∈ measurable a (a1 × a2)

MEASURABLE_SIGMA

⊢ ∀f a b sp.
    sigma_algebra a ∧ subset_class sp b ∧ f ∈ (space a → sp) ∧
    (∀s. s ∈ b ⇒ PREIMAGE f s ∩ space a ∈ subsets a) ⇒
    f ∈ measurable a (sigma sp b)

MEASURABLE_SIGMA_PREIMAGES

⊢ ∀a b f.
    sigma_algebra a ∧ sigma_algebra b ∧ f ∈ (space a → space b) ∧
    (∀s. s ∈ subsets b ⇒ PREIMAGE f s ∈ subsets a) ⇒
    sigma_algebra (space a,IMAGE (PREIMAGE f) (subsets b))

MEASURABLE_SUBSET

⊢ ∀a b. measurable a b ⊆ measurable a (sigma (space b) (subsets b))

MEASURABLE_UP_LIFT

⊢ ∀sp a b c f.
    f ∈ measurable (sp,a) c ∧ sigma_algebra (sp,b) ∧ a ⊆ b ⇒
    f ∈ measurable (sp,b) c

MEASURABLE_UP_SIGMA

⊢ ∀a b. measurable a b ⊆ measurable (sigma (space a) (subsets a)) b

MEASURABLE_UP_SUBSET

⊢ ∀sp a b c.
    a ⊆ b ∧ sigma_algebra (sp,b) ⇒ measurable (sp,a) c ⊆ measurable (sp,b) c

POW_ALGEBRA

⊢ ∀sp. algebra (sp,POW sp)

POW_SIGMA_ALGEBRA

⊢ ∀sp. sigma_algebra (sp,POW sp)

PREIMAGE_SIGMA

⊢ ∀Z sp sts f.
    subset_class sp sts ∧ f ∈ (Z → sp) ⇒
    (IMAGE (λs. PREIMAGE f s ∩ Z) (subsets (sigma sp sts)) =
     subsets (sigma Z (IMAGE (λs. PREIMAGE f s ∩ Z) sts)))

PREIMAGE_SIGMA_ALGEBRA

⊢ ∀sp A f.
    sigma_algebra A ∧ f ∈ (sp → space A) ⇒
    sigma_algebra (sp,IMAGE (λs. PREIMAGE f s ∩ sp) (subsets A))

RING_BIGUNION

⊢ ∀sp sts A n.
    ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i < n} ∈ sts

RING_DIFF

⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s DIFF t ∈ subsets r

RING_DIFF_ALT

⊢ ∀a b sp sts. ring (sp,sts) ∧ a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts

RING_EMPTY

⊢ ∀r. ring r ⇒ ∅ ∈ subsets r

RING_FINITE_BIGUNION1

⊢ ∀X sp sts. ring (sp,sts) ∧ FINITE X ⇒ X ⊆ sts ⇒ BIGUNION X ∈ sts

RING_FINITE_BIGUNION2

⊢ ∀A N sp sts.
    ring (sp,sts) ∧ FINITE N ∧ (∀i. i ∈ N ⇒ A i ∈ sts) ⇒
    BIGUNION {A i | i ∈ N} ∈ sts

RING_FINITE_INTER

⊢ ∀r f n.
    ring r ∧ 0 < n ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
    BIGINTER (IMAGE f (count n)) ∈ subsets r

RING_FINITE_UNION

⊢ ∀r c. ring r ∧ c ⊆ subsets r ∧ FINITE c ⇒ BIGUNION c ∈ subsets r

RING_FINITE_UNION_ALT

⊢ ∀r f n.
    ring r ∧ (∀i. i < n ⇒ f i ∈ subsets r) ⇒
    BIGUNION (IMAGE f (count n)) ∈ subsets r

RING_IMP_SEMIRING

⊢ ∀r. ring r ⇒ semiring r

RING_INSERT

⊢ ∀x A sp sts. ring (sp,sts) ∧ {x} ∈ sts ∧ A ∈ sts ⇒ x INSERT A ∈ sts

RING_INTER

⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r

RING_SETS_COLLECT_FINITE

⊢ ∀sp sts s P.
    ring (sp,sts) ∧ (∀i. i ∈ s ⇒ {x | x ∈ sp ∧ P i x} ∈ sts) ∧ FINITE s ⇒
    {x | x ∈ sp ∧ ∃i. i ∈ s ∧ P i x} ∈ sts

RING_SPACE_IMP_ALGEBRA

⊢ ∀r. ring r ∧ space r ∈ subsets r ⇒ algebra r

RING_UNION

⊢ ∀r s t. ring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r

SEMIRING_DIFF

⊢ ∀r s t.
    semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
    ∃c. c ⊆ subsets r ∧ FINITE c ∧ disjoint c ∧ (s DIFF t = BIGUNION c)

SEMIRING_DIFF_ALT

⊢ ∀r s t.
    semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒
    ∃f n.
      (∀i. i < n ⇒ f i ∈ subsets r) ∧
      (∀i j. i < n ∧ j < n ∧ i ≠ j ⇒ DISJOINT (f i) (f j)) ∧
      (s DIFF t = BIGUNION (IMAGE f (count n)))

SEMIRING_EMPTY

⊢ ∀r. semiring r ⇒ ∅ ∈ subsets r

SEMIRING_INTER

⊢ ∀r s t. semiring r ∧ s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∩ t ∈ subsets r

SEMIRING_PROD_SETS

⊢ ∀a b.
    semiring a ∧ semiring b ⇒
    semiring (space a × space b,prod_sets (subsets a) (subsets b))

SEMIRING_PROD_SETS'

⊢ ∀a b.
    sigma_algebra a ∧ sigma_algebra b ⇒
    semiring (space a × space b,prod_sets (subsets a) (subsets b))

SEMIRING_SETS_COLLECT

⊢ ∀sp sts P Q.
    semiring (sp,sts) ∧ {x | x ∈ sp ∧ P x} ∈ sts ∧ {x | x ∈ sp ∧ Q x} ∈ sts ⇒
    {x | x ∈ sp ∧ P x ∧ Q x} ∈ sts

SIGMA_ALGEBRA

⊢ ∀p. sigma_algebra p ⇔
      subset_class (space p) (subsets p) ∧ ∅ ∈ subsets p ∧
      (∀s. s ∈ subsets p ⇒ space p DIFF s ∈ subsets p) ∧
      ∀c. COUNTABLE c ∧ c ⊆ subsets p ⇒ BIGUNION c ∈ subsets p

SIGMA_ALGEBRA_ALGEBRA

⊢ ∀a. sigma_algebra a ⇒ algebra a

SIGMA_ALGEBRA_ALT

⊢ ∀a. sigma_algebra a ⇔
      algebra a ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALT_DISJOINT

⊢ ∀a. sigma_algebra a ⇔
      algebra a ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALT_MONO

⊢ ∀a. sigma_algebra a ⇔
      algebra a ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_ALT_SPACE

⊢ ∀a. sigma_algebra a ⇔
      subset_class (space a) (subsets a) ∧ space a ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_COMPL

⊢ ∀a s. sigma_algebra a ∧ s ∈ subsets a ⇒ space a DIFF s ∈ subsets a

SIGMA_ALGEBRA_COUNTABLE_INT

⊢ ∀sp sts A X.
    sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ X ≠ ∅ ⇒
    BIGINTER {A x | x ∈ X} ∈ sts

SIGMA_ALGEBRA_COUNTABLE_INT'

⊢ ∀sp sts A X.
    sigma_algebra (sp,sts) ∧ COUNTABLE X ∧ X ≠ ∅ ∧ IMAGE A X ⊆ sts ⇒
    BIGINTER {A x | x ∈ X} ∈ sts

SIGMA_ALGEBRA_COUNTABLE_UN

⊢ ∀sp sts A X.
    sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ⇒ BIGUNION {A x | x ∈ X} ∈ sts

SIGMA_ALGEBRA_COUNTABLE_UN'

⊢ ∀sp sts A X.
    sigma_algebra (sp,sts) ∧ IMAGE A X ⊆ sts ∧ COUNTABLE X ⇒
    BIGUNION {A x | x ∈ X} ∈ sts

SIGMA_ALGEBRA_COUNTABLE_UNION

⊢ ∀a c. sigma_algebra a ∧ COUNTABLE c ∧ c ⊆ subsets a ⇒ BIGUNION c ∈ subsets a

SIGMA_ALGEBRA_DIFF

⊢ ∀a s t.
    sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s DIFF t ∈ subsets a

SIGMA_ALGEBRA_EMPTY

⊢ ∀a. sigma_algebra a ⇒ ∅ ∈ subsets a

SIGMA_ALGEBRA_ENUM

⊢ ∀a f.
    sigma_algebra a ∧ f ∈ (𝕌(:num) → subsets a) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_FN

⊢ ∀a. sigma_algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ⇒ BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_FN_BIGINTER

⊢ ∀a. sigma_algebra a ⇒
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ⇒ BIGINTER (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_FN_DISJOINT

⊢ ∀a. sigma_algebra a ⇔
      subset_class (space a) (subsets a) ∧ ∅ ∈ subsets a ∧
      (∀s. s ∈ subsets a ⇒ space a DIFF s ∈ subsets a) ∧
      (∀s t. s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a) ∧
      ∀f. f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
          BIGUNION (IMAGE f 𝕌(:num)) ∈ subsets a

SIGMA_ALGEBRA_IMP_DYNKIN_SYSTEM

⊢ ∀a. sigma_algebra a ⇒ dynkin_system a

SIGMA_ALGEBRA_INTER

⊢ ∀a s t. sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∩ t ∈ subsets a

SIGMA_ALGEBRA_PROD_SIGMA

⊢ ∀a b.
    subset_class (space a) (subsets a) ∧ subset_class (space b) (subsets b) ⇒
    sigma_algebra (a × b)

SIGMA_ALGEBRA_PROD_SIGMA'

⊢ ∀X Y A B.
    subset_class X A ∧ subset_class Y B ⇒ sigma_algebra ((X,A) × (Y,B))

SIGMA_ALGEBRA_RESTRICT

⊢ ∀sp sts a.
    sigma_algebra (sp,sts) ∧ a ∈ sts ⇒ sigma_algebra (a,IMAGE (λs. s ∩ a) sts)

SIGMA_ALGEBRA_RESTRICT_SUBSET

⊢ ∀sp sts a. sigma_algebra (sp,sts) ∧ a ∈ sts ⇒ IMAGE (λs. s ∩ a) sts ⊆ sts

SIGMA_ALGEBRA_SIGMA

⊢ ∀sp sts. subset_class sp sts ⇒ sigma_algebra (sigma sp sts)

SIGMA_ALGEBRA_SPACE

⊢ ∀a. sigma_algebra a ⇒ space a ∈ subsets a

SIGMA_ALGEBRA_UNION

⊢ ∀a s t. sigma_algebra a ∧ s ∈ subsets a ∧ t ∈ subsets a ⇒ s ∪ t ∈ subsets a

SIGMA_CONG

⊢ ∀sp a b.
    (subsets (sigma sp a) = subsets (sigma sp b)) ⇒ (sigma sp a = sigma sp b)

SIGMA_MEASURABLE

⊢ ∀sp A f.
    sigma_algebra A ∧ f ∈ (sp → space A) ⇒ f ∈ measurable (sigma sp A f) A

SIGMA_MONOTONE

⊢ ∀sp a b. a ⊆ b ⇒ subsets (sigma sp a) ⊆ subsets (sigma sp b)

SIGMA_POW

⊢ ∀s. sigma s (POW s) = (s,POW s)

SIGMA_PROPERTY

⊢ ∀sp p a.
    subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
    (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
    (∀c. COUNTABLE c ∧ c ⊆ p ∩ subsets (sigma sp a) ⇒ BIGUNION c ∈ p) ⇒
    subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_ALT

⊢ ∀sp p a.
    subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
    (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
    subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_DISJOINT

⊢ ∀sp p a.
    algebra (sp,a) ∧ a ⊆ p ∧
    (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧ (f 0 = ∅) ∧
         (∀n. f n ⊆ f (SUC n)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧
         (∀i j. i ≠ j ⇒ DISJOINT (f i) (f j)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
    subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_DISJOINT_LEMMA

⊢ ∀sp a d.
    algebra (sp,a) ∧ a ⊆ d ∧ dynkin_system (sp,d) ⇒ subsets (sigma sp a) ⊆ d

SIGMA_PROPERTY_DISJOINT_LEMMA1

⊢ ∀sp sts.
    algebra (sp,sts) ⇒
    ∀s t.
      s ∈ sts ∧ t ∈ subsets (dynkin sp sts) ⇒ s ∩ t ∈ subsets (dynkin sp sts)

SIGMA_PROPERTY_DISJOINT_LEMMA2

⊢ ∀sp sts.
    algebra (sp,sts) ⇒
    ∀s t.
      s ∈ subsets (dynkin sp sts) ∧ t ∈ subsets (dynkin sp sts) ⇒
      s ∩ t ∈ subsets (dynkin sp sts)

SIGMA_PROPERTY_DISJOINT_WEAK

⊢ ∀sp p a.
    subset_class sp p ∧ ∅ ∈ p ∧ a ⊆ p ∧
    (∀s. s ∈ p ∩ subsets (sigma sp a) ⇒ sp DIFF s ∈ p) ∧
    (∀s t. s ∈ p ∧ t ∈ p ⇒ s ∪ t ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p ∩ subsets (sigma sp a)) ∧
         (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
    subsets (sigma sp a) ⊆ p

SIGMA_PROPERTY_DISJOINT_WEAK_ALT

⊢ ∀sp p a.
    algebra (sp,a) ∧ a ⊆ p ∧ subset_class sp p ∧ (∀s. s ∈ p ⇒ sp DIFF s ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p) ∧ (f 0 = ∅) ∧ (∀n. f n ⊆ f (SUC n)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ∧
    (∀f. f ∈ (𝕌(:num) → p) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
         BIGUNION (IMAGE f 𝕌(:num)) ∈ p) ⇒
    subsets (sigma sp a) ⊆ p

SIGMA_REDUCE

⊢ ∀sp a. (sp,subsets (sigma sp a)) = sigma sp a

SIGMA_SIMULTANEOUSLY_MEASURABLE

⊢ ∀sp A f J.
    (∀i. i ∈ J ⇒ sigma_algebra (A i)) ∧ (∀i. f i ∈ (sp → space (A i))) ⇒
    ∀i. i ∈ J ⇒ f i ∈ measurable (sigma sp A f J) (A i)

SIGMA_SMALLEST

⊢ ∀sp sts A.
    sts ⊆ A ∧ A ⊆ subsets (sigma sp sts) ∧ sigma_algebra (sp,A) ⇒
    (A = subsets (sigma sp sts))

SIGMA_STABLE

⊢ ∀a. sigma_algebra a ⇒ (sigma (space a) (subsets a) = a)

SIGMA_STABLE_LEMMA

⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ (sigma sp sts = (sp,sts))

SIGMA_SUBSET

⊢ ∀a b.
    sigma_algebra b ∧ a ⊆ subsets b ⇒ subsets (sigma (space b) a) ⊆ subsets b

SIGMA_SUBSET_SUBSETS

⊢ ∀sp a. a ⊆ subsets (sigma sp a)

SMALLEST_RING

⊢ ∀sp sts. subset_class sp sts ⇒ ring (smallest_ring sp sts)

SMALLEST_RING_OF_SEMIRING

⊢ ∀sp sts.
    semiring (sp,sts) ⇒
    (subsets (smallest_ring sp sts) =
     {BIGUNION c | c ⊆ sts ∧ FINITE c ∧ disjoint c})

SMALLEST_RING_SUBSET_SUBSETS

⊢ ∀sp a. a ⊆ subsets (smallest_ring sp a)

SPACE

⊢ ∀a. (space a,subsets a) = a

SPACE_DYNKIN

⊢ ∀sp sts. space (dynkin sp sts) = sp

SPACE_PROD_SIGMA

⊢ ∀a b. space (a × b) = space a × space b

SPACE_SIGMA

⊢ ∀sp a. space (sigma sp a) = sp

SPACE_SMALLEST_RING

⊢ ∀sp sts. space (smallest_ring sp sts) = sp

UNIV_SIGMA_ALGEBRA

⊢ sigma_algebra (𝕌(:α),𝕌(:α -> bool))

algebra_alt

⊢ ∀sp sts. algebra (sp,sts) ⇔ ring (sp,sts) ∧ sp ∈ sts

algebra_alt_inter

⊢ ∀sp sts.
    algebra (sp,sts) ⇔
    sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
    ∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∩ b ∈ sts

algebra_alt_union

⊢ ∀sp sts.
    algebra (sp,sts) ⇔
    sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a. a ∈ sts ⇒ sp DIFF a ∈ sts) ∧
    ∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts

prod_sigma_alt_sigma_functions

⊢ ∀A B.
    sigma_algebra A ∧ sigma_algebra B ⇒
    (A × B = sigma (space A × space B) (binary A B) (binary FST SND) {0; 1})

ring_alt

⊢ ring (sp,sts) ⇔
  subset_class sp sts ∧ ∅ ∈ sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
  ∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts

ring_alt_pow

⊢ ∀sp sts.
    ring (sp,sts) ⇔
    sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∪ t ∈ sts) ∧
    ∀s t. s ∈ sts ∧ t ∈ sts ⇒ s DIFF t ∈ sts

ring_alt_pow_imp

⊢ ∀sp sts.
    sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀a b. a ∈ sts ∧ b ∈ sts ⇒ a ∪ b ∈ sts) ∧
    (∀a b. a ∈ sts ∧ b ∈ sts ⇒ a DIFF b ∈ sts) ⇒
    ring (sp,sts)

ring_and_semiring

⊢ ∀r. ring r ⇔
      semiring r ∧ ∀s t. s ∈ subsets r ∧ t ∈ subsets r ⇒ s ∪ t ∈ subsets r

ring_disjointed_sets

⊢ ∀sp sts A.
    ring (sp,sts) ∧ IMAGE A 𝕌(:num) ⊆ sts ⇒
    IMAGE (λn. disjointed A n) 𝕌(:num) ⊆ sts

semiring_alt

⊢ semiring (sp,sts) ⇔
  subset_class sp sts ∧ ∅ ∈ sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
  ∀s t.
    s ∈ sts ∧ t ∈ sts ⇒
    ∃c. c ⊆ sts ∧ FINITE c ∧ disjoint c ∧ (s DIFF t = BIGUNION c)

sigma_algebra_alt

⊢ ∀sp sts.
    sigma_algebra (sp,sts) ⇔
    algebra (sp,sts) ∧
    ∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts

sigma_algebra_alt_pow

⊢ ∀sp sts.
    sigma_algebra (sp,sts) ⇔
    sts ⊆ POW sp ∧ ∅ ∈ sts ∧ (∀s. s ∈ sts ⇒ sp DIFF s ∈ sts) ∧
    ∀A. IMAGE A 𝕌(:num) ⊆ sts ⇒ BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sts

sigma_algebra_sigma_sets

⊢ ∀sp st. st ⊆ POW sp ⇒ sigma_algebra (sp,sigma_sets sp st)

sigma_sets_BIGINTER

⊢ ∀sp st A.
    st ⊆ POW sp ⇒
    (∀i. A i ∈ sigma_sets sp st) ⇒
    BIGINTER {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st

sigma_sets_BIGINTER2

⊢ ∀sp st A N.
    st ⊆ POW sp ∧ (∀i. i ∈ N ⇒ A i ∈ sigma_sets sp st) ∧ N ≠ ∅ ⇒
    BIGINTER {A i | i ∈ N} ∈ sigma_sets sp st

sigma_sets_BIGUNION

⊢ ∀sp st A.
    (∀i. A i ∈ sigma_sets sp st) ⇒
    BIGUNION {A i | i ∈ 𝕌(:num)} ∈ sigma_sets sp st

sigma_sets_basic

⊢ ∀sp st a. a ∈ st ⇒ a ∈ sigma_sets sp st

sigma_sets_cases

⊢ ∀sp st a0.
    sigma_sets sp st a0 ⇔
    (a0 = ∅) ∨ st a0 ∨ (∃a. (a0 = sp DIFF a) ∧ sigma_sets sp st a) ∨
    ∃A. (a0 = BIGUNION {A i | i ∈ 𝕌(:num)}) ∧ ∀i. sigma_sets sp st (A i)

sigma_sets_compl

⊢ ∀sp st a. a ∈ sigma_sets sp st ⇒ sp DIFF a ∈ sigma_sets sp st

sigma_sets_empty

⊢ ∀sp st. ∅ ∈ sigma_sets sp st

sigma_sets_fixpoint

⊢ ∀sp sts. sigma_algebra (sp,sts) ⇒ (sigma_sets sp sts = sts)

sigma_sets_ind

⊢ ∀sp st sigma_sets'.
    sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
    (∀a. sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
    (∀A. (∀i. sigma_sets' (A i)) ⇒ sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
    ∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0

sigma_sets_into_sp

⊢ ∀sp st. st ⊆ POW sp ⇒ ∀x. x ∈ sigma_sets sp st ⇒ x ⊆ sp

sigma_sets_least_sigma_algebra

⊢ ∀sp A.
    A ⊆ POW sp ⇒
    (sigma_sets sp A = BIGINTER {B | A ⊆ B ∧ sigma_algebra (sp,B)})

sigma_sets_rules

⊢ ∀sp st.
    sigma_sets sp st ∅ ∧ (∀a. st a ⇒ sigma_sets sp st a) ∧
    (∀a. sigma_sets sp st a ⇒ sigma_sets sp st (sp DIFF a)) ∧
    ∀A. (∀i. sigma_sets sp st (A i)) ⇒
        sigma_sets sp st (BIGUNION {A i | i ∈ 𝕌(:num)})

sigma_sets_strongind

⊢ ∀sp st sigma_sets'.
    sigma_sets' ∅ ∧ (∀a. st a ⇒ sigma_sets' a) ∧
    (∀a. sigma_sets sp st a ∧ sigma_sets' a ⇒ sigma_sets' (sp DIFF a)) ∧
    (∀A. (∀i. sigma_sets sp st (A i) ∧ sigma_sets' (A i)) ⇒
         sigma_sets' (BIGUNION {A i | i ∈ 𝕌(:num)})) ⇒
    ∀a0. sigma_sets sp st a0 ⇒ sigma_sets' a0

sigma_sets_subset

⊢ ∀sp sts st. sigma_algebra (sp,sts) ∧ st ⊆ sts ⇒ sigma_sets sp st ⊆ sts

sigma_sets_superset_generator

⊢ ∀X A. A ⊆ sigma_sets X A

sigma_sets_top

⊢ ∀sp A. sp ∈ sigma_sets sp A

sigma_sets_union

⊢ ∀sp st a b.
    a ∈ sigma_sets sp st ∧ b ∈ sigma_sets sp st ⇒ a ∪ b ∈ sigma_sets sp st

subset_class_POW

⊢ ∀sp. subset_class sp (POW sp)