measure_biUnion_le

Mathlib.MeasureTheory.OuterMeasure.Basic

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

← MathLib Explorer

English

For I ⊆ ι, μ(⋃ i ∈ I, s i) ≤ ∑' i : I, μ(s i).

Русский

Для множества I ⊆ ι: μ(⋃ i∈I, s_i) ≤ ∑' i∈I μ(s_i).

LaTeX

$$$\forall I \subseteq ι,\; μ(\bigcup_{i\in I} s i) \le \sum' i: I, μ(s i)$$$

Lean4

theorem measure_biUnion_le {I : Set ι} (μ : F) (hI : I.Countable) (s : ι → Set α) :
    μ (⋃ i ∈ I, s i) ≤ ∑' i : I, μ (s i) := by
  have := hI.to_subtype
  rw [biUnion_eq_iUnion]
  apply measure_iUnion_le

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

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

Разделы

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

Аффилиация

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