lean_workbook_plus_59358

Proved

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

Let $D$ be a compact subset of $\mathbb{R}$ and support that $f: D \rightarrow \mathbb{R}$ is continuous. Prove $f(D)$ is compact.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59358 (D : Set ℝ) (f : ℝ → ℝ)
    (hD : IsCompact D) (hf : ContinuousOn f D) :
    IsCompact (Set.image f D)   :=  by sorry

Source

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

View graph