lean_workbook_plus_27568

Proved

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

Given $f(x) = -1$ for $x < 0$ and $f(x) = 1$ for $x \geq 0$ , and $g(x) = 0$ for all $x$ , is $g \circ f(x)$ continuous at $x = 0$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27568 (f g : ℝ → ℝ) (hf : f = fun x => if x < 0 then -1 else 1) (hg : g = fun _ => 0) : Continuous (g ∘ f)   :=  by sorry

Source