log — Mathlib

English

If hf is ContDiffWithinAt f s and hx ensures f x ≠ 0 for x ∈ s, then log ∘ f is ContDiffWithinAt on s.

Русский

Если hf — ContDiffWithinAt f s и hx гарантирует f x ≠ 0 для x ∈ s, то log ∘ f — ContDiffWithinAt на s.

LaTeX

$$ContDiffWithinAt log s x$$

Lean4

@[fun_prop]
theorem log {n} (hf : ContDiffWithinAt ℝ n f s x) (hx : f x ≠ 0) : ContDiffWithinAt ℝ n (fun x => log (f x)) s x :=
  (contDiffAt_log.2 hx).comp_contDiffWithinAt x hf

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