lean_workbook_plus_45807

Proved

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

Given the equations $x^2+y^2=1$ and $u^2+v^2=1$ , prove that $xu+yv\le1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45807 : ∀ x y u v : ℝ, x^2 + y^2 = 1 ∧ u^2 + v^2 = 1 → x * u + y * v ≤ 1   :=  by sorry

Source