English
A swapped version of the previous product- nhds equivalence: exchanging the order yields a corresponding characterization.
Русский
Связанная версия с обменом порядков в предыдущем отношении эквивалентности.
LaTeX
$$$$ \\text{see swap variant of } \\text{eventually_prod_nhds_iff}. $$$$
Lean4
/-- A version of `Filter.eventually_prod_iff` where the first filter consists of neighborhoods
in a pseudo-metric space. -/
theorem eventually_nhds_prod_iff {f : Filter ι} {x₀ : α} {p : α × ι → Prop} :
(∀ᶠ x in 𝓝 x₀ ×ˢ f, p x) ↔
∃ ε > (0 : ℝ), ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧ ∀ ⦃x⦄, dist x x₀ < ε → ∀ ⦃i⦄, pa i → p (x, i) :=
by
refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_
simp only [Prod.exists, forall_prod_set, id, mem_ball, and_assoc, exists_and_left]
rfl
