restrict_of_not_measurable — Mathlib

English

If a set s is not measurable, then restricting a simple function to s yields the zero simple function.

Русский

Если множество s не измеримо, ограничение простой функции на s даёт нулевую простую функцию.

LaTeX

$$$\\text{restrict}(f,s) = 0 \\quad\\text{if } \\neg \\text{MeasurableSet}(s).$$$

Lean4

theorem restrict_of_not_measurable {f : α →ₛ β} {s : Set α} (hs : ¬MeasurableSet s) : restrict f s = 0 :=
  dif_neg hs

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