measure_union_lt_top_iff — Mathlib

English

For sets s,t, μ(s ∪ t) < ∞ if and only if μ(s) < ∞ and μ(t) < ∞.

Русский

Для множеств s,t верно: μ(s ∪ t) < ∞ тогда и только тогда, когда μ(s) < ∞ и μ(t) < ∞.

LaTeX

$$μ(s ∪ t) < ∞ ↔ (μ(s) < ∞ ∧ μ(t) < ∞)$$

Lean4

@[simp]
theorem measure_union_lt_top_iff : μ (s ∪ t) < ∞ ↔ μ s < ∞ ∧ μ t < ∞ :=
  by
  refine ⟨fun h => ⟨?_, ?_⟩, fun h => measure_union_lt_top h.1 h.2⟩
  · exact (measure_mono Set.subset_union_left).trans_lt h
  · exact (measure_mono Set.subset_union_right).trans_lt h

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