log — Mathlib

English

If a function f is ContinuousOn f on a set s and f never vanishes on s, then log(f) is ContinuousOn on s.

Русский

Если f непрерывна на множестве s и не обращается в ноль на s, то log(f) непрерывна на s.

LaTeX

$$$$ \\text{If } f\\text{ is ContinuousOn on } s\\text{ and } \\forall x\\in s, f(x) \\neq 0, \\ log(f(x)) \\text{ is continuous on } s. $$$$

Lean4

@[fun_prop]
theorem log (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun x => log (f x)) s := fun x hx =>
  (hf x hx).log (h₀ x hx)

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