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

diff_const_on_component

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)

  42lemma diff_const_on_component {δ : ℤ} {p q : Pot M}
  43  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 y : M.U}

proof body

Tactic-mode proof.

  44  (hreach : Causality.Reaches (Kin M) x0 y) :
  45  (p y - q y) = (p x0 - q x0) := by
  46  rcases hreach with ⟨n, h⟩
  47  simpa using diff_const_on_ReachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (n:=n) (x:=x0) (y:=y) h
  48
  49/-- If two δ‑potentials agree at a basepoint, they agree on its n-step reach set. -/

used by (1)

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.