hasIntegral_const — Mathlib

English

A constant function c has HasIntegral with value vol I c.

Русский

Пустьf(x) = c. Тогда существует интеграл с значением vol I c.

LaTeX

$$$\text{HasIntegral } I\ l\ (\lambda x. c)\ vol\ (vol\ I\ c)$$$

Lean4

theorem hasIntegral_const (c : E) : HasIntegral I l (fun _ => c) vol (vol I c) :=
  tendsto_const_nhds.congr' <|
    (l.eventually_isPartition I).mono fun _π hπ =>
      Eq.symm <| (vol.map ⟨⟨fun g : E →L[ℝ] F ↦ g c, rfl⟩, fun _ _ ↦ rfl⟩).sum_partition_boxes le_top hπ

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