measure_union_null_iff — Mathlib

English

For any two sets s and t, the measure of their union is zero iff both s and t have zero measure.

Русский

Для любых двух множеств s и t мера их объединения равна нулю тогда и только тогда, когда обе меры равны нулю.

LaTeX

$$$\\\\mu\\\$s\\\\cup t\\\$ = 0 \\\\Longleftrightarrow \\\\mu(s) = 0 \\\\wedge \\\\mu(t) = 0$$$

Lean4

@[simp]
theorem measure_union_null_iff : μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0 := by simp [union_eq_iUnion, and_comm]

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