numeric_powHalf — Mathlib

English

All powHalf(n) are numeric; powHalf(n).Numeric holds for every n.

Русский

Все powHalf(n) являются числовыми; powHalf(n).Numeric выполняется для любого n.

LaTeX

$$$\forall n, \ (\text{powHalf}(n)).\mathrm{Numeric}$$$

Lean4

/-- For all natural numbers `n`, the pre-games `powHalf n` are numeric. -/
theorem numeric_powHalf (n) : (powHalf n).Numeric := by
  induction n with
  | zero => exact numeric_one
  | succ n hn =>
    constructor
    · simpa using hn.moveLeft_lt default
    · exact ⟨fun _ => numeric_zero, fun _ => hn⟩

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