English
If t is a subset of s, then the content on s without t equals the difference of contents: projectiveFamilyContent hP (s \ t) = projectiveFamilyContent hP s - projectiveFamilyContent hP t.
Русский
Если t ⊆ s, то содержание на s без t равно разности содержимостей: projectiveFamilyContent hP (s \ t) = projectiveFamilyContent hP s - projectiveFamilyContent hP t.
LaTeX
$$$\text{If } t \subseteq s, \quad \operatorname{projectiveFamilyContent} hP (s \setminus t) = \operatorname{projectiveFamilyContent} hP s - \operatorname{projectiveFamilyContent} hP t.$$$
Lean4
theorem projectiveFamilyContent_diff_of_subset [∀ J, IsFiniteMeasure (P J)] (hP : IsProjectiveMeasureFamily P)
(hs : s ∈ measurableCylinders α) (ht : t ∈ measurableCylinders α) (hts : t ⊆ s) :
projectiveFamilyContent hP (s \ t) = projectiveFamilyContent hP s - projectiveFamilyContent hP t :=
addContent_diff_of_ne_top (projectiveFamilyContent hP) isSetRing_measurableCylinders
(fun _ _ ↦ projectiveFamilyContent_ne_top hP) hs ht hts
