mem_interior_iff_mem_nhds — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_interior_iff_mem_nhds : x ∈ interior s ↔ s ∈ 𝓝 x :=
  mem_interior.trans mem_nhds_iff.symm

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