Prove2Me

lean_workbook_plus_81178

Proved

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

This is the case when UU is given by the full set 6x2+3y2−1≤0  ⟺  2x2+y2≤1/36x^2+3y^2-1\le 0\iff 2x^2+y^2\le 1/3 .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_81178 (x y : ℝ) (hx: x ∈ Set.Icc (-1) 1) (hy: y ∈ Set.Icc (-1) 1) : 6 * x ^ 2 + 3 * y ^ 2 - 1 ≤ 0 ↔ 2 * x ^ 2 + y ^ 2 ≤ 1 / 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph