productive_iff — Mathlib

English

Let s be a weak sequence. Then s is productive if and only if every get? s n terminates.

Русский

Пусть s — слабая последовательность. Тогда s является продуктивной тогда и только тогда, когда для каждого n вычисление get? s n завершается.

LaTeX

$$$$ \mathrm{Productive}(s) \iff \forall n,\ (s.\mathrm{get?}\ n).\mathrm{Terminates}. $$$$

Lean4

theorem productive_iff (s : WSeq α) : Productive s ↔ ∀ n, (get? s n).Terminates :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

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