English
In a second countable space, a monotone function has at most countably many points of discontinuity on the whole space.
Русский
Во втором счётном пространстве монотонная функция имеет не более счётного числа точек разрыва на всей области определения.
LaTeX
$$$\forall {\alpha, \beta} [LinearOrder(\alpha)] [TopologicalSpace(\alpha)] [OrderTopology(\alpha)] [LinearOrder(\beta)] [TopologicalSpace(\beta)] [OrderTopology(\beta)] [SecondCountableTopology(\beta)],\; (Monotone f) \rightarrow \{ x \mid \neg ContinuousAt f x \} \text{ is countable}.$$
Lean4
/-- In a second countable space, the set of points where a monotone function is not continuous
is at most countable. -/
theorem countable_not_continuousAt (hf : Monotone f) : Set.Countable {x | ¬ContinuousAt f x} := by
simpa [continuousWithinAt_univ] using (hf.monotoneOn univ).countable_not_continuousWithinAt
