tail — Mathlib

English

If a reaches b in zero-step reachability and c is a possible next state from b, then a also reaches c.

Русский

Если из состояния a достигается состояние b в нулевом уровне достижимости и c является допустимым следующим состоянием после b, тогда a достигает и c.

LaTeX

$$$\\forall \\sigma\\, (f:\\\\sigma \\to \\mathrm{Option}\\,\\sigma),\\ a,b,c:\\sigma,\\ Reaches_0\\ f\\ a\\ b \\ \\to\\ c \\in f\\ b\\ \\to\\ Reaches_0\\ f\\ a\\ c$$$

Lean4

theorem tail {σ} {f : σ → Option σ} {a b c : σ} (h₁ : Reaches₀ f a b) (h : c ∈ f b) : Reaches₀ f a c :=
  h₁.trans (Reaches₀.single h)

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