English
Let v1, v2, w be vector measures with v1 ⟂ᵥ w and v2 ⟂ᵥ w. Then v1 + v2 is mutually singular to w.
Русский
Пусть векторные меры v1, v2 и w удовлетворяют v1 ⟂ᵥ w и v2 ⟂ᵥ w. Тогда v1 + v2 взаимно обособлена от w.
LaTeX
$$$ (v_1 \\perp_{\\mathcal{V}} w) \\land (v_2 \\perp_{\\mathcal{V}} w) \\implies (v_1 + v_2) \\perp_{\\mathcal{V}} w $$$
Lean4
theorem add_left [T2Space N] [ContinuousAdd M] (h₁ : v₁ ⟂ᵥ w) (h₂ : v₂ ⟂ᵥ w) : v₁ + v₂ ⟂ᵥ w :=
by
obtain ⟨u, hmu, hu₁, hu₂⟩ := h₁
obtain ⟨v, hmv, hv₁, hv₂⟩ := h₂
refine mk (u ∩ v) (hmu.inter hmv) (fun t ht _ => ?_) fun t ht hmt => ?_
· rw [add_apply, hu₁ _ (Set.subset_inter_iff.1 ht).1, hv₁ _ (Set.subset_inter_iff.1 ht).2, zero_add]
· rw [Set.compl_inter] at ht
rw [(_ : t = uᶜ ∩ t ∪ vᶜ \ uᶜ ∩ t), of_union _ (hmu.compl.inter hmt) ((hmv.compl.diff hmu.compl).inter hmt), hu₂,
hv₂, add_zero]
· exact Set.Subset.trans Set.inter_subset_left diff_subset
· exact Set.inter_subset_left
· exact disjoint_sdiff_self_right.mono Set.inter_subset_left Set.inter_subset_left
· apply Set.Subset.antisymm <;> intro x hx
· by_cases hxu' : x ∈ uᶜ
· exact Or.inl ⟨hxu', hx⟩
rcases ht hx with (hxu | hxv)
exacts [False.elim (hxu' hxu), Or.inr ⟨⟨hxv, hxu'⟩, hx⟩]
· rcases hx with hx | hx <;> exact hx.2
