α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ : SigmaFinite (Measure.restrict μ t)
⊢ FinStronglyMeasurable f μ
haveI : SigmaFinite (μ.restrict t) := htμ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
⊢ FinStronglyMeasurable f μ
let S := spanningSets (μ.restrict t)
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
⊢ FinStronglyMeasurable f μ
have hS_meas : ∀ n, MeasurableSet (S n) := measurable_spanningSets (μ.restrict t)
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
⊢ FinStronglyMeasurable f μ
let f_approx := hf_meas.approx
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
⊢ FinStronglyMeasurable f μ
let fs n := SimpleFunc.restrict (f_approx n) (S n ∩ t)
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ FinStronglyMeasurable f μ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
⊢ FinStronglyMeasurable f μ
have h_fs_t_compl : ∀ n, ∀ x, x ∉ t → fs n x = 0 := by
  intro n x hxt
  rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]
  refine' Set.indicator_of_not_mem _ _
  simp [hxt]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤

case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ FinStronglyMeasurable f μ
refine' ⟨fs, _, fun x => _⟩
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ ↑(fs n) x = 0
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
⊢ ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
intro n x hxt
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ indicator (S n ∩ t) (↑(f_approx n)) x = 0
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ ↑(fs n) x = 0
rw [SimpleFunc.restrict_apply _ ((hS_meas n).inter ht)]
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ ¬x ∈ S n ∩ t
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ indicator (S n ∩ t) (↑(f_approx n)) x = 0
refine' Set.indicator_of_not_mem _ _
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
n : ℕ
x : α
hxt : ¬x ∈ t
⊢ ¬x ∈ S n ∩ t
simp [hxt]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ ∀ (n : ℕ),
    ↑↑μ
        (⋃ (y : β) (_ :
          y ∈
            Finset.filter (fun y => y ≠ 0)
              (SimpleFunc.range
                (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n)
                  (spanningSets (Measure.restrict μ t) n ∩ t)))),
          ↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
            {y}) <
      ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ ∀ (n : ℕ), ↑↑μ (support ↑(fs n)) < ⊤
simp_rw [SimpleFunc.support_eq]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
⊢ ∑ p in
      Finset.filter (fun y => y ≠ 0)
        (SimpleFunc.range
          (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t))),
      ↑↑μ
        (↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
          {p}) <
    ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
⊢ ∀ (n : ℕ),
    ↑↑μ
        (⋃ (y : β) (_ :
          y ∈
            Finset.filter (fun y => y ≠ 0)
              (SimpleFunc.range
                (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n)
                  (spanningSets (Measure.restrict μ t) n ∩ t)))),
          ↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
            {y}) <
      ⊤
refine' fun n => (measure_biUnion_finset_le _ _).trans_lt _
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ
      (↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
        {y}) <
    ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
⊢ ∑ p in
      Finset.filter (fun y => y ≠ 0)
        (SimpleFunc.range
          (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t))),
      ↑↑μ
        (↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
          {p}) <
    ⊤
refine' ENNReal.sum_lt_top_iff.mpr fun y hy => _
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t ∩ ↑(StronglyMeasurable.approx hf_meas n) ⁻¹' {y}) < ⊤

case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ y ≠ 0
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ
      (↑(SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ⁻¹'
        {y}) <
    ⊤
rw [SimpleFunc.restrict_preimage_singleton _ ((hS_meas n).inter ht)]
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ y ≠ 0

case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t ∩ ↑(StronglyMeasurable.approx hf_meas n) ⁻¹' {y}) < ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t ∩ ↑(StronglyMeasurable.approx hf_meas n) ⁻¹' {y}) < ⊤

case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ y ≠ 0
swap
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t) < ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t ∩ ↑(StronglyMeasurable.approx hf_meas n) ⁻¹' {y}) < ⊤
refine' (measure_mono (Set.inter_subset_left _ _)).trans_lt _
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
h_lt_top : ↑↑(Measure.restrict μ t) (spanningSets (Measure.restrict μ t) n) < ⊤
⊢ ↑↑μ (S n ∩ t) < ⊤
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ ↑↑μ (S n ∩ t) < ⊤
have h_lt_top := measure_spanningSets_lt_top (μ.restrict t) n
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
h_lt_top : ↑↑(Measure.restrict μ t) (spanningSets (Measure.restrict μ t) n) < ⊤
⊢ ↑↑μ (S n ∩ t) < ⊤
rwa [Measure.restrict_apply' ht] at h_lt_top
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this✝ : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
this : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable (y = 0)
⊢ y ≠ 0
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
⊢ y ≠ 0
letI : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable _
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this✝ : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
      SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ∧
    y ≠ 0
this : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable (y = 0)
⊢ y ≠ 0
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this✝ : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
    Finset.filter (fun y => y ≠ 0)
      (SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)))
this : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable (y = 0)
⊢ y ≠ 0
rw [Finset.mem_filter] at hy
no goals
case refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this✝ : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
n : ℕ
y : β
hy :
  y ∈
      SimpleFunc.range
        (SimpleFunc.restrict (StronglyMeasurable.approx hf_meas n) (spanningSets (Measure.restrict μ t) n ∩ t)) ∧
    y ≠ 0
