lean_workbook_plus_17522
ProvedWhat if the function was defined as for all in the interval ? Show that is continuous on that interval, but there is no such that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17522 (g : ℝ → ℝ) (hg : ∀ x ∈ Set.Icc (0:ℝ) 1, g x = 0) : ContinuousOn g (Set.Icc (0:ℝ) 1) := by sorry
Source