measure_inter_union — Mathlib

English

If s1 and s2 are disjoint, then m(t ∩ (s1 ∪ s2)) = m(t ∩ s1) + m(t ∩ s2) for all t.

Русский

Если s1 и s2 не пересекаются, то для любого t выполняется m(t ∩ (s1 ∪ s2)) = m(t ∩ s1) + m(t ∩ s2).

LaTeX

$$h : s1 ∩ s2 ⊆ ∅ → m.IsCaratheodory s1 → ∀ t, m (t ∩ (s1 ∪ s2)) = m (t ∩ s1) + m (t ∩ s2)$$

Lean4

theorem measure_inter_union (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : IsCaratheodory m s₁) {t : Set α} :
    m (t ∩ (s₁ ∪ s₂)) = m (t ∩ s₁) + m (t ∩ s₂) := by
  rw [h₁, Set.inter_assoc, Set.union_inter_cancel_left, inter_diff_assoc, union_diff_cancel_left h]

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