lean_workbook_plus_46120

Proved

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

Given $f(x)^{2}=f(x^2)$ , prove that $f(x)\geq 0$ if $x\geq 0$ . Also, given $f(-x)=-f(x)$ , prove that $f(x)\leq 0$ if $x\leq 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46120 (f : ℝ → ℝ) (hf1 : ∀ x, f x ^ 2 = f (x ^ 2)) (hf2 : ∀ x, f (- x) = - f x) : ∀ x ≥ 0, f x ≥ 0   :=  by sorry

Source