log — Mathlib

English

If f is a continuous function with values away from zero on a topological space, then the composition log ∘ f is continuous.

Русский

Если f непрерывна и её значения никогда не равны нулю, то композиция log ∘ f непрерывна.

LaTeX

$$$$ \\text{If } f: X \\to \\mathbb{R} \\text{ is continuous and } f(x) \\neq 0, \\ \\log\\circ f \\text{ is continuous.} $$$$

Lean4

@[fun_prop]
nonrec theorem log (hf : ContinuousAt f a) (h₀ : f a ≠ 0) : ContinuousAt (fun x => log (f x)) a :=
  hf.log h₀

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