logb — Mathlib

English

Let f be a real-valued function defined on a topological space α, continuous on a subset s, and assume f(x) ≠ 0 for all x ∈ s. Then the function x ↦ log_b(f(x)) is continuous on s (log base b).

Русский

Пусть f: α → ℝ непрерывна на подмножестве s и для всех x ∈ s выполняется f(x) ≠ 0. Тогда функция x ↦ log_b(f(x)) непрерывна на s.

LaTeX

$$$\mathrm{ContinuousOn}(f,s) \land (\forall x \in s, f(x) \neq 0) \Rightarrow \mathrm{ContinuousOn}(x \mapsto \log_b(f(x)))\ s$$$

Lean4

@[fun_prop]
theorem logb (hf : ContinuousOn f s) (h₀ : ∀ x ∈ s, f x ≠ 0) : ContinuousOn (fun x => logb b (f x)) s := fun x hx =>
  (hf x hx).logb (h₀ x hx)

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