disjoint_nhds — Mathlib

English

In a seminormed group, the neighborhoods of a point x and a filter f are disjoint iff there exists δ > 0 such that eventually δ ≤ ‖y/x‖ for y in the filter.

Русский

В нормированной группе соседа точки x и фильтр f расходятся тогда и только тогда, когда существует δ>0 такое, что почти всегда δ ≤ ‖y/x‖ при y из фильтра.

LaTeX

$$$\\text{Disjoint}(\\mathcal{N}(x), f) \\iff \\exists \\delta > 0, \\; \\forall^\\infty y \\in f, \\; \\delta \\leq \\|y/x\\|$$$

Lean4

@[to_additive]
theorem disjoint_nhds (x : E) (f : Filter E) : Disjoint (𝓝 x) f ↔ ∃ δ > 0, ∀ᶠ y in f, δ ≤ ‖y / x‖ := by
  simp [NormedCommGroup.nhds_basis_norm_lt x |>.disjoint_iff_left, compl_setOf, eventually_iff]

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