Neighborhoods of a point times a relative neighborhood

In a product of pseudometric spaces, a property holds eventually for the product filter 𝓝 x ×ˢ 𝓝[s] t exactly when it holds on a box of points (y, τ) with dist y x < δ, τ ∈ s and dist τ t < δ (Metric.eventually_nhds_prod_nhdsWithin_iff). This is the form of Metric.eventually_nhds_prod_iff in which the second filter is also given by a distance bound, as used for functions of a space variable and a time variable restricted to an interval.

theorem Metric.eventually_nhds_prod_nhdsWithin_iff {X : Type u_1} {Y : Type u_2} [PseudoMetricSpace X] [PseudoMetricSpace Y] {P : X × Y → Prop} {x : X} {s : Set Y} {t : Y} : (∀ᶠ (p : X × Y) in nhds x ×ˢ nhdsWithin t s, P p) ↔ ∃ δ > 0, ∀ (y : X), dist y x < δ → ∀ τ ∈ s, dist τ t < δ → P (y, τ)

A property holds eventually near x and near t within s if and only if it holds on a box dist y x < δ, τ ∈ s, dist τ t < δ.