α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ UniformEquicontinuous F
rw [Metric.uniformEquicontinuous_iff]
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
intro ε ε0
case intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩
case intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (F i x) (F i y) < ε
case intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
⊢ ∃ δ, δ > 0 ∧ ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
refine' ⟨δ, δ0, fun x y hxy i => _⟩
no goals
case intro.intro
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (F i x) (F i y) < ε
calc
  dist (F i x) (F i y) ≤ b (dist x y) := H x y i
  _ ≤ |b (dist x y)| := (le_abs_self _)
  _ = dist (b (dist x y)) 0 := by simp [Real.dist_eq]
  _ < ε := hδ (by simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy)
no goals
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ abs (b (dist x y)) = dist (b (dist x y)) 0
simp [Real.dist_eq]
no goals
α : Type u_3
β : Type u_2
ι✝ : Type ?u.4017
inst✝¹ : PseudoMetricSpace α
ι : Type u_1
inst✝ : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
δ : ℝ
δ0 : δ > 0
hδ : ∀ {x : ℝ}, dist x 0 < δ → dist (b x) 0 < ε
x y : β
hxy : dist x y < δ
i : ι
⊢ dist (dist x y) 0 < δ
simpa only [Real.dist_eq, tsub_zero, abs_dist] using hxy