eventually_prod_nhds_iff — Mathlib

English

The neighborhoods of x have a basis given by closed balls around x: (𝓝 x) has a basis (closedBall x).

Русский

Окрестности точки x имеют базис из замкнутых шаров вокруг x.

LaTeX

$$$$ (\\mathcal{N}(x)).HasBasis (\\varepsilon > 0) (\\text{closedBall}(x, \\varepsilon)) $$$$

Lean4

/-- A version of `Filter.eventually_prod_iff` where the second filter consists of neighborhoods
in a pseudo-metric space. -/
theorem eventually_prod_nhds_iff {f : Filter ι} {x₀ : α} {p : ι × α → Prop} :
    (∀ᶠ x in f ×ˢ 𝓝 x₀, p x) ↔
      ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i⦄, pa i → ∀ ⦃x⦄, dist x x₀ < ε → p (i, x) :=
  by
  rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]
  constructor <;>
    · rintro ⟨a1, a2, a3, a4, a5⟩
      exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

Похожие утверждения