lean_workbook_plus_17481

Proved

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

Suppose $f: U \rightarrow V, g: V \rightarrow \mathbb{R}$ are continuous functions where $U, V$ are open subsets of $\mathbb{R}$ . Prove that the composition $gf: U \rightarrow \mathbb{R}$ is continuous.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17481 (U V : Set ℝ) (f : U → V) (g : V → ℝ)
    (hf : Continuous f) (hg : Continuous g) : Continuous (g ∘ f)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph