Open_and_Closed_Sets_in_Topological_Space

Proved

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

clopen-setsproofwiki

Let $T = \struct {S, \tau}$ be a topological space. Then $S$ and $\O$ are both both open and closed in $T$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Open_and_Closed_Sets_in_Topological_Space {α : Type _} [TopologicalSpace α] : IsOpen (Set.univ : Set α) ∧ IsOpen (∅ : Set α) ∧ IsClosed (Set.univ : Set α) ∧ IsClosed (∅ : Set α) := by sorry

Source

https://proofwiki.org/wiki/Open_and_Closed_Sets_in_Topological_Space

View graph