measure_union_eq_top_iff — Mathlib

English

μ(s ∪ t) = ∞ if and only if μ(s) = ∞ or μ(t) = ∞.

Русский

μ(союз) бесконечна тогда и только тогда, когда μ(с) бесконечна или μ(т) бесконечна.

LaTeX

$$μ(s ∪ t) = ∞ ↔ μ(s) = ∞ ∨ μ(t) = ∞$$

Lean4

@[simp]
theorem measure_union_eq_top_iff : μ (s ∪ t) = ∞ ↔ μ s = ∞ ∨ μ t = ∞ :=
  not_iff_not.1 <| by simp only [← lt_top_iff_ne_top, ← Ne.eq_def, not_or, measure_union_lt_top_iff]

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