The greatest element of a five-value set

Proved

WorkbookSource.problem_45429

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

If $a=-2$ , the largest number in the set $\\left \\{ -3a,4a,\\frac{24}{a},a^2,1 \\right \\}$ is

Source: InternLM Lean-Workbook, record lean_workbook_45429 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_45429 (a : ℝ) (h : a = -2) : 
  IsGreatest ({-3*a, 4*a, 24/a, a^2, 1} : Set ℝ) 6  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_45429; Apache-2.0

View graph