clog — Mathlib

English

If f is continuous within a set and f(x) lies in the slit plane for every x in the set, then log∘f is continuous within the set.

Русский

Если f непрерывна на множестве и для каждого x из множества f(x) лежит во множестве с вырезом, то log(f) непрерывна на этом множестве.

LaTeX

$$$\forall x,\ x \in s \Rightarrow f(x) \in \text{slitPlane} \Rightarrow \mathrm{ContinuousWithinAt}(\log \circ f)\ s\ x$$$

Lean4

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

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