Closed_Set_in_Topological_Subspace

Proved

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

closed-setsproofwikitopological-subspaces

Let $T$ be a topological space. Let $T' \subseteq T$ be a subspace of $T$ . Then $V \subseteq T'$ is closed in $T'$ $V = T' \cap W$ for some $W$ closed in $T$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Closed_Set_in_Topological_Subspace {α : Type _} [TopologicalSpace α] {s t : Set α} (hs : IsClosed s) : IsClosed ((↑) ⁻¹' s : Set t) := by sorry

Source

https://proofwiki.org/wiki/Closed_Set_in_Topological_Subspace

View graph