Documentation

Marginis.Opris2023

On Preparation Theorems for R_an,exp –definable Functions #

by ANDRE OPRIS

We define Example 0.1 and show that f 0 0 = 0. A "LaTeX proof" of this would be: since 2 < e, ln 2 < 1, so ln (ln 2) < 0 max (ln (ln 2)) 1 = 1, and arctan (ln 1) = arctan 0 = 0.

noncomputable def opris (t : ) (x : ) :
Equations
Instances For