integral_subtype

Mathlib.MeasureTheory.Integral.Bochner.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.integral_subtype

← MathLib Explorer

English

Re-states the subtype integration equality: ∫ x : s, f x = ∫ x ∈ s, f x.

Русский

Повторяет равенство интеграла по подтипу: ∫ x : s, f x = ∫ x ∈ s, f x.

LaTeX

$$$$\int x : s, f x = \int x \in s, f x.$$$$

Lean4

theorem integral_subtype {α} [MeasureSpace α] {s : Set α} (hs : MeasurableSet s) (f : α → G) :
    ∫ x : s, f x = ∫ x in s, f x :=
  integral_subtype_comap hs f

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru