log_ofReal_mul — Mathlib

English

If f is continuous on s and f(x) ∈ slitPlane for all x ∈ s, then log ∘ f is continuous on s.

Русский

Если f непрерывна на s и f(x) лежит в slitPlane для всех x ∈ s, то log ∘ f непрерывна на s.

LaTeX

$$$$\\text{ContinuousOn}(\\lambda t, \\log(f t))\\; s\\quad\\text{при } h_1:\\ ContinuousOn\, f\, s\\text{ и } h_2:\\forall x\\in s, f x \\in \\mathrm{slitPlane}.$$$$

Lean4

theorem log_ofReal_mul {r : ℝ} (hr : 0 < r) {x : ℂ} (hx : x ≠ 0) : log (r * x) = Real.log r + log x :=
  by
  replace hx := norm_ne_zero_iff.mpr hx
  simp_rw [log, norm_mul, norm_real, arg_real_mul _ hr, Real.norm_of_nonneg hr.le, Real.log_mul hr.ne' hx, ofReal_add,
    add_assoc]

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