Prove2Me

lean_workbook_plus_62136

Proved

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

m≤g(1−x2)≤M⇔m4≤14g(1−x2)≤M4 m \le g\left( {1 - {x^2}} \right) \le M \Leftrightarrow \frac{m}{4} \le \frac{1}{4}g\left( {1 - {x^2}} \right) \le \frac{M}{4}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62136 (m M : ℝ) (x : ℝ) (g : ℝ → ℝ): m ≤ g (1 - x^2) ∧ g (1 - x^2) ≤ M ↔ m/4 ≤ (1/4) * g (1 - x^2) ∧ (1/4) * g (1 - x^2) ≤ M/4   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph