clog — Mathlib

English

If f is continuous at a point and f(x) lies in the slit plane, then log∘f is continuous at that point.

Русский

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

LaTeX

$$$\text{If } f \text{ continuous at } x \text{ and } f(x) \in \text{slitPlane},\ \log \circ f \text{ is continuous at } x$$$

Lean4

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

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