binaryRecFromOne — Mathlib

English

A variant of binaryRec that treats 1 as a base case in addition to 0.

Русский

Вариант binaryRec, который рассматривает 1 как базовый случай вместе с 0.

LaTeX

$$$\text{binaryRecFromOne}\;\text{motive}\;\text{zero}\;\text{one}\;\text{bit}\;n$$$

Lean4

/-- The same as `binaryRec`, but special casing both 0 and 1 as base cases -/
@[elab_as_elim, specialize]
def binaryRecFromOne {motive : Nat → Sort u} (zero : motive 0) (one : motive 1)
    (bit : ∀ b n, n ≠ 0 → motive n → motive (bit b n)) : ∀ n, motive n :=
  binaryRec' zero fun b n h ih =>
    if h' : n = 0 then
      have : n.bit b = Nat.bit true 0 := by rw [h', h h']
      congrArg motive this ▸ one
    else bit b n h' ih

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