Real.contDiffAt_arcsin
theorem Real.contDiffAt_arcsin : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → ∀ {n : ℕ∞}, ContDiffAt ℝ n Real.arcsin x
The theorem `Real.contDiffAt_arcsin` states that for any real number `x` which is not equal to `-1` or `1`, and for any natural number or infinity `n`, the function `Real.arcsin` is continuously differentiable at `x`. In mathematical terms, this means the arcsine function has derivatives of all orders at any point in its domain, except at the points `-1` and `1`.
More concisely: For any real number `x` not equal to `-1` or `1`, the function `Real.arcsin` is continuously differentiable at `x`.
|
Real.differentiableAt_arcsin
theorem Real.differentiableAt_arcsin : ∀ {x : ℝ}, DifferentiableAt ℝ Real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1
The theorem states that the inverse of the sine function, `arcsin`, is differentiable at a real point `x` if and only if `x` is not equal to `-1` and `x` is not equal to `1`. In other words, the `arcsin` function has a derivative at a given point in its domain, except at points `-1` and `1`.
More concisely: The function `arcsin` is differentiable at a real number `x` if and only if `x ≠ -1` and `x ≠ 1`.
|
Real.hasDerivAt_arcsin
theorem Real.hasDerivAt_arcsin : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasDerivAt Real.arcsin (1 / (1 - x ^ 2).sqrt) x
The theorem `Real.hasDerivAt_arcsin` states that for all real numbers `x` that are not equal to `-1` or `1`, the function `Real.arcsin` has a derivative at `x`. The derivative is given by the function `1 / Real.sqrt (1 - x ^ 2)`. In other words, except at the points `-1` and `1`, the rate of change of the `arcsin` function at a point `x` is equal to `1` divided by the square root of `(1 - x ^ 2)`.
More concisely: For all real numbers `x` distinct from `-1` and `1`, the derivative of `Real.arcsin` at `x` exists and equals `1 / √(1 - x²)`.
|