Continuity_Defined_from_Closed_Sets

Proved

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

closed-setscontinuous-mappingsproofwiki

Let $T_1$ and $T_2$ be topological spaces. Let $f: T_1 \to T_2$ be a mapping. Then $f$ is continuous for all $V$ closed in $T_2$ , $f^{-1} \sqbrk V$ is closed in $T_1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Continuity_Defined_from_Closed_Sets {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) := by sorry

Source

https://proofwiki.org/wiki/Continuity_Defined_from_Closed_Sets

View graph