∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {s : Set α} [inst_1 : PseudoEMetricSpace β] {f : α → β}
  {t : Set β} {a : α} {b : β},
  Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε