restrict_union₀ — Mathlib

English

Let μ be a measure on α. If s and t are AEDisjoint with respect to μ and t is null-measurable with respect to μ, then the restriction to s ∪ t equals the sum of the restrictions to s and to t.

Русский

Пусть μ — мера на α. Если s и t являются AE-несовместными относительно μ и t является μ-нулеизмеримым, то ограничение μ на s ∪ t равно сумме ограничений μ на s и μ на t.

LaTeX

$$$AEDisjoint\,\mu\,s\,t \land NullMeasurableSet\,t\,\mu \implies \mu\restriction (s \cup t) = \mu\restriction s + \mu\restriction t$$$

Lean4

theorem restrict_union₀ (h : AEDisjoint μ s t) (ht : NullMeasurableSet t μ) :
    μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t := by simp [← restrict_union_add_inter₀ s ht, restrict_zero_set h]

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