generates/measurable

Stream: maths

[Iocta]

image.png

Is this the right way to define generates?

import measure_theory.measure_space

open measure_theory measure_theory.measure_space classical set real

open_locale classical
noncomputable theory

variable Ω : Type
variable [measurable_space Ω]


open measurable_space


structure algebra' (α : Type*) :=
(in_algebra : set α → Prop)
(algebra_empty : in_algebra ∅)
(algebra_compl : ∀ (s : set α), in_algebra s → in_algebra sᶜ)
(algebra_union : ∀ (s1 s2 : set α), in_algebra s1 → in_algebra s2 → in_algebra (s1 ∪ s2))

def generates  (𝓐 : set (set ℝ)) (𝓢 : algebra' ℝ) : Prop :=
(∀A : set ℝ, A ∈ 𝓐 → 𝓢.in_algebra A) ∧ (
    -- 𝓣 contains 𝓐
    ∀𝓣 : algebra' ℝ, ∀A : set ℝ, A ∈ 𝓐 → 𝓣.in_algebra A →
    -- then 𝓣 ⊆ 𝓢.
    ∀A : set ℝ, (𝓢.in_algebra A → 𝓣.in_algebra A)
  )

[Iocta]

I want to use it in this exercise
image.png

[Yury G. Kudryashov]

I guess, $X\colon\Omega\to\alpha$, $\mathcal A$ is a set of sets of $\alpha$, $\mathcal S$ is the $\sigma$-algebra generated by $\mathcal A$. What is $\mathcal F$? Is it "the" $\sigma$-algebra on $\Omega$, so Theorem 1.3.1 is actually docs#measurable_generate_from?

[Yury G. Kudryashov]

And you want to prove docs#comap_generate_from?