unpair₁ — Mathlib

English

The first component of Nat.unpair(f(v)) is Primrec' if f is Primrec'.

Русский

Первая компонента распаковки Nat.unpair(·) является Primrec' при f Primrec'.

LaTeX

$$$\mathrm{unpair}_{1} : \ Primrec'\ n\ f \to\ Primrec'\ n\ (fun v => (f v).unpair.1)$$$

Lean4

theorem unpair₁ {n f} (hf : @Primrec' n f) : @Primrec' n fun v => (f v).unpair.1 :=
  by
  have s := sqrt.comp₁ _ hf
  have fss := sub.comp₂ _ hf (mul.comp₂ _ s s)
  refine (if_lt fss s fss s).of_eq fun v => ?_
  simp [Nat.unpair]; split_ifs <;> rfl

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