measure_biUnion_null_iff — Mathlib

English

Let μ be an outer measure on α. For a countable index set I and sets s_i: I → Set α, we have μ(⋃_{i∈I} s_i) = 0 iff μ(s_i) = 0 for every i ∈ I.

Русский

Пусть μ — внешняя мера на α. Пусть I — счетное множество индексов и заданы множества s_i: I → Set α. Тогда μ(⋃_{i∈I} s_i) = 0 тогда же, когда μ(s_i) = 0 для всех i ∈ I.

LaTeX

$$$\\\\mu\\\\left\\\$\\\\\\\\bigcup_{\\\\,i\\\\in I} s_i\\\\\\\\right\\\$ = 0 \\\\Longleftrightarrow \\\\forall i\\\\in I,\\\\ \\\\mu(s_i) = 0$$$

Lean4

theorem measure_biUnion_null_iff {I : Set ι} (hI : I.Countable) {s : ι → Set α} :
    μ (⋃ i ∈ I, s i) = 0 ↔ ∀ i ∈ I, μ (s i) = 0 :=
  by
  refine ⟨fun h i hi ↦ measure_mono_null (subset_biUnion_of_mem hi) h, fun h ↦ ?_⟩
  have _ := hI.to_subtype
  simpa [h] using measure_iUnion_le (μ := μ) fun x : I ↦ s x

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