lean_workbook_plus_69642
ProvedLet are real numbers such that and Show that at least one of the numbers is greater than or equal to (JBMO 2009 Shortlist A4)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69642 (x y z : ℝ) (hx : 0 < x ∧ x < 1) (hy : 0 < y ∧ y < 1) (hz : 0 < z ∧ z < 1) (h : x * y * z = (1 - x) * (1 - y) * (1 - z)) : 1 / 4 ≤ (1 - x) * y ∨ (1 - y) * z ≥ 1 / 4 ∨ (1 - z) * x ≥ 1 / 4 := by sorry
Source