contDiffOn_log — Mathlib

English

Log is ContDiffOn on the domain excluding 0, i.e., log is smoothly differentiable away from 0.

Русский

Логарифм непрерывно-дифференцируем на множестве без нуля; логарифм гладко дифференцируем вне 0.

LaTeX

$$ContDiffOn ℝ n log (Set.compl {0})$$

Lean4

@[fun_prop]
theorem contDiffOn_log {n : WithTop ℕ∞} : ContDiffOn ℝ n log {0}ᶜ :=
  by
  intro x hx
  simp only [mem_compl_iff, mem_singleton_iff] at hx
  exact (contDiffAt_log.2 hx).contDiffWithinAt

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