interior_eq_nhds' — Mathlib

English

Let X be a topological space and s ⊆ X. The interior of s consists exactly of those points x for which s is a neighborhood of x; equivalently, x ∈ interior(s) iff s ∈ 𝒩(x).

Русский

Пусть X — топологическое пространство и s ⊆ X. Внутренность множества s состоит ровно из таких точек x, для которых s является окрестностью x; эквивалентно x ∈ interior(s) тогда и только тогда s ∈ 𝒩(x).

LaTeX

$$$\\operatorname{int}(s) = \\{x \\in X \\mid s \\in \\mathcal{N}(x)\\}$$$

Lean4

theorem interior_eq_nhds' : interior s = {x | s ∈ 𝓝 x} :=
  Set.ext fun x => by simp only [mem_interior, mem_nhds_iff, mem_setOf_eq]

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