Theorems · Theorem · real analysis
ContinuousWithinAt.log
∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {a : α},
ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (fun x => Real.log (f x)) s a- Cited by
- 3 results in Mathlib
- Foundations
- Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- Real.logstatement · cited by 939
- ContinuousWithinAtstatement and proof · cited by 512
- Filter.Tendsto.logproof · cited by 3
Cited by3
Results whose statement or proof uses this declaration.
- ContinuousOn.logproof · cited by 11
- Complex.continuousWithinAt_log_of_re_neg_of_im_zeroproof · cited by 1
- Complex.tendsto_log_nhdsWithin_im_neg_of_re_neg_of_im_zeroproof · cited by 0