clog — Mathlib

English

If a complex-valued function f is continuous on a set s and f(x) lies in the slit plane for all x ∈ s, then log(f) is continuous on s.

Русский

Пусть f: α → ℂ непрерывна на s и для всех x∈s f(x) лежит в плоскости slitPlane; тогда log(f) непрерывна на s.

LaTeX

$$$f:\alpha \to \mathbb{C},\; s\subseteq\alpha,\; (\forall x\in s)\; f(x)\in\text{slitPlane} ∧ f\text{ непрерывно на }s \Rightarrow x\mapsto \log f(x)\text{ непрерывно на }s$$$

Lean4

nonrec theorem _root_.ContinuousOn.clog {f : α → ℂ} {s : Set α} (h₁ : ContinuousOn f s)
    (h₂ : ∀ x ∈ s, f x ∈ slitPlane) : ContinuousOn (fun t => log (f t)) s := fun x hx => (h₁ x hx).clog (h₂ x hx)

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