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

diff_const_on_ReachN

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)

  30lemma diff_const_on_ReachN {δ : ℤ} {p q : Pot M}
  31  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) :

proof body

Tactic-mode proof.

  32  ∀ {n x y}, Causality.ReachN (Kin M) n x y → (p y - q y) = (p x - q x) := by
  33  intro n x y h
  34  induction h with
  35  | zero => rfl
  36  | @succ n x y z hxy hyz ih =>
  37      have h_edge : (p z - q z) = (p y - q y) :=
  38        edge_diff_invariant (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq hyz
  39      exact h_edge.trans ih
  40
  41/-- On reach components, the difference (p − q) equals its basepoint value. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.