mem_closure_iff_nhds' — Mathlib

English

x ∈ closure s iff nhds x ∩ s ≠ ∅ (equivalently, nhds x ⊓ 𝓟 s ≠ ⊥).

Русский

x ∈ замыкание s тогда и только тогда, когда nhds x ⊓ s ≠ ⊥ (эквивалентно nhds x ∩ s ≠ ∅).

LaTeX

$$$x \in \overline{s} \iff \mathcal{N}(x) \cap s \neq \emptyset$$

Lean4

theorem mem_closure_iff_nhds' : x ∈ closure s ↔ ∀ t ∈ 𝓝 x, ∃ y : s, ↑y ∈ t := by
  simp only [mem_closure_iff_nhds, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

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