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

additive_three

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)

 202theorem additive_three (κ : CostFunction Config)
 203    (Γ₁ Γ₂ Γ₃ : Config)
 204    (_h₁₂ : Independent Γ₁ Γ₂)
 205    (_h₁₃ : Independent Γ₁ Γ₃)
 206    (h₂₃ : Independent Γ₂ Γ₃)
 207    (h₁_join : Independent Γ₁ (join Γ₂ Γ₃)) :
 208    κ.C (join Γ₁ (join Γ₂ Γ₃)) = κ.C Γ₁ + κ.C Γ₂ + κ.C Γ₃ := by

proof body

Term-mode proof.

 209  rw [κ.additivity Γ₁ (join Γ₂ Γ₃) h₁_join,
 210      κ.additivity Γ₂ Γ₃ h₂₃]
 211  ring
 212
 213/-- The (D) and (A) axioms together imply that the cost of an
 214independent join of two inconsistent configurations is strictly
 215larger than each individual cost. -/

used by (1)

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

depends on (22)

Lean names referenced from this declaration's body.