measure_toMeasurable_union

Mathlib.MeasureTheory.Measure.MeasureSpace

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

← MathLib Explorer

English

For any sets s,t, μ(toMeasurable μ s ∪ t) = μ(s ∪ t).

Русский

Для любых множеств s,t верно μ(toMeasurable μ s ∪ t) = μ(s ∪ t).

LaTeX

$$$ μ\bigl(toMeasurable μ s \cup t\bigr) = μ(s \cup t) $$$

Lean4

@[simp]
theorem measure_toMeasurable_union : μ (toMeasurable μ s ∪ t) = μ (s ∪ t) :=
  Eq.symm <| measure_union_congr_of_subset (subset_toMeasurable _ _) (measure_toMeasurable _).le Subset.rfl le_rfl

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

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

Разделы

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

Аффилиация

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