continuousAt_rpow_const — Mathlib

English

For a fixed exponent q with q ≥ 0, the map x ↦ x^q is continuous on ℝ.

Русский

Для фиксированного показателя q ≥ 0 отображение x ↦ x^q непрерывно на ℝ.

LaTeX

$$$$\forall q\in\mathbb{R},\ q\ge 0\Rightarrow \text{Continuous}(x \mapsto x^q).$$$$

Lean4

@[fun_prop]
theorem continuousAt_rpow_const (x : ℝ) (q : ℝ) (h : x ≠ 0 ∨ 0 ≤ q) : ContinuousAt (fun x : ℝ => x ^ q) x :=
  by
  rw [le_iff_lt_or_eq, ← or_assoc] at h
  obtain h | rfl := h
  · exact (continuousAt_rpow (x, q) h).comp₂ continuousAt_id continuousAt_const
  · simp_rw [rpow_zero]; exact continuousAt_const

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