α : Type u
β : Type v
X : Type ?u.207501
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
α : Type u
β : Type v
X : Type ?u.207501
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
no goals
α : Type u
β : Type v
X : Type ?u.207501
inst✝¹ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ (ε : ℝ≥0∞), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
simp only [mem_univ, true_and_iff]