Lean-Workbook Plus 40944: Trigonometric identity

Proved

WorkbookRestored.plus_40944

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

The function $(u,v)\mapsto\sin(u^2+v^2)$ is continuous on $\mathbb R^2$ , in particular at the origin.

Source: Lean-Workbook row lean_workbook_plus_40944 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.

Preamble

import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
open Real

Formal statement

theorem WorkbookRestored.plus_40944 (x y : ℝ) : Continuous (fun p : ℝ × ℝ => sin (p.1^2 + p.2^2))   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_40944; immutable original Prove2Me node faf2ec93-96c5-46c6-b710-7454ed63b1bb

View graph