continuous_rpow_const — Mathlib

English

For any real y, the map a ↦ a^y is continuous on ENNReal.

Русский

Для любого вещественного y отображение a^y для a ∈ ENNReal непрерывно.

LaTeX

$$$\\\\forall y \\\\in \\\\mathbb{R},\\\\; \\text{Continuous}(a \\\\mapsto a^y) \\\\text{ on } \\\\mathbb{R}_{\\ge 0 \\infty}$$$

Lean4

@[continuity, fun_prop]
theorem continuous_rpow_const {y : ℝ} : Continuous fun a : ℝ≥0∞ => a ^ y :=
  by
  refine continuous_iff_continuousAt.2 fun x => ?_
  rcases lt_trichotomy (0 : ℝ) y with (hy | rfl | hy)
  · exact continuousAt_rpow_const_of_pos hy
  · simp only [rpow_zero]
    exact continuousAt_const
  · obtain ⟨z, hz⟩ : ∃ z, y = -z := ⟨-y, (neg_neg _).symm⟩
    have z_pos : 0 < z := by simpa [hz] using hy
    simp_rw [hz, rpow_neg]
    exact continuous_inv.continuousAt.comp (continuousAt_rpow_const_of_pos z_pos)

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