LeanMachineLearning exposition

ProbabilityTheory.measurableSet_graph'🔗

Minimal Lean file

measurableSet_graph'🔗

LemmaProbabilityTheory.measurableSet_graph'
Details

No docstring.

🔗theorem
ProbabilityTheory.measurableSet_graph'.{u_7, u_8} {β : Type u_7}
  {Ω : Type u_8} {x✝ : MeasurableSpace β} {x✝¹ : MeasurableSpace Ω}
  [MeasurableEq Ω] {f : β → Ω} (hf : Measurable f) :
  MeasurableSet {p | Prod.snd p = f (Prod.fst p)}
ProbabilityTheory.measurableSet_graph'.{u_7,
    u_8}
  {β : Type u_7} {Ω : Type u_8}
  {x✝ : MeasurableSpace β}
  {x✝¹ : MeasurableSpace Ω}
  [MeasurableEq Ω] {f : β → Ω}
  (hf : Measurable f) :
  MeasurableSet
    {p | Prod.snd p = f (Prod.fst p)}

Code

lemma measurableSet_graph' {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω}
    [MeasurableEq Ω] {f : β → Ω} (hf : Measurable f) :
    MeasurableSet {p : β × Ω | p.2 = f p.1}
Used by (1)

Actions: Source · Open Issue

Proof
measurableSet_eq_fun (by fun_prop) (by fun_prop)