Restrict a MeasurableSpace to a set

Stream: new members

[Iocta]

What do I need to do here?

import Mathlib

namespace MeasureTheory

open MeasurableSpace

variable {α : Type}  {s : Set (Set α)} {m : MeasurableSpace α}

/-
Let m be a measurable space on α and (y : Set α).
Then the restriction of m to y -- {a ∩ y such that a ∈ m} is also a measurable set.
-/
def measurable_space_subtype (y : Set α) : MeasurableSpace {x // x ∈ y} where
  MeasurableSet' s := ∃ a, MeasurableSet[m] a ∧ s = {x | x ∈ a}
  measurableSet_empty := by {
    simp only [Set.mem_inter_iff]
    use ∅
    simp_all only [MeasurableSet.empty, Set.image_empty, Set.mem_empty_iff_false, Set.setOf_false, and_self]
  }
  measurableSet_compl t ht := by {
    -- reduce at *
    -- simp only [Subtype.exists, exists_and_right, exists_eq_right, exists_eq_right', imp_false] at *
    reduce at *
    simp only [Subtype.exists, exists_and_right, exists_eq_right, exists_eq_right', imp_false] at *
/-
α : Type
J s : Set (Set α)
m : MeasurableSpace α
y : α → Prop
t : { x // x ∈ y } → Prop
ht : m.1 fun x ↦ ∃ (x_1 : x ∈ y), t ⟨x, ⋯⟩
⊢ m.1 fun x ↦ ∃ (x_1 : x ∈ y), ⟨x, ⋯⟩ ∉ t
-/


  }
  measurableSet_iUnion f := _

[Eric Wieser]

def measurable_space_subtype (y : Set α) : MeasurableSpace {x // x ∈ y} :=
  MeasurableSpace.comap Subtype.val ‹_›

[Eric Wieser]

Assuming this produces the sets you want

[Etienne Marion]

It is docs#Subtype.instMeasurableSpace