measure_iUnion_null_iff — Mathlib

English

Let ι be a type with a countable index set. For s_i: ι → Set α, μ(⋃ i, s_i) = 0 iff ∀ i, μ(s_i) = 0.

Русский

Пусть ι — множество индексов счётного типа; для каждого i ∈ ι множество s_i ⊆ α: μ(⋃ i, s_i) = 0 тогда же, когда μ(s_i) = 0 для всех i.

LaTeX

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

Lean4

@[simp]
theorem measure_iUnion_null_iff {ι : Sort*} [Countable ι] {s : ι → Set α} : μ (⋃ i, s i) = 0 ↔ ∀ i, μ (s i) = 0 := by
  rw [← sUnion_range, measure_sUnion_null_iff (countable_range s), forall_mem_range]

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