E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ Tendsto (fun i => Function.support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : Tendsto (fun i => (φ i).rOut) l (𝓝 0)
⊢ Tendsto (fun i => Function.support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
simp_rw [NormedAddCommGroup.tendsto_nhds_zero, Real.norm_eq_abs,
  abs_eq_self.mpr (φ _).rOut_pos.le] at hφ
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (Function.support fun x_1 => ContDiffBump.normed (φ x) μ x_1) ∈ 𝒫 ball c i
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ Tendsto (fun i => Function.support fun x => ContDiffBump.normed (φ i) μ x) l (smallSets (𝓝 c))
rw [nhds_basis_ball.smallSets.tendsto_right_iff]
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (Function.support fun x => ContDiffBump.normed (φ i) μ x) ∈ 𝒫 ball c ε
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
⊢ ∀ (i : ℝ), 0 < i → ∀ᶠ (x : ι) in l, (Function.support fun x_1 => ContDiffBump.normed (φ x) μ x_1) ∈ 𝒫 ball c i
refine fun ε hε ↦ (hφ ε hε).mono fun i hi ↦ ?_
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ (Function.support fun x => ContDiffBump.normed (φ i) μ x) ∈ 𝒫 ball c ε
rw [(φ i).support_normed_eq]
no goals
E : Type u_2
X : Type ?u.2328028
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup X
inst✝⁶ : NormedSpace ℝ X
inst✝⁵ : HasContDiffBump E
c : E
f : ContDiffBump c
x : E
n : ℕ∞
inst✝⁴ : MeasurableSpace E
μ : MeasureTheory.Measure E
inst✝³ : BorelSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : IsLocallyFiniteMeasure μ
inst✝ : Measure.IsOpenPosMeasure μ
ι : Type u_1
φ : ι → ContDiffBump c
l : Filter ι
hφ : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : ι) in l, (φ x).rOut < ε
ε : ℝ
hε : 0 < ε
i : ι
hi : (φ i).rOut < ε
⊢ ball c (φ i).rOut ∈ 𝒫 ball c ε
exact ball_subset_ball hi.le