unpair₂ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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