differentiableAt_negMulLog_iff — Mathlib

English

DifferentiableAt negMulLog x if and only if x ≠ 0.

Русский

Функция negMulLog дифференцируема в точке x тогда и только тогда, когда x ≠ 0.

LaTeX

$$DifferentiableAt(\mathbb{R}, \operatorname{negMulLog}, x) \iff x \neq 0$$

Lean4

theorem differentiableAt_negMulLog_iff {x : ℝ} : DifferentiableAt ℝ negMulLog x ↔ x ≠ 0 :=
  by
  constructor
  · unfold negMulLog
    intro h eq0
    simp only [neg_mul, differentiableAt_fun_neg_iff, eq0] at h
    exact not_DifferentiableAt_log_mul_zero h
  · intro hx
    have : x ∈ ({0} : Set ℝ)ᶜ := by simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true]
    have := differentiableOn_negMulLog x this
    apply DifferentiableWithinAt.differentiableAt (s := {0}ᶜ) <;>
      simp_all only [ne_eq, Set.mem_compl_iff, Set.mem_singleton_iff, not_false_eq_true, compl_singleton_mem_nhds_iff]

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