Composite_of_Continuous_Mappings_is_Continuous

Proved

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

composite-mappingscontinuous-mappingsproofwikitopology

Let $T_1, T_2, T_3$ be topological spaces. Let $f: T_1 \to T_2$ and $g: T_2 \to T_3$ be continuous mappings. Then the composite mapping $g \circ f: T_1 \to T_3$ is continuous.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Composite_of_Continuous_Mappings_is_Continuous {α : Type _} {β : Type _} {γ : Type _} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α → β) (g : β → γ) (hf : Continuous f) (hg : Continuous g) : Continuous (g ∘ f) := by sorry

Source

https://proofwiki.org/wiki/Composite_of_Continuous_Mappings_is_Continuous

View graph