theorem
proved
edge_cost_zero_iff
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Papers.GCIC.GraphRigidity on GitHub at line 103.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
100/-! ### Corollary: edge cost characterizations -/
101
102/-- J(x_v/x_w) = 0 iff x_v = x_w, for positive x. -/
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
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