α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (Set.piecewise s f g ⁻¹' t)
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
⊢ Measurable (Set.piecewise s f g)
refine' measurable_of_isOpen fun t ht => _
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (Set.piecewise s f g ⁻¹' t)
rw [piecewise_preimage, Set.ite]
case h₁
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (f ⁻¹' t ∩ s)

case h₂
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (g ⁻¹' t \ s)
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (f ⁻¹' t ∩ s ∪ g ⁻¹' t \ s)
apply MeasurableSet.union
case h₁.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (f ⁻¹' t ∩ s)
case h₁
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (f ⁻¹' t ∩ s)
rcases _root_.continuousOn_iff'.1 hf t ht with ⟨u, u_open, hu⟩
case h₁.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s)
case h₁.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (f ⁻¹' t ∩ s)
rw [hu]
no goals
case h₁.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : f ⁻¹' t ∩ s = u ∩ s
⊢ MeasurableSet (u ∩ s)
exact u_open.measurableSet.inter hs
case h₂.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (g ⁻¹' t \ s)
case h₂
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
⊢ MeasurableSet (g ⁻¹' t \ s)
rcases _root_.continuousOn_iff'.1 hg t ht with ⟨u, u_open, hu⟩
case h₂.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (u ∩ sᶜ)
case h₂.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (g ⁻¹' t \ s)
rw [diff_eq_compl_inter, inter_comm, hu]
no goals
case h₂.intro.intro
α : Type u_1
β : Type ?u.930878
γ : Type u_2
γ₂ : Type ?u.930884
δ : Type ?u.930887
ι : Sort y
s✝ t✝ u✝ : Set α
inst✝¹⁵ : TopologicalSpace α
inst✝¹⁴ : MeasurableSpace α
inst✝¹³ : OpensMeasurableSpace α
inst✝¹² : TopologicalSpace β
inst✝¹¹ : MeasurableSpace β
inst✝¹⁰ : OpensMeasurableSpace β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : MeasurableSpace γ
inst✝⁷ : BorelSpace γ
inst✝⁶ : TopologicalSpace γ₂
inst✝⁵ : MeasurableSpace γ₂
inst✝⁴ : BorelSpace γ₂
inst✝³ : MeasurableSpace δ
α' : Type ?u.930980
inst✝² : TopologicalSpace α'
inst✝¹ : MeasurableSpace α'
f g : α → γ
s : Set α
inst✝ : (j : α) → Decidable (j ∈ s)
hf : ContinuousOn f s
hg : ContinuousOn g (sᶜ)
hs : MeasurableSet s
t : Set γ
ht : IsOpen t
u : Set α
u_open : IsOpen u
hu : g ⁻¹' t ∩ sᶜ = u ∩ sᶜ
⊢ MeasurableSet (u ∩ sᶜ)
exact u_open.measurableSet.inter hs.compl