subset_interior_iff_nhds — Mathlib

English

For any V ⊆ X, s ⊆ interior(V) if and only if for all x ∈ s, V ∈ 𝓝(x).

Русский

Для множества V ⊆ X верно: s ⊆ interior(V) эквивалентно для каждого x ∈ s, V ∈ 𝓝(x).

LaTeX

$$$s \\subseteq \\operatorname{int}(V) \\iff \\forall x \\in s, V \\in \\mathcal{N}(x)$$$

Lean4

theorem subset_interior_iff_nhds {V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x := by
  simp_rw [subset_def, mem_interior_iff_mem_nhds]

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