continuous_parametric_intervalIntegral_of_continuous'

English

A variant showing that continuous uncurry of f yields continuous interval integral over the parametric domain.

Русский

Вариант, показывающий, что непрерывное разложение через uncurry приводит к непрерывности интервального интеграла по параметру.

LaTeX

$$$\\text{Continuous}\\left(\\text{Function.uncurry } f \right) \\Rightarrow \\text{Continuous intervalIntegral}(f, a, b, μ)$$$

Lean4

theorem continuous_parametric_intervalIntegral_of_continuous' (hf : Continuous f.uncurry) (a₀ b₀ : ℝ) :
    Continuous fun x ↦ ∫ t in a₀..b₀, f x t ∂μ := by fun_prop

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