continuousAt_logb_iff — Mathlib

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)

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