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

additive_strict_of_both_inconsistent

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)

 216theorem additive_strict_of_both_inconsistent (κ : CostFunction Config)
 217    (Γ₁ Γ₂ : Config)
 218    (h_indep : Independent Γ₁ Γ₂)
 219    (h₁ : ¬IsConsistent Γ₁) (h₂ : ¬IsConsistent Γ₂) :
 220    κ.C (join Γ₁ Γ₂) > κ.C Γ₁ ∧ κ.C (join Γ₁ Γ₂) > κ.C Γ₂ := by

proof body

Term-mode proof.

 221  have h_eq : κ.C (join Γ₁ Γ₂) = κ.C Γ₁ + κ.C Γ₂ :=
 222    κ.additivity Γ₁ Γ₂ h_indep
 223  have h₁_pos : 0 < κ.C Γ₁ := cost_pos_of_inconsistent κ Γ₁ h₁
 224  have h₂_pos : 0 < κ.C Γ₂ := cost_pos_of_inconsistent κ Γ₂ h₂
 225  refine ⟨?_, ?_⟩
 226  · linarith
 227  · linarith
 228
 229/-- Cost is additive over independent join with the empty configuration
 230(degenerate case of independent additivity). -/

depends on (17)

Lean names referenced from this declaration's body.