differentiableWithinAt_arcsin_Ici

English

For every real x, DifferentiableWithinAt arccos on Ici x holds iff x ≠ −1.

Русский

Для любого x ∈ ℝ, дифференцируемость arccos внутри (Ici x) эквивалентна x ≠ −1.

LaTeX

$$$\\text{DifferentiableWithinAt}(\\arccos, \\mathrm{Ici}\\;x, x) \\iff x \\neq -1.$$$

Lean4

theorem differentiableWithinAt_arcsin_Ici {x : ℝ} : DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1 :=
  by
  refine ⟨?_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
  rintro h rfl
  have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
    filter_upwards [Icc_mem_nhdsGE (neg_lt_self zero_lt_one)] with x using sin_arcsin'
  have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)
  simpa using (uniqueDiffOn_Ici _ _ left_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)

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