92def singletonHinge {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) : 93 HingeDatum n :=
proof body
Definition body.
94 { edges := [(i, j)] 95 , weight := fun e => if e = (i, j) then w else 0 96 , weight_nonneg := by 97 intro e 98 by_cases h : e = (i, j) 99 · simp [h, hw] 100 · simp [h] 101 } 102
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.