Condition_for_Point_being_in_Closure

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiset-closures

Let $T$ be a topological space. Let $H \subseteq T$ . Let $x \in T$ . Then $x \in H^-$ every open set of $T$ which contains $x$ contains a point in $H$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Condition_for_Point_being_in_Closure {α : Type _} [TopologicalSpace α] (s : Set α) (x : α) : x ∈ closure s ↔ ∀ U, IsOpen U → x ∈ U → (U ∩ s).Nonempty := by sorry

Source

https://proofwiki.org/wiki/Condition_for_Point_being_in_Closure

View graph