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

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

  50theorem T4_unique_on_reachN {δ : ℤ} {p q : Pot M}
  51  (hp : DE (M:=M) δ p) (hq : DE (M:=M) δ q) {x0 : M.U}

proof body

Tactic-mode proof.

  52  (hbase : p x0 = q x0) : ∀ {n y}, Causality.ReachN (Kin M) n x0 y → p y = q y := by
  53  intro n y h
  54  have hdiff := diff_const_on_ReachN (M:=M) (δ:=δ) (p:=p) (q:=q) hp hq h
  55  have : p x0 - q x0 = 0 := by simp [hbase]
  56  have : p y - q y = 0 := by simpa [this] using hdiff
  57  exact sub_eq_zero.mp this
  58
  59/-- Componentwise uniqueness: if p and q agree at x0, then they agree at every y reachable from x0. -/

used by (3)

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

depends on (15)

Lean names referenced from this declaration's body.