English
For ENNReal, the map x ↦ a − x is continuous on ENNReal away from ∞ (i.e., for x ≠ ∞).
Русский
Для ENNReal отображение x ↦ a − x непрерывно на множестве x ≠ ∞.
LaTeX
$$$\\\\forall a, x \\\\text{ with } x \\\\neq ∞, \\\\text{ContinuousAt } (\\\\lambda t, a - t) \\\\ x.$$$
Lean4
@[continuity, fun_prop]
protected theorem continuous_pow (n : ℕ) : Continuous fun a : ℝ≥0∞ => a ^ n := by
induction n with
| zero => simp [continuous_const]
| succ n IH =>
simp_rw [pow_add, pow_one, continuous_iff_continuousAt]
intro x
refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
· simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
· exact Or.inl fun h => H (pow_eq_zero h)
· simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne, not_false_iff, false_and]
· simp only [H, true_or, Ne, not_false_iff]
