Real.sinh_bijective
theorem Real.sinh_bijective : Function.Bijective Real.sinh
The theorem `Real.sinh_bijective` states that the real hyperbolic sine function, represented by `Real.sinh`, is bijective, meaning it is both injective and surjective. In other words, every real output value is produced by exactly one real input value and every real number can be produced as an output. This implies that for any pair of real numbers, if the hyperbolic sine of the two numbers is equal then the numbers themselves are equal, and for any real number, there exists a real number whose hyperbolic sine is equal to it.
More concisely: The real hyperbolic sine function `Real.sinh` is a bijective function from the real numbers to themselves.
|
Real.differentiable_arsinh
theorem Real.differentiable_arsinh : Differentiable ℝ Real.arsinh
The theorem `Real.differentiable_arsinh` states that the function `arsinh`, which is defined for real numbers as `arsinh x = log (x + sqrt(1 + x^2))`, is differentiable at any point in its domain. In other words, for any real number `x`, the function `arsinh` has a derivative at `x`.
More concisely: The function `arsinh` is differentiable for all real numbers `x` in its domain.
|
Real.hasDerivAt_arsinh
theorem Real.hasDerivAt_arsinh : ∀ (x : ℝ), HasDerivAt Real.arsinh (1 + x ^ 2).sqrt⁻¹ x
The theorem `Real.hasDerivAt_arsinh` states that for all real numbers `x`, the function `arsinh`, which is defined as `arsinh x = log (x + sqrt(1 + x^2))`, has a derivative at the point `x`, and the derivative is equal to the reciprocal of `sqrt (1 + x ^ 2)`. In mathematical terms, we have $\frac{d}{dx} \text{arsinh} (x) = \frac{1}{\sqrt{1 + x^2}}$.
More concisely: The function `arsinh` has a derivative equal to the reciprocal of the square root of one plus the square of the argument at every real number. In mathematical notation, $\frac{d}{dx} \text{arsinh} (x) = \frac{1}{\sqrt{1 + x^2}}$.
|
Real.arsinh_sinh
theorem Real.arsinh_sinh : ∀ (x : ℝ), x.sinh.arsinh = x
This theorem states that the hyperbolic arc sine function (`arsinh`) is the left inverse of the hyperbolic sine function (`sinh`) for any real number `x`. In mathematical terms, this means that if you apply the `sinh` function to a real number `x` and then apply the `arsinh` function to the result, you will get back the original number `x`.
More concisely: The function `arsinh` is the left inverse of `sinh`, that is, `arsinh (sinh x) = x` for all real numbers `x`.
|
Real.sinh_surjective
theorem Real.sinh_surjective : Function.Surjective Real.sinh
The theorem `Real.sinh_surjective` states that the hyperbolic sine function (denoted as `sinh`) is surjective, which in mathematical terms means that for every real number `b`, there exists a real number `a` such that `sinh(a) = b`. In other words, every real number can be obtained as the hyperbolic sine of some real number. In this particular case, we find the required `a` as `a = arsinh(b)`, where `arsinh` is the inverse of the hyperbolic sine function.
More concisely: The hyperbolic sine function is a surjection from the real numbers to themselves.
|
Real.contDiff_arsinh
theorem Real.contDiff_arsinh : ∀ {n : ℕ∞}, ContDiff ℝ n Real.arsinh
The theorem `Real.contDiff_arsinh` declares that the inverse hyperbolic sine function (`arsinh`), which is defined on real numbers as `log (x + sqrt(1 + x^2))`, is continuously differentiable for all natural numbers `n`, including infinity. Continuous differentiability means that the function is smooth, i.e., it has continuous derivatives up to any order `n`.
More concisely: The function `arsinh : ℝ → ℝ` defined as `log (x + sqrt(1 + x^2))` is continuously differentiable for all natural numbers `n`, including infinity.
|
Real.sinh_arsinh
theorem Real.sinh_arsinh : ∀ (x : ℝ), x.arsinh.sinh = x
The theorem `Real.sinh_arsinh` states that the function `arsinh` acts as the right inverse of the function `sinh` for real numbers. In other words, for every real number `x`, if you first apply the `arsinh` function to `x` and then apply the `sinh` function to the result, you get back the original real number `x`. In mathematical terms, this is expressed as $\sinh(\text{arsinh}(x)) = x$ for all real numbers `x`.
More concisely: The `Real.sinh_arsinh` theorem asserts that for all real numbers `x`, `sinh(arsinh(x)) = x`.
|
Real.arsinh_zero
theorem Real.arsinh_zero : Real.arsinh 0 = 0
This theorem states that the inverse hyperbolic sine (also known as `arsinh` or `sinh^-1`) of zero is zero itself. In other words, if we input zero into the `arsinh` function, which is defined as `arsinh x = log (x + sqrt(1 + x^2))` where `log` is the natural logarithm and `sqrt` stands for the square root, the output will be zero. This is congruent with the mathematical property of the `arsinh` function.
More concisely: The theorem asserts that that the inverse hyperbolic sine of zero equals zero. In Lean 4, this is expressed as `arsinh 0 = 0`.
|
Real.hasStrictDerivAt_arsinh
theorem Real.hasStrictDerivAt_arsinh : ∀ (x : ℝ), HasStrictDerivAt Real.arsinh (1 + x ^ 2).sqrt⁻¹ x
The theorem `Real.hasStrictDerivAt_arsinh` states that for any real number `x`, the function `arsinh` has a strict derivative at the point `x`. Specifically, the derivative of `arsinh` at `x` is the reciprocal of the square root of `1 + x^2`. In mathematical terms, this can be written as: for all `x` in ℝ, the derivative of the `arsinh` function at `x` is `(1 + x^2)^{-0.5}`.
More concisely: The theorem `Real.hasStrictDerivAt_arsinh` asserts that the derivative of `arsinh(x)` at `x` is `(1 + x^2)^(-0.5)`.
|