hasDerivWithinAt_arcsin_Iic — Mathlib

English

Let x ∈ ℝ with x ≠ 1. Then arcsin has a derivative within the half-line (−∞, x] at x with derivative 1/√(1 − x^2).

Русский

Пусть x ∈ ℝ и x ≠ 1. arcsin имеет производную внутри (−∞, x] в точке x равную 1/√(1 − x^2).

LaTeX

$$$HasDerivWithinAt(\\arcsin, \\tfrac{1}{\\sqrt{1 - x^2}}, \\mathrm{Iic}\\;x, x).$$$

Lean4

theorem hasDerivWithinAt_arcsin_Iic {x : ℝ} (h : x ≠ 1) : HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Iic x) x :=
  by
  rcases em (x = -1) with (rfl | h')
  · convert (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _ <;> simp +contextual [arcsin_of_le_neg_one]
  · exact (hasDerivAt_arcsin h' h).hasDerivWithinAt

Похожие утверждения