Theory sigma_algebra

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

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

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

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

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

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

⊢ ∀a f.
    exhausting_sequence a f ⇔
    f ∈ (𝕌(:num) → subsets a) ∧ (∀n. f n ⊆ f (SUC n)) ∧
    BIGUNION (IMAGE f 𝕌(:num)) = space a

⊢ ∀top. general_borel top = sigma (topspace top) (open_in top)

⊢ ∀a. has_exhausting_sequence a ⇔ ∃f. exhausting_sequence a f

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

⊢ ∀p. pi_system p ⇔
      subset_class (space p) (subsets p) ∧ subsets p ≠ ∅ ∧
      ∀s t. s ∈ subsets p ∧ t ∈ subsets p ⇒ s ∩ t ∈ subsets p

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

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

⊢ ∀A sp.
    restrict_algebra A sp = (sp ∩ space A,IMAGE (λa. a ∩ sp) (subsets A))

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

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

⊢ ∀E. liminf E = BIGUNION (IMAGE (λm. BIGINTER {E n | m ≤ n}) 𝕌(:num))

⊢ ∀E. limsup E = BIGINTER (IMAGE (λm. BIGUNION {E n | m ≤ n}) 𝕌(:num))

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀a. algebra a ⇒ ∅ ∈ subsets a

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

⊢ ∀a c.
    algebra a ∧ FINITE c ∧ c ⊆ subsets a ∧ c ≠ ∅ ⇒ BIGINTER c ∈ subsets a

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

⊢ ∀a. algebra a ⇒ ring a

⊢ ∀a. algebra a ⇒ semiring a

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

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

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

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

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

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

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

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

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

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

⊢ ∀f s d.
    s ≠ ∅ ⇒ BIGINTER (IMAGE f s) ∩ d = BIGINTER (IMAGE (λi. f i ∩ d) s)

⊢ ∀f s d.
    s ≠ ∅ ⇒ d ∩ BIGINTER (IMAGE f s) = BIGINTER (IMAGE (λi. d ∩ f i) s)

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

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

⊢ ∀f g.
    (∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
    BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))

⊢ ∀f g s.
    BIGUNION (IMAGE f s) ∪ BIGUNION (IMAGE g s) =
    BIGUNION (IMAGE (λi. f i ∪ g i) s)

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

⊢ ∀f s d. BIGUNION (IMAGE f s) DIFF d = BIGUNION (IMAGE (λi. f i DIFF d) s)

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

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

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

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

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

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

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

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

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

