measurableSet_of_continuousAt — Mathlib

English

The set {x | ContinuousAt f x} is measurable for any function f into a pseudo-mymmetric metric space.

Русский

Множество {x | ContinuousAt f x} измеримо для любой функции f в псевдометрическое пространство.

LaTeX

$$$$ \text{MeasurableSet}(\{x \mid \text{ContinuousAt}(f,x)\}). $$$$

Lean4

theorem measurableSet_of_continuousAt {β} [PseudoEMetricSpace β] (f : α → β) : MeasurableSet {x | ContinuousAt f x} :=
  (IsGδ.setOf_continuousAt f).measurableSet

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