`edge_cost_zero_iff`

proved

show as: view math explainer →

module: IndisputableMonolith.Papers.GCIC.GraphRigidity
domain: Papers
line: 103 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Papers.GCIC.GraphRigidity on GitHub at line 103.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.