Set_between_Connected_Set_and_Closure_is_Connected

Proved

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

connected-setsproofwikiset-between-connected-set-and-closure-is-connectedset-closures

Let $T$ be a topological space. Let $H$ be a connected set of $T$ . Let $H \subseteq K \subseteq H^-$ , where $H^-$ denotes the closure of $H$ . Then $K$ is connected.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Set_between_Connected_Set_and_Closure_is_Connected {α : Type _} [TopologicalSpace α] {s t : Set α} (hs : IsConnected s) (hst : s ⊆ t) (hts : t ⊆ closure s) : IsConnected t := by sorry

Source

https://proofwiki.org/wiki/Set_between_Connected_Set_and_Closure_is_Connected

View graph