mem_nhdsWithin_iff — Mathlib

English

A set s belongs to nhdsWithin x t if and only if there exists ε > 0 with ball x ε ∩ t ⊆ s.

Русский

Множество s принадлежит nhdsWithin x t тогда и только тогда, когда существует ε > 0 такое, что ball x ε ∩ t ⊆ s.

LaTeX

$$$s \\in \\mathcal{N}[t](x) \\iff \\exists \\varepsilon > 0, \\ ball(x,\\varepsilon) \\cap t \\subseteq s$$$

Lean4

theorem mem_nhdsWithin_iff : s ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s :=
  nhdsWithin_basis_eball.mem_iff

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