projectiveFamilyContent_mono — Mathlib

English

If s ⊆ t and both are cylinders in the measurable cylinder system, then the content is monotone: projectiveFamilyContent hP s ≤ projectiveFamilyContent hP t.

Русский

Если s ⊆ t и оба являются цилиндрами в системе измеримых цилиндров, то содержимое не уменьшается: projectiveFamilyContent hP s ≤ projectiveFamilyContent hP t.

LaTeX

$$$\text{If } s \in measurableCylinders \text{ and } t \in measurableCylinders \text{ with } s \subseteq t, \text{ then } \ operatorname{projectiveFamilyContent} hP s \le \operatorname{projectiveFamilyContent} hP t.$$$

Lean4

theorem projectiveFamilyContent_mono (hP : IsProjectiveMeasureFamily P) (hs : s ∈ measurableCylinders α)
    (ht : t ∈ measurableCylinders α) (hst : s ⊆ t) : projectiveFamilyContent hP s ≤ projectiveFamilyContent hP t :=
  addContent_mono isSetSemiring_measurableCylinders hs ht hst

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