corec_nil — Mathlib

English

If at state b the generating step yields none, then the corecursive stream is empty (nil).

Русский

Если на состоянии b функция генерации возвращает none, то результирующий поток пуст (nil).

LaTeX

$$$\\forall f:\\beta \\to \\mathrm{Option}(\\alpha \\times \\beta),\\; b:\\beta,\\; f(b)=\\mathrm{none} \\Rightarrow \\mathrm{corec}\\,f\\,b = \\mathrm{nil}.$$$

Lean4

theorem corec_nil (f : β → Option (α × β)) (b : β) (h : f b = .none) : corec f b = nil :=
  by
  apply destruct_eq_none
  simp [h]

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