countable_not_continuousWithinAt_Iio

English

In a second countable space, a monotone function has at most countably many left-discontinuities within a set.

Русский

В пространстве второй счетности монотонная функция имеет не более счетное число левых точек разрыва на заданном множестве.

LaTeX

$$$\text{MonotoneOn } f s \rightarrow \text{Set.Countable}\{x\in s \mid \neg\text{ContinuousWithinAt}(f, s \cap Iio x, x)\}$$$

Lean4

/-- In a second countable space, the set of points where a monotone function is not left-continuous
within a set is at most countable. Superseded by `MonotoneOn.countable_not_continuousWithinAt`
which gives the two-sided version. -/
theorem countable_not_continuousWithinAt_Iio (hf : MonotoneOn f s) :
    Set.Countable ({x ∈ s | ¬ContinuousWithinAt f (s ∩ Iio x) x}) :=
  hf.dual.countable_not_continuousWithinAt_Ioi

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