measurable_of_measurable_on_compl_singleton

English

If singleton sets are measurable, then a function restricted to the complement of a point a is measurable implies f is measurable.

Русский

Если для одиноких точек выполняется измеримость, то f измеримо.

LaTeX

$$$\\\\operatorname{Measurable}({x \\\\neq a}.\\\\restrict f)$$$

Lean4

theorem measurable_of_measurable_on_compl_singleton [MeasurableSingletonClass α] {f : α → β} (a : α)
    (hf : Measurable ({x | x ≠ a}.restrict f)) : Measurable f :=
  measurable_of_measurable_on_compl_finite { a } (finite_singleton a) hf

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