projectiveFamilyContent_diff — Mathlib

English

For cylinders s and t, the difference content is controlled by the content of s \ t: projectiveFamilyContent hP s - projectiveFamilyContent hP t ≤ projectiveFamilyContent hP (s \ t).

Русский

Для цилиндров s и t разность содержания удовлетворяет неравенству: projectiveFamilyContent hP s - projectiveFamilyContent hP t ≤ projectiveFamilyContent hP (s \ t).

LaTeX

$$$\operatorname{projectiveFamilyContent} hP s - \operatorname{projectiveFamilyContent} hP t \le \operatorname{projectiveFamilyContent} hP (s \setminus t)$$$

Lean4

theorem projectiveFamilyContent_diff (hP : IsProjectiveMeasureFamily P) (hs : s ∈ measurableCylinders α)
    (ht : t ∈ measurableCylinders α) :
    projectiveFamilyContent hP s - projectiveFamilyContent hP t ≤ projectiveFamilyContent hP (s \ t) :=
  le_addContent_diff (projectiveFamilyContent hP) isSetRing_measurableCylinders hs ht

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