lean_workbook_plus_69149

Proved

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

ProofLet $y \in[ 0, 4k-\frac{1}{2}]$ , then $\frac{1}{8} + \frac{y}{4} \in [0,k]$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69149 (y : ℝ) (k : ℝ) (hy: y ∈ Set.Icc 0 (4 * k - 1 / 2)) : 1 / 8 + y / 4 ∈ Set.Icc 0 k   :=  by sorry

Source