eval_maximal — Mathlib

English

If b is in eval f a, then every reachable c from b is trivial: Reaches f b c holds only when c = b.

Русский

Если b в eval f a, то все достигнутые из b состояния совпадают с b.

LaTeX

$$$b \\in \\mathrm{eval}\\ f\\ a \\Rightarrow \\forall c, \\mathrm{Reaches}\\ f\\ b\\ c \\Leftrightarrow c = b$$$

Lean4

theorem eval_maximal {σ} {f : σ → Option σ} {a b} (h : b ∈ eval f a) {c} : Reaches f b c ↔ c = b :=
  let ⟨_, b0⟩ := mem_eval.1 h
  reflTransGen_iff_eq fun b' h' ↦ by cases b0.symm.trans h'

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