pith. machine review for the scientific record. sign in
def definition def or abbrev

SeparatelyAdditive

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)

  47def SeparatelyAdditive (P : ℝ → ℝ → ℝ) : Prop :=

proof body

Definition body.

  48  ∃ p q : ℝ → ℝ, ∀ u v : ℝ, P u v = p u + q v
  49
  50/-- A combiner is a **coupling combiner** when it is not separately
  51additive. Equivalently, the joint structure of the two arguments enters
  52the output; the cost of a composite genuinely depends on how its
  53components fit together. -/

used by (6)

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

depends on (15)

Lean names referenced from this declaration's body.