⊢ ∀sts f.
    (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (𝕌(:num) → sts) ⇒
    ∀n. 0 < n ⇒ BIGINTER (IMAGE f (count n)) ∈ sts

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀d. dynkin_system d ⇒ ∅ ∈ subsets d

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

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

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

⊢ ∀s t. FINITE {s; t}

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

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

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

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

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

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

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

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

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

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

⊢ ∀sp sts f.
    subset_class sp sts ∧ BIJ f sp (IMAGE f sp) ⇒
    IMAGE (IMAGE f) (subsets (sigma sp sts)) =
    subsets (sigma (IMAGE f sp) (IMAGE (IMAGE f) sts))

⊢ ∀sp sts f.
    sigma_algebra (sp,sts) ∧ BIJ f sp (IMAGE f sp) ⇒
    sigma_algebra (IMAGE f sp,IMAGE (IMAGE f) sts)

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

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

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

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

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

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

⊢ ∀A x. x ∈ liminf A ⇔ ∃m. ∀n. m ≤ n ⇒ x ∈ A n

⊢ ∀A x. x ∈ limsup A ⇔ ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ x ∈ A n

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

⊢ ∀f g h a b c.
    f ∈ measurable a b ∧ g ∈ measurable b c ∧
    (∀x. x ∈ space a ⇒ h x = g (f x)) ⇒
    h ∈ measurable a c

⊢ ∀a b c d f g.
    a = c ∧ b = d ∧ (∀x. x ∈ space c ⇒ f x = g x) ⇒
    (f ∈ measurable a b ⇔ g ∈ measurable c d)

⊢ ∀a b c f.
    sigma_algebra a ∧ c ∈ space b ∧ (∀x. x ∈ space a ⇒ f x = c) ⇒
    f ∈ measurable a b

⊢ ∀a b f g.
    f ∈ measurable a b ∧ (∀x. x ∈ space a ⇒ g x = f x) ⇒ g ∈ measurable a b

⊢ ∀a b c f.
    sigma_algebra a ∧ sigma_algebra b ∧ sigma_algebra c ∧
    f ∈ measurable (a × b) c ⇒
    (∀y. y ∈ space b ⇒ (λx. f (x,y)) ∈ measurable a c) ∧
    ∀x. x ∈ space a ⇒ (λy. f (x,y)) ∈ measurable b c

⊢ ∀a bx by fx fy f.
    sigma_algebra a ∧ subset_class (space bx) (subsets bx) ∧
    subset_class (space by) (subsets by) ∧ fx ∈ measurable a bx ∧
    fy ∈ measurable a by ∧ (∀z. z ∈ space a ⇒ f z = (fx z,fy z)) ⇒
    f ∈ measurable a (bx × by)

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

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

⊢ ∀a b z. z ∈ space (a × b) ⇔ FST z ∈ space a ∧ SND z ∈ space b

⊢ ∀E. COMPL (liminf E) = limsup (COMPL ∘ E)

⊢ ∀sp E. (∀n. E n ⊆ sp) ⇒ sp DIFF liminf E = limsup (λn. sp DIFF E n)

⊢ ∀A B. (∀y n. y ∈ A n ⇒ ∃m. n ≤ m ∧ y ∈ B m) ⇒ limsup A ⊆ limsup B

⊢ ∀A B. (∃d. ∀y n. y ∈ A n ⇒ ∃m. n − d ≤ m ∧ y ∈ B m) ⇒ limsup A ⊆ limsup B

⊢ ∀A B. (∀n. A n ⊆ B n) ⇒ limsup A ⊆ limsup B

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

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

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

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

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

⊢ ∀a b c. sigma_algebra a ∧ c ∈ space b ⇒ (λx. c) ∈ measurable a b

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

⊢ ∀a b. sigma_algebra a ∧ sigma_algebra b ⇒ FST ∈ measurable (a × b) a

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

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

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

⊢ ∀a b1 b2 X Y.
    sigma_algebra a ∧ sigma_algebra b1 ∧ sigma_algebra b2 ∧
    X ∈ measurable a b1 ∧ Y ∈ measurable a b2 ⇒
    (λx. (X x,Y x)) ∈ measurable a (b1 × b2)

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

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

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

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

⊢ ∀a b. sigma_algebra a ∧ sigma_algebra b ⇒ SND ∈ measurable (a × b) b

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

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

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

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

⊢ ∀sp sts P.
    pi_system (sp,sts) ∧ sts ⊆ P ∧ dynkin_system (sp,P) ⇒
    subsets (sigma sp sts) ⊆ P

⊢ ∀sp. algebra (sp,POW sp)

⊢ ∀sp. sigma_algebra (sp,POW sp)

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

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

⊢ ∀a b s y.
    sigma_algebra a ∧ subset_class (space b) (subsets b) ∧
    s ∈ subsets (a × b) ⇒
    {x | (x,y) ∈ s} ∈ subsets a

⊢ ∀a b s x.
    subset_class (space a) (subsets a) ∧ sigma_algebra b ∧
    s ∈ subsets (a × b) ⇒
    {y | (x,y) ∈ s} ∈ subsets b

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

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

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

⊢ ∀r. ring r ⇒ ∅ ∈ subsets r

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

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

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

⊢ ∀r c. ring r ∧ FINITE c ∧ c ⊆ subsets r ∧ c ≠ ∅ ⇒ BIGINTER c ∈ subsets r

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

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

⊢ ∀r. ring r ⇒ semiring r

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

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

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

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

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

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

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

⊢ ∀r. semiring r ⇒ ∅ ∈ subsets r

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

⊢ ∀r c.
    semiring r ∧ FINITE c ∧ c ⊆ subsets r ∧ c ≠ ∅ ⇒ BIGINTER c ∈ subsets r

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

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

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

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

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

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

⊢ ∀f. ∃g.
    g 0 = f 0 ∧ (∀n. g n = BIGUNION (IMAGE f (count1 n))) ∧
    (∀n. g n ⊆ g (SUC n)) ∧
    BIGUNION (IMAGE f 𝕌(:num)) = BIGUNION (IMAGE g 𝕌(:num))

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

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

⊢ ∀a. sigma_algebra a ⇒ algebra a

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

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

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

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

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

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

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

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

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

⊢ ∀a c.
    sigma_algebra a ∧ countable c ∧ c ≠ ∅ ∧ c ⊆ subsets a ⇒
    BIGINTER c ∈ subsets a

⊢ ∀a P.
    sigma_algebra a ∧ P ⊆ subsets a ⇒
    (λs. countably_infinite s) INTERSECTION_OF P ⊆ subsets a

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

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

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

⊢ ∀a P. sigma_algebra a ∧ P ⊆ subsets a ⇒ countable UNION_OF P ⊆ subsets a

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

⊢ ∀a. sigma_algebra a ⇒ ∅ ∈ subsets a

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

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

⊢ ∀a c.
    sigma_algebra a ∧ FINITE c ∧ c ⊆ subsets a ∧ c ≠ ∅ ⇒
    BIGINTER c ∈ subsets a

⊢ ∀a P.
    sigma_algebra a ∧ P ⊆ subsets a ⇒
    (λs. finitely_many s) INTERSECTION_OF P ⊆ subsets a

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

⊢ ∀a P. sigma_algebra a ∧ P ⊆ subsets a ⇒ FINITE UNION_OF P ⊆ subsets a

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

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

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

⊢ ∀a. sigma_algebra a ⇒ dynkin_system a

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

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

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

⊢ ∀a b. sigma_algebra a ∧ sigma_algebra b ⇒ sigma_algebra (a × b)

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

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

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

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

⊢ ∀sts. sigma_algebra (sigma 𝕌(:α) sts)

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

⊢ ∀a. sigma_algebra a ⇒ subset_class (space a) (subsets a)

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

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

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

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

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

⊢ ∀a. sigma_algebra a ⇔ pi_system a ∧ dynkin_system a

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

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

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

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

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

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

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

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

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

⊢ ∀sp sts d.
    subset_class sp sts ∧ (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧
    sts ⊆ d ∧ dynkin_system (sp,d) ⇒
    subsets (sigma sp sts) ⊆ d

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

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

⊢ ∀sp sts B.
    subset_class sp sts ∧ B ⊆ sp ⇒
    sigma_algebra (B,IMAGE (λs. s ∩ B) (subsets (sigma sp sts))) ∧
    subsets (sigma B (IMAGE (λs. s ∩ B) sts)) =
    IMAGE (λs. s ∩ B) (subsets (sigma sp sts))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

⊢ ∀a b.
    subsets (a × b) =
    BIGINTER
      {s |
       prod_sets (subsets a) (subsets b) ⊆ s ∧
       sigma_algebra (space a × space b,s)}

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

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

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

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

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

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

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

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

⊢ ∀N s t. N ⊆ {s; t} ∧ N ≠ ∅ ⇒ N = {s} ∨ N = {t} ∨ N = {s; t}

⊢ ∀a E.
    sigma_algebra a ∧ E ⊆ space a ⇒
    sigma_algebra (E,{A ∩ E | A ∈ subsets a})

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

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

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

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

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

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

⊢ ∀a. algebra a ∧ FINITE (space a) ⇒ sigma_algebra a

⊢ ∀a. algebra a ∧ FINITE (subsets a) ⇒ sigma_algebra a

⊢ ∀top s. closed_in top s ⇒ s ∈ subsets (general_borel top)

⊢ ∀n. count1 n = {m | m ≤ n}

⊢ ∀n. count1 n = {0 .. n}

⊢ ∀A. disjoint_family A ⇔ ∀i j. i ≠ j ⇒ DISJOINT (A i) (A j)

⊢ ∀A. disjoint_family (disjointed A)

⊢ ∀A J.
    disjoint_family_on A J ⇔
    ∀i j. i ∈ J ∧ j ∈ J ∧ i ≠ j ⇒ DISJOINT (A i) (A j)

⊢ ∀a s.
    INJ a s (IMAGE a s) ⇒ (disjoint_family_on a s ⇔ disjoint (IMAGE a s))

⊢ ∀a s. disjoint_family_on a s ⇒ disjoint (IMAGE a s)

⊢ ∀A n. disjointed A n ⊆ A n

⊢ ∀a f.
    exhausting_sequence a f ⇔
    f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
    BIGUNION (IMAGE f 𝕌(:num)) = space a

⊢ ∀E c. exhausting_sequence (general_borel (mtop E)) (λn. mcball E (c,&n))

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

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

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

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

⊢ ∀f s.
    FINITE s ∧ (∀x. f x ∈ s) ∧ (∀m n. m ≠ n ⇒ DISJOINT (f m) (f n)) ⇒
    ∃N. ∀n. n ≥ N ⇒ f n = ∅

⊢ ∀a. has_exhausting_sequence a ⇔
      ∃f. f ∈ (𝕌(:num) → subsets a) ∧ (∀m n. m ≤ n ⇒ f m ⊆ f n) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = space a

⊢ ∀a. has_exhausting_sequence a ⇔
      ∃f. f ∈ (𝕌(:num) → subsets a) ∧ (∀n. f n ⊆ f (SUC n)) ∧
          BIGUNION (IMAGE f 𝕌(:num)) = space a

⊢ ∀E. has_exhausting_sequence (general_borel (mtop E))

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

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

⊢ ∀top s. open_in top s ⇒ s ∈ subsets (general_borel top)

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

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

⊢ ∀A sp.
    sigma_algebra A ∧ sp ∈ subsets A ⇒
    subsets (restrict_algebra A sp) ⊆ subsets A

⊢ ∀A. subset_class (space A) (subsets A) ⇒ restrict_algebra A (space A) = A

⊢ ∀A. sigma_algebra A ⇒ restrict_algebra A (space A) = A

⊢ ∀sp sts.
    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

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

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

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

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

⊢ ∀sp sts.
    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

⊢ ∀E. limsup E = BIGINTER (IMAGE (λn. BIGUNION (IMAGE E (from n))) 𝕌(:num))

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

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

⊢ ∀sp sts. sigma_algebra (sp,sts) ⇔ sigma_algebra_alt sp sts

⊢ sigma_algebra (general_borel top)

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

⊢ ∀A sp.
    sigma_algebra A ∧ sp ∈ subsets A ⇒
    sigma_algebra (restrict_algebra A sp)

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

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

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

⊢ ∀sp A X.
    sigma_algebra A ∧ X ∈ (sp → space A) ⇒
    sigma sp A X = sigma sp (λn. A) (λn x. X x) (count 1)

⊢ ∀A B f.
    sigma_algebra A ∧ f ∈ measurable A B ⇒
    subsets (sigma (space A) B f) ⊆ subsets A

⊢ ∀sp A f.
    sigma_algebra A ∧ f 0 ∈ (sp → space A) ⇒
    sigma sp (λn. A) f (count 1) = sigma sp A (f 0)

⊢ ∀A B f J.
    sigma_algebra A ∧ (∀i. i ∈ J ⇒ sigma_algebra (B i)) ∧
    (∀i. i ∈ J ⇒ f i ∈ measurable A (B i)) ⇒
    subsets (sigma (space A) B f J) ⊆ subsets A

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

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

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

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

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

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

⊢ ∀sp st. ∅ ∈ sigma_sets sp st

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

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

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

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

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

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

⊢ ∀sp A. A ⊆ POW sp ⇒ sigma_sets sp A = subsets (sigma sp A)

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

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

⊢ ∀X A. A ⊆ sigma_sets X A

⊢ ∀sp A. sp ∈ sigma_sets sp A

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

⊢ ∀top. space (general_borel top) = topspace top

⊢ ∀E. space (general_borel (mtop E)) = mspace E

⊢ ∀sp A f. space (sigma sp A f) = sp

⊢ ∀sp A f J. space (sigma sp A f J) = sp

⊢ ∀sp. subset_class sp (POW sp)

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

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

⊢ ∀sp. algebra (sp,{∅; sp})

⊢ ∀h t. algebra ({h; t},{∅; {h}; {t}; {h; t}})

⊢ ∀sp s. s ⊆ sp ⇒ algebra (sp,{∅; s; sp DIFF s; sp})