piPremeasure_pi_mono — Mathlib

English

If s ⊆ t are sets of the product space, then piPremeasure(m, s) ≤ piPremeasure(m, t).

Русский

Если множество s вложено в t, то piPremeasure(m, s) ≤ piPremeasure(m, t).

LaTeX

$$s \subseteq t \implies \text{piPremeasure}(m)(s) \le \text{piPremeasure}(m)(t)$$

Lean4

theorem piPremeasure_pi_mono {s t : Set (∀ i, α i)} (h : s ⊆ t) : piPremeasure m s ≤ piPremeasure m t :=
  Finset.prod_le_prod' fun _ _ => measure_mono (Set.image_mono h)

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