α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
⊢ AEMeasurable f
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
⊢ AEMeasurable f
nontriviality α
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
⊢ AEMeasurable f
inhabit α
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ AEMeasurable f
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
⊢ AEMeasurable f
have : (Set.piecewise s f fun _ => f default) =ᵐ[μ.restrict s] f := piecewise_ae_eq_restrict hs
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ Measurable (Set.piecewise s f fun x => f default)
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ AEMeasurable f
refine' ⟨Set.piecewise s f fun _ => f default, _, this.symm⟩
case hf
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ ∀ (s_1 : Set β), IsOpen s_1 → MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' s_1)
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ Measurable (Set.piecewise s f fun x => f default)
apply measurable_of_isOpen
case hf
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
case hf
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
⊢ ∀ (s_1 : Set β), IsOpen s_1 → MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' s_1)
intro t ht
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
case hf
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
obtain ⟨u, u_open, hu⟩ : ∃ u : Set α, IsOpen u ∧ f ⁻¹' t ∩ s = u ∩ s :=
  _root_.continuousOn_iff'.1 hf t ht
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s ∪ (fun x => f default) ⁻¹' t \ s)
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet ((Set.piecewise s f fun x => f default) ⁻¹' t)
rw [piecewise_preimage, Set.ite, hu]
no goals
case hf.intro.intro
α : Type u_1
β : Type u_2
E : Type ?u.1668784
F : Type ?u.1668787
inst✝⁶ : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : TopologicalSpace α
inst✝³ : OpensMeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : TopologicalSpace β
inst✝ : BorelSpace β
f : α → β
s : Set α
μ : MeasureTheory.Measure α
hf : ContinuousOn f s
hs : MeasurableSet s
✝ : Nontrivial α
inhabited_h : Inhabited α
this : (Set.piecewise s f fun x => f default) =ᵐ[Measure.restrict μ s] f
t : Set β
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s ∪ (fun x => f default) ⁻¹' t \ s)
exact (u_open.measurableSet.inter hs).union ((measurable_const ht.measurableSet).diff hs)