α : Type u_3
β : Type u_2
ι✝ : Type ?u.3074
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.3074
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ EquicontinuousAt F x₀
rw [Metric.equicontinuousAt_iff_right]
α : Type u_3
β : Type u_2
ι✝ : Type ?u.3074
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.3074
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
intro ε ε0
no goals
α : Type u_3
β : Type u_2
ι✝ : Type ?u.3074
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
filter_upwards [Filter.mem_map.mp <| b_lim (Iio_mem_nhds ε0), H] using
  fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