lean_workbook_plus_6055

Proved

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

$f(u,v)=a$ $\forall u,v$ such that $uv<0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_6055 (a : ℝ) (f : ℝ → ℝ → ℝ) (hf: ∀ u v : ℝ, u * v < 0 → f u v = a) : ∀ u v : ℝ, u * v < 0 → f u v = a   :=  by sorry

Source