isCaratheodory_union — Mathlib

English

If s1 and s2 are Carathéodory-measurable with respect to m, then s1 ∪ s2 is Carathéodory-measurable.

Русский

Если s1 и s2 карatheodory-измеримы относительно m, то s1 ∪ s2 тоже карatheodory-измеримо.

LaTeX

$$m.IsCaratheodory s1 \rightarrow m.IsCaratheodory s2 \rightarrow m.IsCaratheodory (s1 \cup s2)$$

Lean4

theorem isCaratheodory_union (h₁ : IsCaratheodory m s₁) (h₂ : IsCaratheodory m s₂) : IsCaratheodory m (s₁ ∪ s₂) :=
  fun t =>
  by
  rw [h₁ t, h₂ (t ∩ s₁), h₂ (t \ s₁), h₁ (t ∩ (s₁ ∪ s₂)), inter_diff_assoc _ _ s₁, Set.inter_assoc _ _ s₁,
    inter_eq_self_of_subset_right Set.subset_union_left, union_diff_left, h₂ (t ∩ s₁)]
  simp [diff_eq, add_assoc]

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