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

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)

  26lemma unique_on_reachN {δ : ℤ} {L L' : Recognition.Ledger M}
  27  (hL : IsAffine (M:=M) δ L) (hL' : IsAffine (M:=M) δ L')

proof body

Tactic-mode proof.

  28  {x0 : M.U} (hbase : Recognition.phi L x0 = Recognition.phi L' x0) :
  29  ∀ {n y}, Causality.ReachN (Potential.Kin M) n x0 y →
  30    Recognition.phi L y = Recognition.phi L' y := by
  31  intro n y hreach
  32  have : (fun x => Recognition.phi L x) y = (fun x => Recognition.phi L' x) y := by
  33    refine Potential.T4_unique_on_reachN (M:=M) (δ:=δ)
  34      (p:=fun x => Recognition.phi L x) (q:=fun x => Recognition.phi L' x)
  35      hL hL' (x0:=x0) (by simpa using hbase) (n:=n) (y:=y) hreach
  36  simpa using this
  37

depends on (13)

Lean names referenced from this declaration's body.