English
For hb0>0 and hb ≠ 1, log_b is continuous at x iff x ≠ 0.
Русский
При hb0>0 и b ≠ 1 лог_b непрерывна в x тогда и только тогда, когда x ≠ 0.
LaTeX
$$$0 < b \wedge b \neq 1 \Rightarrow \text{ContinuousAt}(\log_b b) x \iff x \neq 0$$$
Lean4
@[simp]
theorem continuousAt_logb_iff (hb₀ : 0 < b) (hb : b ≠ 1) : ContinuousAt (logb b) x ↔ x ≠ 0 :=
by
refine ⟨?_, continuousAt_logb⟩
rintro h rfl
cases lt_or_gt_of_ne hb with
| inl hb₁ =>
exact
not_tendsto_nhds_of_tendsto_atTop (tendsto_logb_nhdsNE_zero_of_base_lt_one hb₀ hb₁) _
(h.tendsto.mono_left inf_le_left)
| inr hb₁ =>
exact not_tendsto_nhds_of_tendsto_atBot (tendsto_logb_nhdsNE_zero hb₁) _ (h.tendsto.mono_left inf_le_left)