mem_closure_iff_comap_neBot — Mathlib

English

x ∈ closure s iff nhdsWithin x s ≠ ⊥.

Русский

x принадлежит замыканию s тогда и только тогда, когда nhdsWithin x s не тождественно нулю.

LaTeX

$$$x \in \overline{s} \iff nhdsWithin\ x\ s \neq \bot$$

Lean4

theorem mem_closure_iff_comap_neBot : x ∈ closure s ↔ NeBot (comap ((↑) : s → X) (𝓝 x)) := by
  simp_rw [mem_closure_iff_nhds, comap_neBot_iff, Set.inter_nonempty_iff_exists_right, SetCoe.exists, exists_prop]

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