restrict_apply — Mathlib

English

If the almost-everywhere relation holds (ae μ) between sets s and t, then μ|s ≤ μ|t in the measure order; this extends to the broader inequality when paired with μ ≤ ν.

Русский

Если s и t связаны отношением почти везде относительно μ, то μ|s ≤ μ|t в порядке мер; это распространяется на неравенство μ ≤ ν.

LaTeX

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

Lean4

/-- If `t` is a measurable set, then the measure of `t` with respect to the restriction of
  the measure to `s` equals the outer measure of `t ∩ s`. An alternate version requiring that `s`
  be measurable instead of `t` exists as `Measure.restrict_apply'`. -/
@[simp]
theorem restrict_apply (ht : MeasurableSet t) : μ.restrict s t = μ (t ∩ s) :=
  restrict_apply₀ ht.nullMeasurableSet

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