restrict_mono_set — Mathlib

English

If s ⊆ t almost everywhere with respect to μ, then μ|s ≤ μ|t; similarly, with μ ≤ ν, one gets μ|s ≤ ν|t.

Русский

Если s почти везде включено в t относительно μ, то μ|s ≤ μ|t; аналогично при μ ≤ ν получаем μ|s ≤ ν|t.

LaTeX

$$$(\text{ae } μ).\EventuallyLE(s, t) \rightarrow μ|s ≤ μ|t$.$$

Lean4

theorem restrict_mono_set {_ : MeasurableSpace α} (μ : Measure α) {s t : Set α} (h : s ⊆ t) :
    μ.restrict s ≤ μ.restrict t :=
  restrict_mono h le_rfl

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