Continuity of the sine of a sum of coordinate squares
ProvedWorkbookSource.problem_28348lean-workbooksource-checked
Show regoriously that the function is continuous at
Source: InternLM Lean-Workbook, record lean_workbook_28348 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_28348 (x y : ℝ) : Continuous fun p : ℝ × ℝ => sin (p.1^2 + p.2^2) := by sorry
Source