α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
let g_seq_s : ℕ → @SimpleFunc α m β := fun n => (hf.approx n).restrict s
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x := by
  intro x hx n
  rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
have hg_zero : ∀ (x) (_ : x ∉ s), ∀ n, g_seq_s n x = 0 := by
  intro x hx n
  rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_not_mem hx]
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))) ∧ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(fs n) x = 0
refine' ⟨g_seq_s, fun x => _, hg_zero⟩
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : ¬x ∈ s
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
by_cases hx : x ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
x : α
hx : x ∈ s
n : ℕ
⊢ ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
⊢ ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
intro x hx n
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
x : α
hx : x ∈ s
n : ℕ
⊢ ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
x : α
hx : ¬x ∈ s
n : ℕ
⊢ ↑(g_seq_s n) x = 0
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
⊢ ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
intro x hx n
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
x : α
hx : ¬x ∈ s
n : ℕ
⊢ ↑(g_seq_s n) x = 0
rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_not_mem hx]
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
simp_rw [hg_eq x hx]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => ↑(StronglyMeasurable.approx hf n) x) atTop (𝓝 (f x))
exact hf.tendsto_approx x
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : ¬x ∈ s
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : ¬x ∈ s
⊢ Tendsto (fun n => ↑(g_seq_s n) x) atTop (𝓝 (f x))
simp_rw [hg_zero x hx, hf_zero x hx]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.228351
ι : Type ?u.228354
inst✝² : Countable ι
f✝ g : α → β
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ (x : α), ¬x ∈ s → f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (StronglyMeasurable.approx hf n) s
hg_eq : ∀ (x : α), x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = ↑(StronglyMeasurable.approx hf n) x
hg_zero : ∀ (x : α), ¬x ∈ s → ∀ (n : ℕ), ↑(g_seq_s n) x = 0
x : α
hx : ¬x ∈ s
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
exact tendsto_const_nhds