Theorems · Theorem · real analysis

ContinuousWithinAt.logb

∀ {α : Type u_1} {b : ℝ} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α},
  ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (fun x => Real.logb b (f x)) s a

Defined in

Mathlib.Analysis.SpecialFunctions.Log.Base

Cited by

1 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace