Lean-Workbook Plus 37935: Trigonometric inequality

Lean-Workbook Plus 37935: Monotonicity of x^a + a^x

For every real $a\ge1$, the function $x\mapsto x^a+a^x$ is nondecreasing on $[0,\infty)$: if $0\le x\le y$, then $x^a+a^x\le y^a+a^y$.

Source: Lean-Workbook row lean_workbook_plus_37935 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.