log — Mathlib

English

If a function f is ContinuousWithinAt at a point a on a set s and f(a) ≠ 0, then log ∘ f is ContinuousWithinAt at a on s.

Русский

Если f непрерывна на месте внутри области s в точке a и f(a) ≠ 0, то log(f(x)) непрерывна в этой точке по области.

LaTeX

$$$$ \\text{If } f: X \\to \\mathbb{R}, \\ \text{ ContinuousWithinAt } f\\ s\\ a \\text{ and } f(a) \\neq 0, \\text{ then } \\text{ContinuousWithinAt}(\\lambda x. \\log(f(x)))\\ s\\ a. $$$$

Lean4

nonrec theorem log (hf : ContinuousWithinAt f s a) (h₀ : f a ≠ 0) : ContinuousWithinAt (fun x => log (f x)) s a :=
  hf.log h₀

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