evenOddRec_zero

Mathlib.Data.Nat.EvenOddRec

URI: https://scilib.ai/kg/mathlib#Nat.evenOddRec_zero

← MathLib Explorer

English

The value at 0 is the base case: evenOddRec h0 h_even h_odd 0 = h0.

Русский

Значение в точке 0 равно базовому случаю: evenOddRec h0 h_even h_odd 0 = h0.

LaTeX

$$$$ evenOddRec(h0,h_even,h_odd,0) = h0. $$$$

Lean4

@[simp]
theorem evenOddRec_zero {P : ℕ → Sort*} (h0 : P 0) (h_even : ∀ i, P i → P (2 * i)) (h_odd : ∀ i, P i → P (2 * i + 1)) :
    evenOddRec h0 h_even h_odd 0 = h0 :=
  binaryRec_zero _ _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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