contDiffAt_arcsin_iff — Mathlib

English

For all x ∈ ℝ, ContDiffAt ℝ n arcsin x holds if and only if n = 0 or x ≠ −1 ∧ x ≠ 1.

Русский

Для всех x ∈ ℝ, ContDiffAt ℝ n(arcsin, x) эквивалентно n = 0 или x ≠ −1 и x ≠ 1.

LaTeX

$$$\\text{ContDiffAt}(\\mathbb{R}, n, \\arcsin, x) \\iff (n = 0) \\lor (x \\neq -1 \\land x \\neq 1).$$$

Lean4

theorem contDiffAt_arcsin_iff {x : ℝ} {n : WithTop ℕ∞} : ContDiffAt ℝ n arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1 :=
  ⟨fun h =>
    or_iff_not_imp_left.2 fun hn =>
      differentiableAt_arcsin.1 <| h.differentiableAt <| ENat.one_le_iff_ne_zero_withTop.mpr hn,
    fun h =>
    h.elim (fun hn => hn.symm ▸ (contDiff_zero.2 continuous_arcsin).contDiffAt) fun hx => contDiffAt_arcsin hx.1 hx.2⟩

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