mem_nhdsSet — Mathlib

English

Let s be an open set. Then s belongs to the set-neighborhoods filter 𝓝ˢ t if and only if t is contained in s.

Русский

Пусть s открыто. Тогда s принадлежит фильтру множеств-окрестностей 𝓝ˢ t тогда и только тогда, когда t ⊆ s.

LaTeX

$$$ IsOpen(s) \rightarrow (s \in 𝓝ˢ t \leftrightarrow t \subseteq s) $$$

Lean4

theorem mem_nhdsSet (hU : IsOpen s) : s ∈ 𝓝ˢ t ↔ t ⊆ s := by rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]

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