Countable Measurable

Stream: new members

[Iocta]

Is there something like this? I'm not sure how to even do the empty part. I expected there to be an iUnion_mem_of_forall_mem but I couldn't find it.

import Mathlib


import Mathlib
import Mathlib.Data.Set.SymmDiff

namespace MeasureTheory

open MeasurableSpace

variable {α : Type}

def countable_measurable {a : Set (Set α)} {d}
    (hd : d = {b | b ⊆ a ∧ Countable b}) (hd' : d.Nonempty) : MeasurableSpace α where
  MeasurableSet' := ⋃ b ∈ d, (generateFrom b).MeasurableSet'
  measurableSet_empty := by {
    have empty_measurable : ∀ b ∈ d, (generateFrom b).MeasurableSet' ∅ := by
      exact fun b a ↦ (generateFrom b).measurableSet_empty
    sorry
  }
  measurableSet_compl := _
  measurableSet_iUnion := _

[Matt Diamond]

rw [Set.mem_iUnion] works if you do change ∅ ∈ Set.iUnion _ first

[Matt Diamond]

actually you don't need to use change, you can solve it like this:

measurableSet_empty := by {
  have ⟨s, hs⟩ := hd'
  exact Set.mem_biUnion hs (generateFrom s).measurableSet_empty
}