lean_workbook_plus_74363

Proved

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

Can we use such function: $f(x) = 0$ for $x \in [0, \frac{1}{8}]$ and $f(x) = \frac{8x - 1}{14}$ for $x \geq \frac{1}{8}$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_74363 : ∃ f : ℝ → ℝ, ∀ x ∈ Set.Icc 0 (1 / 8), f x = 0 ∧ ∀ x ≥ 1 / 8, f x = (8 * x - 1) / 14   :=  by sorry

Source