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

edge_cost_zero_iff

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)

 103theorem edge_cost_zero_iff {x : V → ℝ} {v w : V}
 104    (hv : 0 < x v) (hw : 0 < x w) :
 105    Jcost (x v / x w) = 0 ↔ x v = x w := by

proof body

Term-mode proof.

 106  constructor
 107  · intro h
 108    have h1 := Jcost_zero_iff_one (div_pos hv hw) h
 109    rwa [div_eq_iff (ne_of_gt hw), one_mul] at h1
 110  · intro h
 111    rw [h, div_self (ne_of_gt hw)]
 112    exact Jcost_unit0
 113
 114end IndisputableMonolith.Papers.GCIC.GraphRigidity

depends on (9)

Lean names referenced from this declaration's body.