pith. machine review for the scientific record. sign in
theorem proved term proof

continuous_composition_not_enough

show as:
view Lean formalization →

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

generate prose now

formal statement (Lean)

  90theorem continuous_composition_not_enough :
  91    ¬ ∃ c : ℝ, ∀ a b : ℝ, 0 < a → 0 < b →
  92      quarticCombiner a b = 2 * a + 2 * b + c * a * b :=

proof body

Term-mode proof.

  93  quarticCombiner_not_rcl_family
  94
  95/-- Searchable boundary theorem: analytic composition is not enough to force
  96degree-two RCL form. -/

depends on (7)

Lean names referenced from this declaration's body.