lean_workbook_plus_4760

Proved

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

Let $X=(0,1) \in \mathbb{R}$ with the usual metric. Then $S=[0,1)$ is not closed.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4760 : ¬IsClosed (Set.Ico (0 : ℝ) 1)   :=  by sorry

Source