trim_measurableSet_eq — Mathlib

English

Restricting the trim to a measurable set equals trimming the restriction: restrict(i) of v.trim(hle) equals (restrict(i) v).trim(hle) under measurability of i.

Русский

Ограничение тримирования к измеримому множеству даёт равенство: ограничение тримирования в i равно тримированию ограничения.

LaTeX

$$$ (vtrim\\ hle).restrict(i) = (v.restrict(i)).trim(hle) $ for measurable i$$

Lean4

theorem trim_measurableSet_eq (hle : m ≤ n) {i : Set α} (hi : MeasurableSet[m] i) : v.trim hle i = v i :=
  if_pos hi

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