clog — Mathlib

English

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

Русский

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

LaTeX

$$$$\\text{Continuous } f \\Rightarrow \\text{Continuous }(\\lambda x, \\log(f x))\\text{ under slitPlane condition.}$$$$

Lean4

nonrec theorem _root_.Continuous.clog {f : α → ℂ} (h₁ : Continuous f) (h₂ : ∀ x, f x ∈ slitPlane) :
    Continuous fun t => log (f t) :=
  continuous_iff_continuousAt.2 fun x => h₁.continuousAt.clog (h₂ x)

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