reaches_eval — Mathlib

English

If a reaches b, then eval f a equals eval f b; evaluation is invariant along reachability.

Русский

Если a достигает b, то eval f a = eval f b; вычисление сохраняется по достижимости.

LaTeX

$$$\\operatorname{Reaches} f\\ a\\ b \\Rightarrow \\mathrm{eval}\\ f\\ a = \\mathrm{eval}\\ f\\ b$$$

Lean4

theorem reaches_eval {σ} {f : σ → Option σ} {a b} (ab : Reaches f a b) : eval f a = eval f b :=
  by
  refine Part.ext fun _ ↦ ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have ⟨ac, c0⟩ := mem_eval.1 h
    exact
      mem_eval.2 ⟨(or_iff_left_of_imp fun cb ↦ (eval_maximal h).1 cb ▸ ReflTransGen.refl).1 (reaches_total ab ac), c0⟩
  · have ⟨bc, c0⟩ := mem_eval.1 h
    exact mem_eval.2 ⟨ab.trans bc, c0⟩

Похожие утверждения