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

T4_unique_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)

  60theorem T4_unique_on_component {δ : ℤ} {p q : Pot M}
  61  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 y : M.U}

proof body

Tactic-mode proof.

  62  (hbase : p x0 = q x0)
  63  (hreach : Causality.Reaches (Kin M) x0 y) : p y = q y := by
  64  rcases hreach with ⟨n, h⟩
  65  exact T4_unique_on_reachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq (x0:=x0) hbase (n:=n) (y:=y) h
  66
  67/-- If y lies in the n-ball around x0, then the two δ-potentials agree at y. -/

depends on (12)

Lean names referenced from this declaration's body.