tail' — Mathlib

English

From a zero-level reachability and a next state from b, there exists a one-step reachability from a to that next state.

Русский

Из нулевой достижимости a к b и того, что c лежит в f(b), следует существование Reaches₁ f a c.

LaTeX

$$$\\forall \\sigma\\ (f:\\\\sigma \\\\to \\\\mathrm{Option}\\\\, a,b,c:\\sigma),\\ Reaches_0\\ f\\ a\\ b \\to c\\in f\\ b \\Rightarrow Reaches_1\\ 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 _ (TransGen.single h₂)

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