pith. machine review for the scientific record. sign in
lemma proved tactic proof

diff_in_deltaSub

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)

 106lemma diff_in_deltaSub {δ : ℤ} {p : Pot M}
 107  (hp : DE (M:=M) δ p) {n x y}

proof body

Tactic-mode proof.

 108  (h : Causality.ReachN (Kin M) n x y) : ∃ k : ℤ, p y - p x = k * δ := by
 109  refine ⟨(n : ℤ), ?_⟩
 110  simpa using increment_on_ReachN (M:=M) (δ:=δ) (p:=p) hp (n:=n) (x:=x) (y:=y) h
 111
 112end Potential
 113end IndisputableMonolith

depends on (10)

Lean names referenced from this declaration's body.