88lemma increment_on_ReachN {δ : ℤ} {p : Pot M} 89 (hp : DE (M:=M) δ p) :
proof body
Tactic-mode proof.
90 ∀ {n x y}, Causality.ReachN (Kin M) n x y → p y - p x = (n : ℤ) * δ := by 91 intro n x y h 92 induction h with 93 | zero => 94 simp 95 | @succ n x y z hxy hyz ih => 96 -- p z - p x = (p z - p y) + (p y - p x) = δ + n·δ = (n+1)·δ 97 have hz : p z - p y = δ := hp hyz 98 calc 99 p z - p x = (p z - p y) + (p y - p x) := by ring 100 _ = δ + (n : ℤ) * δ := by simpa [hz, ih] 101 _ = ((n : ℤ) + 1) * δ := by ring 102 _ = ((Nat.succ n : Nat) : ℤ) * δ := by 103 simp [Nat.cast_add] 104 105/-- Corollary: the set of potential differences along reaches is the δ-generated subgroup. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.