α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (piecewise s f g)
refine' ⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => _⟩
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : ¬x ∈ s
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))
by_cases hx : x ∈ s
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))
simpa [@Set.piecewise_eq_of_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
  hx] using hf.tendsto_approx x
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.193105
ι : Type ?u.193108
inst✝¹ : Countable ι
f g : α → β
m : MeasurableSpace α
inst✝ : TopologicalSpace β
s : Set α
x✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : ¬x ∈ s
⊢ Tendsto
    (fun n =>
      ↑((fun n => SimpleFunc.piecewise s hs (StronglyMeasurable.approx hf n) (StronglyMeasurable.approx hg n)) n) x)
    atTop (𝓝 (piecewise s f g x))
simpa [@Set.piecewise_eq_of_not_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
  hx] using hg.tendsto_approx x