theorem proved term proof

`polynomial_continuous`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 277private theorem polynomial_continuous
 278    (a b c d e f : ℝ) :
 279    Continuous (Function.uncurry
 280      (fun u v : ℝ => a + b*u + c*v + d*u*v + e*u^2 + f*v^2)) := by

proof body

Term-mode proof.

 281  unfold Function.uncurry
 282  fun_prop
 283
 284/-- Polynomial route-independence implies continuous route-independence. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

polynomial_implies_continuous in IndisputableMonolith.Foundation.GeneralizedDAlembert decl_use