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

ratio_rigidity_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)

  92theorem ratio_rigidity_iff {adj : V → V → Prop}
  93    (hconn : ∀ u v : V, Relation.ReflTransGen adj u v)
  94    {x : V → ℝ} (hpos : ∀ v, 0 < x v) :
  95    (∀ v w, adj v w → Jcost (x v / x w) = 0) ↔
  96    (∀ v w : V, x v = x w) :=

proof body

Term-mode proof.

  97  ⟨ratio_rigidity hconn hpos,
  98   fun hconst v w _ => constant_implies_zero_cost (hconst v w) (hpos w)⟩
  99
 100/-! ### Corollary: edge cost characterizations -/
 101
 102/-- J(x_v/x_w) = 0 iff x_v = x_w, for positive x. -/

depends on (8)

Lean names referenced from this declaration's body.