this : (y : β) → Decidable (y = 0) := fun y => Classical.propDecidable (y = 0)
⊢ y ≠ 0
exact hy.2
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
case refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
by_cases hxt : x ∈ t
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))

case pos
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))

case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
swap
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
case pos
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
have h : Tendsto (fun n => (f_approx n) x) atTop (𝓝 (f x)) := hf_meas.tendsto_approx x
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
⊢ ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
rw [tendsto_atTop'] at h ⊢
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
s : Set β
hs : s ∈ 𝓝 (f x)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
⊢ ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
intro s hs
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
case pos.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
s : Set β
hs : s ∈ 𝓝 (f x)
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
obtain ⟨n₂, hn₂⟩ := h s hs
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → ↑(fs m) x = ↑(f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
m : ℕ
hm : m ≥ max n₁ n₂
⊢ ↑(fs m) x ∈ s
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m_1 : ℕ), n₁ ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
⊢ ∃ a, ∀ (b : ℕ), b ≥ a → ↑(fs b) x ∈ s
refine' ⟨max n₁ n₂, fun m hm => _⟩
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → ↑(fs m) x = ↑(f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
m : ℕ
hm : m ≥ max n₁ n₂
⊢ ↑(f_approx m) x ∈ s
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → ↑(fs m) x = ↑(f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
m : ℕ
hm : m ≥ max n₁ n₂
⊢ ↑(fs m) x ∈ s
rw [hn₁ m ((le_max_left _ _).trans hm.le)]
no goals
case pos.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h✝ : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
h : ∀ (s : Set β), s ∈ 𝓝 (f x) → ∃ a, ∀ (b : ℕ), b ≥ a → ↑(f_approx b) x ∈ s
n₁ : ℕ
hn₁ : ∀ (m : ℕ), n₁ ≤ m → ↑(fs m) x = ↑(f_approx m) x
s : Set β
hs : s ∈ 𝓝 (f x)
n₂ : ℕ
hn₂ : ∀ (b : ℕ), b ≥ n₂ → ↑(f_approx b) x ∈ s
m : ℕ
hm : m ≥ max n₁ n₂
⊢ ↑(f_approx m) x ∈ s
exact hn₂ m ((le_max_right _ _).trans hm.le)
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 (f x))
rw [funext fun n => h_fs_t_compl n x hxt, hft_zero x hxt]
no goals
case neg
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : ¬x ∈ t
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
exact tendsto_const_nhds
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
m : ℕ
hnm : n ≤ m
⊢ ↑(fs m) x = ↑(f_approx m) x
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
⊢ ∃ n, ∀ (m_1 : ℕ), n ≤ m_1 → ↑(fs m_1) x = ↑(f_approx m_1) x
refine' ⟨n, fun m hnm => _⟩
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m✝ : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
m : ℕ
hnm : n ≤ m
⊢ ↑(fs m) x = ↑(f_approx m) x
simp_rw [SimpleFunc.restrict_apply _ ((hS_meas m).inter ht),
  Set.indicator_of_mem (hn m hnm)]
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t

α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
rsuffices ⟨n, hn⟩ : ∃ n, ∀ m, n ≤ m → x ∈ S m
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : x ∈ S n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m

α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, x ∈ S n
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m
rsuffices ⟨n, hn⟩ : ∃ n, x ∈ S n
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ x ∈ univ
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ ∃ n, x ∈ S n
rw [← Set.mem_iUnion, iUnion_spanningSets (μ.restrict t)]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
⊢ x ∈ univ
trivial
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → x ∈ S m
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m ∩ t
exact ⟨n, fun m hnm => Set.mem_inter (hn m hnm) hxt⟩
no goals
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.51589
ι : Type ?u.51592
inst✝² : Countable ι
f g : α → β
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
m : MeasurableSpace α
μ : Measure α
hf_meas : StronglyMeasurable f
t : Set α
ht : MeasurableSet t
hft_zero : ∀ (x : α), x ∈ tᶜ → f x = 0
htμ this : SigmaFinite (Measure.restrict μ t)
S : ℕ → Set α := spanningSets (Measure.restrict μ t)
hS_meas : ∀ (n : ℕ), MeasurableSet (S n)
f_approx : ℕ → α →ₛ β := StronglyMeasurable.approx hf_meas
fs : ℕ → α →ₛ β := fun n => SimpleFunc.restrict (f_approx n) (S n ∩ t)
h_fs_t_compl : ∀ (n : ℕ) (x : α), ¬x ∈ t → ↑(fs n) x = 0
x : α
hxt : x ∈ t
h : Tendsto (fun n => ↑(f_approx n) x) atTop (𝓝 (f x))
n : ℕ
hn : x ∈ S n
⊢ ∃ n, ∀ (m : ℕ), n ≤ m → x ∈ S m
exact ⟨n, fun m hnm => monotone_spanningSets (μ.restrict t) hnm hn⟩