measurable_of_continuousOn_compl_singleton

English

If a function is continuous on the complement of a single point in a T1 space, it is measurable.

Русский

Если функция непрерывна на дополнении одной точки в T1 пространстве, она измерима.

LaTeX

$$$[T1Space(\\alpha)]\\{a\\}\\;\\text{покрытие}\\\\ ContinuousOn(f, {a}^c)\\Rightarrow Measurable(f)$$$

Lean4

@[fun_prop]
theorem measurable_of_continuousOn_compl_singleton [T1Space α] {f : α → γ} (a : α) (hf : ContinuousOn f { a }ᶜ) :
    Measurable f :=
  measurable_of_measurable_on_compl_singleton a (continuousOn_iff_continuous_restrict.1 hf).measurable

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