continuousOn_rpowIntegrand₀₁ — Mathlib

English

For p in (0,1) and x ≥ 0, the function t ↦ rpowIntegrand₀₁(p, t, x) is continuous on (0, ∞).

Русский

Для p ∈ (0,1) и x ≥ 0 функция t ↦ rpowIntegrand₀₁(p, t, x) непрерывна на (0, ∞).

LaTeX

$$$\text{ContinuousOn}(t \mapsto \mathrm{rpowIntegrand}_{01}(p,t,x), (0,\infty))$ для $p \in (0,1)$ и $x \ge 0$$$

Lean4

theorem continuousOn_rpowIntegrand₀₁ (hp : p ∈ Ioo 0 1) (hx : 0 ≤ x) : ContinuousOn (rpowIntegrand₀₁ p · x) (Ioi 0) :=
  by
  refine ContinuousOn.congr ?_ <| rpowIntegrand₀₁_eqOn_pow_div hp hx
  have h₀ : ContinuousOn (· ^ (p - 1) : ℝ → ℝ) (Ioi 0) := .rpow_const (by fun_prop) <| fun t ht => .inl ht.ne'
  fun_prop (disch := intros; simp_all; positivity)

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