lean_workbook_plus_19163

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $a>0$ and $t\ge 0$ , then : $g(x)=x^t$ $\forall x>0$ $g(0)=0$ $g(x)=-a(-x)^t$ $\forall x<0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19163 (a t : ℝ) (ha : a > 0) (ht : t ≥ 0) : ∃ g : ℝ → ℝ, ∀ x > 0, g x = x ^ t ∧ g 0 = 0 ∧ ∀ x < 0, g x = -a * (-x) ^ t   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph