mem_nhds_iff — Mathlib

English

A set s belongs to the neighborhood filter at x iff there exists an open set t contained in s with x ∈ t.

Русский

Множество s принадлежит фильтру окрестностей x тогда и только тогда, когда существует открытое t ⊆ s с x ∈ t.

LaTeX

$$$s \\in \\mathcal N(x) \\iff \\exists t \\subseteq s,\\ IsOpen(t) \\land x \\in t$$$

Lean4

theorem mem_nhds_iff : s ∈ 𝓝 x ↔ ∃ t ⊆ s, IsOpen t ∧ x ∈ t :=
  (nhds_basis_opens x).mem_iff.trans <|
    exists_congr fun _ => ⟨fun h => ⟨h.2, h.1.2, h.1.1⟩, fun h => ⟨⟨h.2.2, h.2.1⟩, h.1⟩⟩

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