continuousOn_log — Mathlib

English

The log is continuous on the punctured real line, i.e. on ℝ \ {0}.

Русский

Логарифм непрерывен на множествах ℝ \ {0}.

LaTeX

$$$\\\\mathrm{ContinuousOn}(\\\\log, \\\\mathbb{R} \\\\setminus \\\\{0\\\\})$$$

Lean4

theorem continuousOn_log : ContinuousOn log {0}ᶜ :=
  by
  simp +unfoldPartialApp only [continuousOn_iff_continuous_restrict, restrict]
  conv in log _ => rw [log_of_ne_zero (show (x : ℝ) ≠ 0 from x.2)]
  exact expOrderIso.symm.continuous.comp (continuous_subtype_val.norm.subtype_mk _)

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