sublistsLenAux_zero — Mathlib

English

Base case for the auxiliary function: when the length parameter is zero, the result is f([]) cons to r.

Русский

Базовый случай вспомогательной функции: при длине равной нулю результат равен f([]) :: r.

LaTeX

$$$\\operatorname{sublistsLenAux}(0, l, f, r) = f([]) :: r$$$

Lean4

theorem sublistsLenAux_zero (l : List α) (f : List α → β) (r) : sublistsLenAux 0 l f r = f [] :: r := by cases l <;> rfl

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