ThmDex – An index of mathematical definitions, results, and conjectures.
 ▼ Set of symbols ▼ Alphabet ▼ Deduction system ▼ Theory ▼ Zermelo-Fraenkel set theory ▼ Set ▼ Binary cartesian set product ▼ Binary relation ▼ Binary endorelation ▼ Preordering relation ▼ Partial ordering relation ▼ Partially ordered set ▼ Closed interval ▼ Implicit interval partition ▼ Implicit basic real interval partition ▼ Closed real interval tagged partition ▼ Stieltjes sum ▼ Riemann sum ▼ Riemann integrable real function ▼ Real Riemann integral
Definition D865
Standard natural real logarithm function

The standard natural real logarithm function is the D4364: Real function $$\log : (0, \infty) \to \mathbb{R}, \quad \log(x) = \int^x_1 \frac{1}{t} \, d t$$

The standard natural real logarithm function is the D4364: Real function $$\log : (0, \infty) \to \mathbb{R}, \quad \log(x) = \int^x_1 \frac{dt}{t}$$

The standard natural real logarithm function is the D4364: Real function $$\log : (0, \infty) \to \mathbb{R}, \quad \log(x) = \int^x_1 t^{-1} \, d t$$
Children
 ▶ D5705: Natural real entropy function ▶ D5754: Standard real log-sum-exp function ▶ D866: Standard real logarithm function
Results
 ▶ R4829: Base inversion property of standard natural logarithm function
Conventions
 ▶ Convention 0 (Notation for standard natural basic real logarithm function) The notation used for the D865: Standard natural real logarithm function is $x \mapsto \log(x)$ or $x \mapsto \ln(x)$.