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

fromSubsetSum_isSolution

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)

 111theorem fromSubsetSum_isSolution {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
 112    (S : Finset (Fin n)) (h : (∑ i ∈ S, weight i) = target) :
 113    isSolution (fromSubsetSum weight target) ⟨S⟩ := by

proof body

Term-mode proof.

 114  constructor
 115  · simpa [weightTarget, weightSum, fromSubsetSum] using h
 116  constructor
 117  · simp [residueNeutral, residueSum, fromSubsetSum]
 118  · have hcost := fromSubsetSum_totalJCost_zero weight target S
 119    change totalJCost (fromSubsetSum weight target) ⟨S⟩ ≤ 0
 120    exact le_of_eq hcost
 121
 122end
 123
 124end BalancedJSubsetSum
 125end Cryptography
 126end IndisputableMonolith

depends on (13)

Lean names referenced from this declaration's body.