contDiffAt_arccos_iff — Mathlib

English

ContDiffAt Real n arccos x holds iff n = 0 or x ≠ −1 ∧ x ≠ 1.

Русский

ContDiffAt Real n arccos x эквивалентно n = 0 или x ≠ −1 и x ≠ 1.

LaTeX

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

Lean4

theorem contDiffAt_arccos_iff {x : ℝ} {n : WithTop ℕ∞} : ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1 := by
  refine Iff.trans ⟨fun h => ?_, fun h => ?_⟩ contDiffAt_arcsin_iff <;>
    simpa [arccos] using (contDiffAt_const (c := π / 2)).sub h

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