log

Mathlib.Analysis.SpecialFunctions.Log.Deriv

URI: https://scilib.ai/kg/mathlib#ContDiff.log

← MathLib Explorer

English

If f is ContDiff on a set s and f x ≠ 0 for all x in s, then log ∘ f is ContDiff on s.

Русский

Если f — ContDiff на s и f(x) ≠ 0 для всех x ∈ s, то log ∘ f — ContDiff на s.

LaTeX

$$ContDiff log s$$

Lean4

@[fun_prop]
theorem log {n} (hf : ContDiff ℝ n f) (h : ∀ x, f x ≠ 0) : ContDiff ℝ n fun x => log (f x) :=
  contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.log (h x)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru