iterate_eq_nil

Mathlib.Data.List.Iterate

URI: https://scilib.ai/kg/mathlib#List.iterate_eq_nil

English

For any f, a, n, iterate f a n = [] if and only if n = 0.

Русский

Для любых f, a, n выполнено: iterate f a n = [] тогда и только тогда, когда n = 0.

LaTeX

$$$$ \\operatorname{iterate} f\\, a\\, n = \\emptyset \\iff n = 0. $$$$

Lean4

@[simp]
theorem iterate_eq_nil {f : α → α} {a : α} {n : ℕ} : iterate f a n = [] ↔ n = 0 := by
  rw [← length_eq_zero_iff, length_iterate]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru