theorem
Measurable.dite_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{p : Prop}
[Decidable p]
{f : p → α → β}
{g : ¬p → α → β}
(hf : ∀ (h : p), Measurable (f h))
(hg : ∀ (h : ¬p), Measurable (g h))
:
Measurable (dite p f g)
theorem
Measurable.fun_dite_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{p : Prop}
[Decidable p]
{f : p → α → β}
{g : ¬p → α → β}
(hf : ∀ (h : p), Measurable (f h))
(hg : ∀ (h : ¬p), Measurable (g h))
:
Measurable fun (a : α) => if h : p then f h a else g h a
theorem
Measurable.ite_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{p : Prop}
[Decidable p]
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable (if p then f else g)
theorem
Measurable.fun_ite_const
{α : Type u_1}
{β : Type u_2}
{mα : MeasurableSpace α}
{mβ : MeasurableSpace β}
{p : Prop}
[Decidable p]
{f g : α → β}
(hf : Measurable f)
(hg : Measurable g)
:
Measurable fun (a : α) => if p then f a else g a